src/Tools/Metis/src/Waiting.sig

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Waiting.sig	Wed Jun 20 22:07:52 2007 +0200
@@ -0,0 +1,48 @@
+(* ========================================================================= *)
+(* THE WAITING SET OF CLAUSES                                                *)
+(* Copyright (c) 2002-2007 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Waiting =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of waiting sets of clauses.                                        *)
+(* ------------------------------------------------------------------------- *)
+
+type parameters =
+     {symbolsWeight : real,
+      literalsWeight : real,
+      modelsWeight : real,
+      modelChecks : int,
+      models : Model.parameters list}
+
+type waiting
+
+type distance
+
+(* ------------------------------------------------------------------------- *)
+(* Basic operations.                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+val default : parameters
+
+val new : parameters -> Clause.clause list -> waiting
+
+val size : waiting -> int
+
+val pp : waiting Parser.pp
+
+(* ------------------------------------------------------------------------- *)
+(* Adding new clauses.                                                       *)
+(* ------------------------------------------------------------------------- *)
+
+val add : waiting -> distance * Clause.clause list -> waiting
+
+(* ------------------------------------------------------------------------- *)
+(* Removing the lightest clause.                                             *)
+(* ------------------------------------------------------------------------- *)
+
+val remove : waiting -> ((distance * Clause.clause) * waiting) option
+
+end