X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.mli;h=149bbb0486f76726169f207cf3d4d13ae8455b46;hb=2f77bd6071bd316ed0a91448f4c04e638f853442;hp=cce81944bd497d286b50c22c31d4055c3c4e5228;hpb=4ae7d510a430a2a6929f973d36b993d528772d64;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli
index cce81944b..149bbb048 100644
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -37,21 +37,43 @@ 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
 
-  end
+    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
 
 
+    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
 
+    val  orphan_murder:
+      B.t Terms.bag ->
+      B.t Terms.unit_clause list ->
+      B.t Terms.unit_clause ->
+      bool
+
+
+  end