X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.mli;h=5878918c2b37d60c1a8b8a4b63758d927882b229;hb=a14157957532b731330492388ab32909b4147758;hp=c2c0ef43d0603be7c520331ffbd76fa80aae0f93;hpb=6b0a195b180e3526af7b55771b2df7b10acd7c30;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli
index c2c0ef43d..5878918c2 100644
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -11,16 +11,45 @@
 
 (* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *)
 
-
 module Superposition (B : Terms.Blob) : 
   sig
 
-    val superposition_right_step :
+    exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
+
+    (* The returned active set is the input one + the selected clause *)
+    val infer_right :
+          B.t Terms.bag -> 
+          int -> (* maxvar *)
+          B.t Terms.unit_clause -> (* selected passive *)
+          Index.Index(B).active_set ->
+            B.t Terms.bag * int * Index.Index(B).active_set * B.t Terms.unit_clause list
+
+    val infer_left :  
           B.t Terms.bag -> 
+          int -> (* maxvar *)
+          B.t Terms.unit_clause -> (* selected goal *)
+          Index.Index(B).active_set ->
+            B.t Terms.bag * int * B.t Terms.unit_clause list
+
+    val demodulate : 
+          B.t Terms.bag ->
           B.t Terms.unit_clause ->
+          Index.Index(B).DT.t -> B.t Terms.bag * B.t Terms.unit_clause
+
+    val forward_simplify : 
           Index.Index(B).DT.t ->
-            B.t Terms.bag * B.t Terms.unit_clause list
-                  
+          B.t Terms.bag ->
+          B.t Terms.unit_clause ->
+            (B.t Terms.bag * B.t Terms.unit_clause) option
+
+    (* may raise success *)
+    val backward_simplify : 
+          int ->
+          Index.Index(B).DT.t ->
+          B.t Terms.bag ->
+          B.t Terms.unit_clause ->
+            B.t Terms.bag * B.t Terms.unit_clause
+
   end