1) added simplification of actives w.r.t. selected

[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 adfaf68e299d539776cac2a6cddc8d966036af49..5878918c2b37d60c1a8b8a4b63758d927882b229 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -11,18 +11,45 @@
 
 (* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *)
 
-
 module Superposition (B : Terms.Blob) : 
   sig
 
+    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
 
+    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 ->
+            (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