Branched paramodulation for CNF (Horn clauses)

[helm.git] / helm / software / components / ng_paramodulation / superposition.ml

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 0a7c5cfcc1c82fdb0be718e4ddde26bca391d876..54f7e10466a2a3550d7c08fc50cead3246b60ba4 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -20,7 +20,7 @@ module Superposition (B : Orderings.Blob) =
     module Utils = FoUtils.Utils(B)
     module Pp = Pp.Pp(B)
     
-    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
 
     let debug s = prerr_endline s;;
     let debug _ = ();;
@@ -165,7 +165,7 @@ module Superposition (B : Orderings.Blob) =
                      ((*prerr_endline ("Filtering: " ^ 
                         Pp.pp_foterm side ^ " =(< || =)" ^ 
                         Pp.pp_foterm newside ^ " coming from " ^ 
-                        Pp.pp_unit_clause uc );*)None)
+                        Pp.pp_clause uc );*)None)
                  else
                    Some (newside, subst, id, dir)
                with FoUnif.UnificationFailure _ -> None)
@@ -273,8 +273,8 @@ module Superposition (B : Orderings.Blob) =
 (*      in
         if are_alpha_eq c1 c2 then bag1,c1
         else begin
-          prerr_endline (Pp.pp_unit_clause c1);
-          prerr_endline (Pp.pp_unit_clause c2);
+          prerr_endline (Pp.pp_clause c1);
+          prerr_endline (Pp.pp_clause c2);
           prerr_endline "Bag :";
           prerr_endline (Pp.pp_bag bag1);
           assert false
@@ -481,7 +481,7 @@ module Superposition (B : Orderings.Blob) =
       match simplify atable maxvar bag new_clause with
         | bag,None -> bag,None (* new_clause has been discarded *)
         | bag,(Some clause) ->
-            let ctable = IDX.index_unit_clause IDX.DT.empty clause in
+            let ctable = IDX.index_clause IDX.DT.empty clause in
             let bag, alist, atable = 
               List.fold_left 
                 (fun (bag, alist, atable) c ->
@@ -489,7 +489,7 @@ module Superposition (B : Orderings.Blob) =
                      |bag,None -> (bag,alist,atable)
                         (* an active clause as been discarded *)
                      |bag,Some c1 ->
-                        bag, c :: alist, IDX.index_unit_clause atable c)
+                        bag, c :: alist, IDX.index_clause atable c)
                 (bag,[],IDX.DT.empty) alist
             in
               bag, Some (clause, (alist,atable))
@@ -502,7 +502,7 @@ module Superposition (B : Orderings.Blob) =
     let simplification_step ~new_cl cl (alist,atable) bag maxvar new_clause =
       let atable1 =
         if new_cl then atable else
-        IDX.index_unit_clause atable cl
+        IDX.index_clause atable cl
       in
         (* Simplification of new_clause with :      *
          * - actives and cl if new_clause is not cl *
@@ -513,7 +513,7 @@ module Superposition (B : Orderings.Blob) =
           | bag,Some clause ->
               (* Simplification of each active clause with clause *
                * which is the simplified form of new_clause       *)
-              let ctable = IDX.index_unit_clause IDX.DT.empty clause in
+              let ctable = IDX.index_clause IDX.DT.empty clause in
               let bag, newa, alist, atable = 
                 List.fold_left 
                   (fun (bag, newa, alist, atable) c ->
@@ -523,7 +523,7 @@ module Superposition (B : Orderings.Blob) =
                        |bag,Some c1 ->
                             if (c1 == c) then 
                               bag, newa, c :: alist,
-                            IDX.index_unit_clause atable c
+                            IDX.index_clause atable c
                             else
                               bag, c1 :: newa, alist, atable)                  
                   (bag,[],[],IDX.DT.empty) alist
@@ -565,7 +565,7 @@ module Superposition (B : Orderings.Blob) =
                   | bag,(None, Some _) -> bag,None
                   | bag,(Some cl1, Some (clause, (alist,atable), newa)) ->
                       let alist,atable =
-                        (clause::alist, IDX.index_unit_clause atable clause)
+                        (clause::alist, IDX.index_clause atable clause)
                       in
                         keep_simplified_aux ~new_cl:(cl!=cl1) cl1 (alist,atable)
                           bag (newa@tl)
@@ -693,12 +693,12 @@ module Superposition (B : Orderings.Blob) =
       (* We demodulate actives clause with current until all *
        * active clauses are reduced w.r.t each other         *)
       (* let bag, (alist,atable) = keep_simplified (alist,atable) bag [current] in *)
-      let ctable = IDX.index_unit_clause IDX.DT.empty current in
+      let ctable = IDX.index_clause IDX.DT.empty current in
       (* let bag, (alist, atable) = 
         let bag, alist = 
           HExtlib.filter_map_acc (simplify ctable) bag alist
         in
-        bag, (alist, List.fold_left IDX.index_unit_clause IDX.DT.empty alist)
+        bag, (alist, List.fold_left IDX.index_clause IDX.DT.empty alist)
       in*)
         debug "Simplified active clauses with fact";
       (* We superpose active clauses with current *)
@@ -715,10 +715,10 @@ module Superposition (B : Orderings.Blob) =
         (* We add current to active clauses so that it can be *
          * superposed with itself                             *)
       let alist, atable = 
-        current :: alist, IDX.index_unit_clause atable current
+        current :: alist, IDX.index_clause atable current
       in
         debug "Indexed";
-      let fresh_current, maxvar = Utils.fresh_unit_clause maxvar current in
+      let fresh_current, maxvar = Utils.fresh_clause maxvar current in
         (* We need to put fresh_current into the bag so that all *
          * variables clauses refer to are known.                 *)
       let bag, fresh_current = Terms.add_to_bag fresh_current bag in