1 (* ========================================================================= *) |
1 (* ========================================================================= *) |
2 (* THE WAITING SET OF CLAUSES *) |
2 (* THE WAITING SET OF CLAUSES *) |
3 (* Copyright (c) 2002-2007 Joe Hurd, distributed under the BSD License *) |
3 (* Copyright (c) 2002-2007 Joe Hurd, distributed under the BSD License *) |
4 (* ========================================================================= *) |
4 (* ========================================================================= *) |
5 |
5 |
6 signature Waiting = |
6 signature Waiting = |
7 sig |
7 sig |
8 |
8 |
9 (* ------------------------------------------------------------------------- *) |
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 (* ------------------------------------------------------------------------- *) |
10 (* A type of waiting sets of clauses. *) |
43 (* A type of waiting sets of clauses. *) |
11 (* ------------------------------------------------------------------------- *) |
44 (* ------------------------------------------------------------------------- *) |
12 |
|
13 type parameters = |
|
14 {symbolsWeight : real, |
|
15 literalsWeight : real, |
|
16 modelsWeight : real, |
|
17 modelChecks : int, |
|
18 models : Model.parameters list} |
|
19 |
45 |
20 type waiting |
46 type waiting |
21 |
47 |
22 type distance |
48 type distance |
23 |
49 |
25 (* Basic operations. *) |
51 (* Basic operations. *) |
26 (* ------------------------------------------------------------------------- *) |
52 (* ------------------------------------------------------------------------- *) |
27 |
53 |
28 val default : parameters |
54 val default : parameters |
29 |
55 |
30 val new : parameters -> Clause.clause list -> waiting |
56 val new : |
|
57 parameters -> |
|
58 {axioms : Clause.clause list, |
|
59 conjecture : Clause.clause list} -> waiting |
31 |
60 |
32 val size : waiting -> int |
61 val size : waiting -> int |
33 |
62 |
34 val pp : waiting Parser.pp |
63 val pp : waiting Print.pp |
35 |
64 |
36 (* ------------------------------------------------------------------------- *) |
65 (* ------------------------------------------------------------------------- *) |
37 (* Adding new clauses. *) |
66 (* Adding new clauses. *) |
38 (* ------------------------------------------------------------------------- *) |
67 (* ------------------------------------------------------------------------- *) |
39 |
68 |