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