|
1 (* ========================================================================= *) |
|
2 (* SUBSUMPTION CHECKING FOR FIRST ORDER LOGIC CLAUSES *) |
|
3 (* Copyright (c) 2002-2006 Joe Hurd, distributed under the GNU GPL version 2 *) |
|
4 (* ========================================================================= *) |
|
5 |
|
6 signature Subsume = |
|
7 sig |
|
8 |
|
9 (* ------------------------------------------------------------------------- *) |
|
10 (* A type of clause sets that supports efficient subsumption checking. *) |
|
11 (* ------------------------------------------------------------------------- *) |
|
12 |
|
13 type 'a subsume |
|
14 |
|
15 val new : unit -> 'a subsume |
|
16 |
|
17 val size : 'a subsume -> int |
|
18 |
|
19 val insert : 'a subsume -> Thm.clause * 'a -> 'a subsume |
|
20 |
|
21 val filter : ('a -> bool) -> 'a subsume -> 'a subsume |
|
22 |
|
23 val pp : 'a subsume Print.pp |
|
24 |
|
25 val toString : 'a subsume -> string |
|
26 |
|
27 (* ------------------------------------------------------------------------- *) |
|
28 (* Subsumption checking. *) |
|
29 (* ------------------------------------------------------------------------- *) |
|
30 |
|
31 val subsumes : |
|
32 (Thm.clause * Subst.subst * 'a -> bool) -> 'a subsume -> Thm.clause -> |
|
33 (Thm.clause * Subst.subst * 'a) option |
|
34 |
|
35 val isSubsumed : 'a subsume -> Thm.clause -> bool |
|
36 |
|
37 val strictlySubsumes : (* exclude subsuming clauses with more literals *) |
|
38 (Thm.clause * Subst.subst * 'a -> bool) -> 'a subsume -> Thm.clause -> |
|
39 (Thm.clause * Subst.subst * 'a) option |
|
40 |
|
41 val isStrictlySubsumed : 'a subsume -> Thm.clause -> bool |
|
42 |
|
43 (* ------------------------------------------------------------------------- *) |
|
44 (* Single clause versions. *) |
|
45 (* ------------------------------------------------------------------------- *) |
|
46 |
|
47 val clauseSubsumes : Thm.clause -> Thm.clause -> Subst.subst option |
|
48 |
|
49 val clauseStrictlySubsumes : Thm.clause -> Thm.clause -> Subst.subst option |
|
50 |
|
51 end |