almost complete superposition right step

[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 b67233563591d624f42bdaba3e1a2564f6b61e54..54b5ae50f322a031bc926de684e25539c9ec7204 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -15,12 +15,13 @@
 module Superposition (B : Terms.Blob) : 
   sig
 
-    val superposition_right_with_table :
+    (* The returned active set is the input one + the selected clause *)
+    val superposition_right :
           B.t Terms.bag -> 
           int -> (* maxvar *)
-          B.t Terms.unit_clause ->
-          Index.Index(B).DT.t ->
-            B.t Terms.bag * int * B.t Terms.unit_clause list
+          B.t Terms.unit_clause -> (* selected *)
+          Index.Index(B).active_set ->
+            B.t Terms.bag * int * Index.Index(B).active_set * B.t Terms.unit_clause list
                   
   end