X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.mli;h=c67dbfb07dbbc13b3297d0b8903305a9680cf588;hb=9c21f4a9a35415878189aca003847cbd42c1a9fc;hp=a7badaba4a5bb32769af0cc4f7bad2322fda7f4b;hpb=2701c980f48541dd5e8317b5a5661b439ced8b29;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli
index a7badaba4..c67dbfb07 100644
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -11,11 +11,15 @@
 
 (* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *)
 
-module Superposition (B : Terms.Blob) : 
+module Superposition (B : Orderings.Blob) : 
   sig
 
                         (* bag, maxvar, meeting point *)
-    exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
+    exception Success of 
+      B.t Terms.bag 
+      * int 
+      * B.t Terms.unit_clause
+      * B.t Terms.substitution
 
     (* The returned active set is the input one + the selected clause *)
     val infer_right :
@@ -45,7 +49,8 @@ module Superposition (B : Terms.Blob) :
             B.t Terms.bag * (B.t Terms.unit_clause option)
 
     (* may raise success *)
-    val simplify_goal : 
+    val simplify_goal :
+          no_demod:bool ->
           int ->
           Index.Index(B).DT.t ->
           B.t Terms.bag ->
@@ -59,8 +64,6 @@ module Superposition (B : Terms.Blob) :
       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 ->
@@ -68,5 +71,14 @@ module Superposition (B : Terms.Blob) :
       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
 
+    val are_alpha_eq : 
+      B.t Terms.unit_clause ->
+      B.t Terms.unit_clause ->
+      bool
   end