|
1 (* ========================================================================= *) |
|
2 (* THE WAITING SET OF CLAUSES *) |
|
3 (* Copyright (c) 2002-2007 Joe Hurd, distributed under the GNU GPL version 2 *) |
|
4 (* ========================================================================= *) |
|
5 |
|
6 signature Waiting = |
|
7 sig |
|
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 |
|
27 type weight = real |
|
28 |
|
29 type modelParameters = |
|
30 {model : Model.parameters, |
|
31 initialPerturbations : int, |
|
32 maxChecks : int option, |
|
33 perturbations : int, |
|
34 weight : weight} |
|
35 |
|
36 type 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 |
|
46 type waiting |
|
47 |
|
48 type distance |
|
49 |
|
50 (* ------------------------------------------------------------------------- *) |
|
51 (* Basic operations. *) |
|
52 (* ------------------------------------------------------------------------- *) |
|
53 |
|
54 val default : parameters |
|
55 |
|
56 val new : |
|
57 parameters -> |
|
58 {axioms : Clause.clause list, |
|
59 conjecture : Clause.clause list} -> waiting |
|
60 |
|
61 val size : waiting -> int |
|
62 |
|
63 val pp : waiting Print.pp |
|
64 |
|
65 (* ------------------------------------------------------------------------- *) |
|
66 (* Adding new clauses. *) |
|
67 (* ------------------------------------------------------------------------- *) |
|
68 |
|
69 val add : waiting -> distance * Clause.clause list -> waiting |
|
70 |
|
71 (* ------------------------------------------------------------------------- *) |
|
72 (* Removing the lightest clause. *) |
|
73 (* ------------------------------------------------------------------------- *) |
|
74 |
|
75 val remove : waiting -> ((distance * Clause.clause) * waiting) option |
|
76 |
|
77 end |