One-side indexing for commutativity

[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 dd394ce675450f1a6b3083c875d3c7dd20907664..27361859bffbfb6e5f2e7d192d1c84d0ce1082b4 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -482,7 +482,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_unit_clause maxvar IDX.DT.empty clause in
             let bag, alist, atable = 
               List.fold_left 
                 (fun (bag, alist, atable) c ->
@@ -490,7 +490,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_unit_clause maxvar atable c)
                 (bag,[],IDX.DT.empty) alist
             in
               bag, Some (clause, (alist,atable))
@@ -503,7 +503,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_unit_clause maxvar atable cl
       in
         (* Simplification of new_clause with :      *
          * - actives and cl if new_clause is not cl *
@@ -514,7 +514,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_unit_clause maxvar IDX.DT.empty clause in
               let bag, newa, alist, atable = 
                 List.fold_left 
                   (fun (bag, newa, alist, atable) c ->
@@ -524,7 +524,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_unit_clause maxvar atable c
                             else
                               bag, c1 :: newa, alist, atable)                  
                   (bag,[],[],IDX.DT.empty) alist
@@ -566,7 +566,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_unit_clause maxvar atable clause)
                       in
                         keep_simplified_aux ~new_cl:(cl!=cl1) cl1 (alist,atable)
                           bag (newa@tl)
@@ -694,7 +694,7 @@ 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_unit_clause maxvar IDX.DT.empty current in
       (* let bag, (alist, atable) = 
         let bag, alist = 
           HExtlib.filter_map_acc (simplify ctable) bag alist
@@ -716,7 +716,7 @@ 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_unit_clause maxvar atable current
       in
         debug "Indexed";
       let fresh_current, maxvar = Utils.fresh_unit_clause maxvar current in