X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.mli;h=e3e2f8b9f2f6f15d12c791a4351309f022139ccd;hb=2c2b31c242aa81dc6f3c73e7e2a3ec0789a21edd;hp=adfaf68e299d539776cac2a6cddc8d966036af49;hpb=a99b3bf44964a6a3d56d752efbdc2c962ce24d08;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli
index adfaf68e2..e3e2f8b9f 100644
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -11,19 +11,62 @@
 
 (* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *)
 
-
 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 *)
     val infer_right :
           B.t Terms.bag -> 
           int -> (* maxvar *)
-          B.t Terms.unit_clause -> (* selected *)
+          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
 
-  end
+    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 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)
 
+    (* 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) 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
+
+
+    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