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