Trying to be faster

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

diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli
index 30d32d540a330d8bdb9495b086a134e0fffd5391..c67dbfb07dbbc13b3297d0b8903305a9680cf588 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -15,7 +15,11 @@ module Superposition (B : Orderings.Blob) :
   sig
 
                         (* bag, maxvar, meeting point *)
-    exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
+    exception Success of 
+      B.t Terms.bag 
+      * int 
+      * B.t Terms.unit_clause
+      * B.t Terms.substitution
 
     (* The returned active set is the input one + the selected clause *)
     val infer_right :
@@ -60,8 +64,6 @@ module Superposition (B : Orderings.Blob) :
       B.t Terms.bag ->
       int ->
       B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option
-
-
     val keep_simplified:
       B.t Terms.unit_clause ->
       Index.Index(B).active_set ->
@@ -75,5 +77,8 @@ module Superposition (B : Orderings.Blob) :
       B.t Terms.unit_clause ->
       bool
 
-
+    val are_alpha_eq : 
+      B.t Terms.unit_clause ->
+      B.t Terms.unit_clause ->
+      bool
   end