--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Subsume.sig Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,51 @@
+(* ========================================================================= *)
+(* SUBSUMPTION CHECKING FOR FIRST ORDER LOGIC CLAUSES *)
+(* Copyright (c) 2002-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Subsume =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of clause sets that supports efficient subsumption checking. *)
+(* ------------------------------------------------------------------------- *)
+
+type 'a subsume
+
+val new : unit -> 'a subsume
+
+val size : 'a subsume -> int
+
+val insert : 'a subsume -> Thm.clause * 'a -> 'a subsume
+
+val filter : ('a -> bool) -> 'a subsume -> 'a subsume
+
+val pp : 'a subsume Print.pp
+
+val toString : 'a subsume -> string
+
+(* ------------------------------------------------------------------------- *)
+(* Subsumption checking. *)
+(* ------------------------------------------------------------------------- *)
+
+val subsumes :
+ (Thm.clause * Subst.subst * 'a -> bool) -> 'a subsume -> Thm.clause ->
+ (Thm.clause * Subst.subst * 'a) option
+
+val isSubsumed : 'a subsume -> Thm.clause -> bool
+
+val strictlySubsumes : (* exclude subsuming clauses with more literals *)
+ (Thm.clause * Subst.subst * 'a -> bool) -> 'a subsume -> Thm.clause ->
+ (Thm.clause * Subst.subst * 'a) option
+
+val isStrictlySubsumed : 'a subsume -> Thm.clause -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Single clause versions. *)
+(* ------------------------------------------------------------------------- *)
+
+val clauseSubsumes : Thm.clause -> Thm.clause -> Subst.subst option
+
+val clauseStrictlySubsumes : Thm.clause -> Thm.clause -> Subst.subst option
+
+end