Implemented orphan murder test (clauses are not discarded for now)

[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 a89b13f5bbeb3e9f70c29e84f94dae5a0647623f..a7badaba4a5bb32769af0cc4f7bad2322fda7f4b 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -42,22 +42,23 @@ module Superposition (B : Terms.Blob) :
           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 simplify_goal : 
           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.unit_clause * B.t Terms.bag * Index.Index(B).active_set) option
+      B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option
 
 
     val keep_simplified:
@@ -65,7 +66,7 @@ module Superposition (B : Terms.Blob) :
       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
+      B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option
 
 
   end