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