attempt to run a last chance procedure after the timeout

[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 5878918c2b37d60c1a8b8a4b63758d927882b229..52011c3e806893d3ca2a8854ce135454ea8586a3 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -14,6 +14,7 @@
 module Superposition (B : Terms.Blob) : 
   sig
 
+                        (* bag, maxvar, meeting point *)
     exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
 
     (* The returned active set is the input one + the selected clause *)
@@ -36,21 +37,37 @@ module Superposition (B : Terms.Blob) :
           B.t Terms.unit_clause ->
           Index.Index(B).DT.t -> B.t Terms.bag * B.t Terms.unit_clause
 
-    val forward_simplify : 
+    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
+            B.t Terms.bag * (B.t Terms.unit_clause option)
 
     (* may raise success *)
-    val backward_simplify : 
+    val simplify_goal :
+          no_demod:bool ->
           int ->
           Index.Index(B).DT.t ->
           B.t Terms.bag ->
+          B.t Terms.unit_clause list ->
           B.t Terms.unit_clause ->
-            B.t Terms.bag * B.t Terms.unit_clause
+            (B.t Terms.bag * B.t Terms.unit_clause) option
+
+    val one_pass_simplification:
+      B.t Terms.unit_clause ->
+      Index.Index(B).active_set ->
+      B.t Terms.bag ->
+      int ->
+      B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option
 
-  end
 
+    val keep_simplified:
+      B.t Terms.unit_clause ->
+      Index.Index(B).active_set ->
+      B.t Terms.bag ->
+      int ->
+      B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option
 
 
+  end