Branched paramodulation for CNF (Horn clauses)

[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 30d32d540a330d8bdb9495b086a134e0fffd5391..ad780c82c1e1f3fc645cc6a193b59886d2401dbc 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -15,34 +15,34 @@ 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.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 *)
+          B.t Terms.clause -> (* selected passive *)
           Index.Index(B).active_set ->
-            B.t Terms.bag * int * Index.Index(B).active_set * B.t Terms.unit_clause list
+            B.t Terms.bag * int * Index.Index(B).active_set * B.t Terms.clause list
 
     val infer_left :  
           B.t Terms.bag -> 
           int -> (* maxvar *)
-          B.t Terms.unit_clause -> (* selected goal *)
+          B.t Terms.clause -> (* selected goal *)
           Index.Index(B).active_set ->
-            B.t Terms.bag * int * B.t Terms.unit_clause list
+            B.t Terms.bag * int * B.t Terms.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
+          B.t Terms.clause ->
+          Index.Index(B).DT.t -> B.t Terms.bag * B.t Terms.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)
+          B.t Terms.clause ->
+            B.t Terms.bag * (B.t Terms.clause option)
 
     (* may raise success *)
     val simplify_goal :
@@ -50,29 +50,29 @@ module Superposition (B : Orderings.Blob) :
           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
+          B.t Terms.clause list ->
+          B.t Terms.clause ->
+            (B.t Terms.bag * B.t Terms.clause) option
 
     val one_pass_simplification:
-      B.t Terms.unit_clause ->
+      B.t Terms.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
+      B.t Terms.bag * (B.t Terms.clause * Index.Index(B).active_set) option
 
 
     val keep_simplified:
-      B.t Terms.unit_clause ->
+      B.t Terms.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
+      B.t Terms.bag * (B.t Terms.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 ->
+      B.t Terms.clause list ->
+      B.t Terms.clause ->
       bool