Invert dependencies between baseuris (files) are now stored in the db.

[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 23477be1a00d3d03b016d42520b69b6d8c7fa145..a89b13f5bbeb3e9f70c29e84f94dae5a0647623f 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -39,6 +39,7 @@ module Superposition (B : Terms.Blob) :
 
     val simplify : 
           Index.Index(B).DT.t ->
+          int ->
           B.t Terms.bag ->
           B.t Terms.unit_clause ->
             (B.t Terms.bag * B.t Terms.unit_clause) option
@@ -51,7 +52,20 @@ module Superposition (B : Terms.Blob) :
           B.t Terms.unit_clause ->
             B.t Terms.bag * B.t Terms.unit_clause
 
-  end
+    val one_pass_simplification:
+      B.t Terms.unit_clause ->
+      Index.Index(B).active_set ->
+      B.t Terms.bag ->
+      int ->
+      (B.t Terms.unit_clause * B.t Terms.bag * Index.Index(B).active_set) option
 
 
+    val keep_simplified:
+      B.t Terms.unit_clause ->
+      Index.Index(B).active_set ->
+      B.t Terms.bag ->
+      int ->
+      (B.t Terms.unit_clause * B.t Terms.bag * Index.Index(B).active_set) option
 
+
+  end