1(* ========================================================================= *) 2(* THE WAITING SET OF CLAUSES *) 3(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6signature Waiting = 7sig 8 9(* ------------------------------------------------------------------------- *) 10(* The parameters control the order that clauses are removed from the *) 11(* waiting set: clauses are assigned a weight and removed in strict weight *) 12(* order, with smaller weights being removed before larger weights. *) 13(* *) 14(* The weight of a clause is defined to be *) 15(* *) 16(* d * s^symbolsWeight * v^variablesWeight * l^literalsWeight * m *) 17(* *) 18(* where *) 19(* *) 20(* d = the derivation distance of the clause from the axioms *) 21(* s = the number of symbols in the clause *) 22(* v = the number of distinct variables in the clause *) 23(* l = the number of literals in the clause *) 24(* m = the truth of the clause wrt the models *) 25(* ------------------------------------------------------------------------- *) 26 27type weight = real 28 29type modelParameters = 30 {model : Model.parameters, 31 initialPerturbations : int, 32 maxChecks : int option, 33 perturbations : int, 34 weight : weight} 35 36type parameters = 37 {symbolsWeight : weight, 38 variablesWeight : weight, 39 literalsWeight : weight, 40 models : modelParameters list} 41 42(* ------------------------------------------------------------------------- *) 43(* A type of waiting sets of clauses. *) 44(* ------------------------------------------------------------------------- *) 45 46type waiting 47 48type distance 49 50(* ------------------------------------------------------------------------- *) 51(* Basic operations. *) 52(* ------------------------------------------------------------------------- *) 53 54val default : parameters 55 56val new : 57 parameters -> 58 {axioms : Clause.clause list, 59 conjecture : Clause.clause list} -> waiting 60 61val size : waiting -> int 62 63val pp : waiting Print.pp 64 65(* ------------------------------------------------------------------------- *) 66(* Adding new clauses. *) 67(* ------------------------------------------------------------------------- *) 68 69val add : waiting -> distance * Clause.clause list -> waiting 70 71(* ------------------------------------------------------------------------- *) 72(* Removing the lightest clause. *) 73(* ------------------------------------------------------------------------- *) 74 75val remove : waiting -> ((distance * Clause.clause) * waiting) option 76 77end 78