Now iterating superposition

[helm.git] / helm / software / components / ng_paramodulation / clauses.mli

diff --git a/helm/software/components/ng_paramodulation/clauses.mli b/helm/software/components/ng_paramodulation/clauses.mli
index 885e97607077dcca3b682a9a34316a57692453d4..b857eb01629d5f0ceda19eb4d375a748d881b789 100644 (file)
--- a/helm/software/components/ng_paramodulation/clauses.mli
+++ b/helm/software/components/ng_paramodulation/clauses.mli
@@ -22,7 +22,9 @@ module Clauses (B : Orderings.Blob) :
 
     val eq_clause : B.t Terms.clause -> B.t Terms.clause -> bool
     val compare_clause : B.t Terms.clause -> B.t Terms.clause -> int      
-    val fresh_clause : int -> B.t Terms.clause -> B.t Terms.clause * int
+    val fresh_clause : int ->
+         ?subst: B.t Terms.substitution ->
+         B.t Terms.clause -> B.t Terms.clause * int
 
     val mk_clause : int -> B.t Terms.foterm list -> B.t Terms.foterm list
                            -> B.t Terms.foterm -> B.t Terms.clause * int
@@ -37,4 +39,13 @@ module Clauses (B : Orderings.Blob) :
     val compare_passive_clauses_age :
            int * B.t Terms.clause -> int * B.t Terms.clause -> int
 
+    val are_alpha_eq_cl :
+           B.t Terms.clause -> B.t Terms.clause -> bool
+
+    val vars_of_clause :
+           B.t Terms.clause -> int list
+
+    (*val apply_subst :
+          B.t Terms.substitution -> B.t Terms.clause -> B.t Terms.clause*)
+
 end