]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_paramodulation/superposition.mli
New functorialization: paramod is abstracted over a Orderings.Blob, that is like...
[helm.git] / helm / software / components / ng_paramodulation / superposition.mli
index d7efb1b42b8921d4bb225575cc5bab1aea7639a9..30d32d540a330d8bdb9495b086a134e0fffd5391 100644 (file)
@@ -11,7 +11,7 @@
 
 (* $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 *)
@@ -39,23 +39,41 @@ module Superposition (B : Terms.Blob) :
 
     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 simplify_goal : 
+    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
+
+    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 ->
-      (B.t Terms.unit_clause * B.t Terms.bag * Index.Index(B).active_set) option
+      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