equal
deleted
inserted
replaced
1 (* ========================================================================= *) |
1 (* ========================================================================= *) |
2 (* THE ACTIVE SET OF CLAUSES *) |
2 (* THE ACTIVE SET OF CLAUSES *) |
3 (* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *) |
3 (* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *) |
4 (* ========================================================================= *) |
4 (* ========================================================================= *) |
5 |
5 |
6 signature Active = |
6 signature Active = |
7 sig |
7 sig |
8 |
8 |
9 (* ------------------------------------------------------------------------- *) |
9 (* ------------------------------------------------------------------------- *) |
10 (* A type of active clause sets. *) |
10 (* A type of active clause sets. *) |
11 (* ------------------------------------------------------------------------- *) |
11 (* ------------------------------------------------------------------------- *) |
12 |
12 |
13 type simplify = {subsume : bool, reduce : bool, rewrite : bool} |
13 type simplify = |
|
14 {subsume : bool, |
|
15 reduce : bool, |
|
16 rewrite : bool} |
14 |
17 |
15 type parameters = |
18 type parameters = |
16 {clause : Clause.parameters, |
19 {clause : Clause.parameters, |
17 prefactor : simplify, |
20 prefactor : simplify, |
18 postfactor : simplify} |
21 postfactor : simplify} |
25 |
28 |
26 val default : parameters |
29 val default : parameters |
27 |
30 |
28 val size : active -> int |
31 val size : active -> int |
29 |
32 |
30 val saturated : active -> Clause.clause list |
33 val saturation : active -> Clause.clause list |
31 |
34 |
32 (* ------------------------------------------------------------------------- *) |
35 (* ------------------------------------------------------------------------- *) |
33 (* Create a new active clause set and initialize clauses. *) |
36 (* Create a new active clause set and initialize clauses. *) |
34 (* ------------------------------------------------------------------------- *) |
37 (* ------------------------------------------------------------------------- *) |
35 |
38 |
36 val new : parameters -> Thm.thm list -> active * Clause.clause list |
39 val new : |
|
40 parameters -> {axioms : Thm.thm list, conjecture : Thm.thm list} -> |
|
41 active * {axioms : Clause.clause list, conjecture : Clause.clause list} |
37 |
42 |
38 (* ------------------------------------------------------------------------- *) |
43 (* ------------------------------------------------------------------------- *) |
39 (* Add a clause into the active set and deduce all consequences. *) |
44 (* Add a clause into the active set and deduce all consequences. *) |
40 (* ------------------------------------------------------------------------- *) |
45 (* ------------------------------------------------------------------------- *) |
41 |
46 |
43 |
48 |
44 (* ------------------------------------------------------------------------- *) |
49 (* ------------------------------------------------------------------------- *) |
45 (* Pretty printing. *) |
50 (* Pretty printing. *) |
46 (* ------------------------------------------------------------------------- *) |
51 (* ------------------------------------------------------------------------- *) |
47 |
52 |
48 val pp : active Parser.pp |
53 val pp : active Print.pp |
49 |
54 |
50 end |
55 end |