One-side indexing for commutativity

diff --git a/helm/software/components/ng_paramodulation/foUnif.ml b/helm/software/components/ng_paramodulation/foUnif.ml
index cb3045c1918e9b0c9682e68c939440eb061d5c10..0946873b9af5c11fea237022b2394a40393e3de6 100644 (file)
--- a/helm/software/components/ng_paramodulation/foUnif.ml
+++ b/helm/software/components/ng_paramodulation/foUnif.ml
@@ -81,6 +81,7 @@ module Founif (B : Orderings.Blob) = struct
     subst
 ;;
 
+(* Sets of variables in s and t are assumed to be disjoint  *)
   let alpha_eq s t =
     let rec equiv subst s t =
       let s = match s with Terms.Var i -> Subst.lookup i subst | _ -> s
@@ -106,5 +107,6 @@ module Founif (B : Orderings.Blob) = struct
     in
       equiv Subst.id_subst s t
 ;;
+       
 
 end

diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml
index 889e1e7ef14955960fb1b88bbb7d8f40581ecf1c..5c085c5188db5a4473337995e167d17b290f5bfe 100644 (file)
--- a/helm/software/components/ng_paramodulation/index.ml
+++ b/helm/software/components/ng_paramodulation/index.ml
@@ -13,6 +13,8 @@
 
 module Index(B : Orderings.Blob) = struct
   module U = FoUtils.Utils(B)
+  module Unif = FoUnif.Founif(B)
+  module Pp = Pp.Pp(B)
 
   module ClauseOT =
     struct 
@@ -79,12 +81,23 @@ module Index(B : Orderings.Blob) = struct
       type dataset = ClauseSet.t
     = Make(FotermIndexable)(ClauseSet)
 
-  let index_unit_clause t = function
+  let are_invertible maxvar varlist l r =
+    let _,_,subst = U.relocate maxvar varlist FoSubst.id_subst in
+    let l = FoSubst.apply_subst subst l in
+      try (ignore(Unif.alpha_eq l r);true) with
+         FoUnif.UnificationFailure _ -> false
+  
+  let index_unit_clause maxvar t = function
     | (_,Terms.Equation (l,_,_,Terms.Gt),_,_) as c -> 
           DT.index t l (Terms.Left2Right, c)
     | (_,Terms.Equation (_,r,_,Terms.Lt),_,_) as c -> 
           DT.index t r (Terms.Right2Left, c)
-    | (_,Terms.Equation (l,r,_,Terms.Incomparable),_,_) as c ->  
+    | (_,Terms.Equation (l,r,_,Terms.Incomparable),vl,_) as c ->
+       if are_invertible maxvar vl l r then
+         (prerr_endline ("Invertible " ^ (Pp.pp_foterm l) ^ "=" ^
+            (Pp.pp_foterm r));
+           DT.index t l (Terms.Left2Right, c))
+          else
           DT.index  
            (DT.index t l (Terms.Left2Right, c))
            r (Terms.Right2Left, c)

diff --git a/helm/software/components/ng_paramodulation/index.mli b/helm/software/components/ng_paramodulation/index.mli
index 7d75f28370d00eb487764e4e8d87cd5b18c40f33..bfed8d533e73dfc9d315c7188d6ae6595154697a 100644 (file)
--- a/helm/software/components/ng_paramodulation/index.mli
+++ b/helm/software/components/ng_paramodulation/index.mli
@@ -27,7 +27,7 @@ module Index (B : Orderings.Blob) :
       type dataset = ClauseSet.t
     
     val index_unit_clause :
-          DT.t -> B.t Terms.unit_clause -> DT.t 
+          int -> DT.t -> B.t Terms.unit_clause -> DT.t 
 
     type active_set = B.t Terms.unit_clause list * DT.t
 

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 182545b1edda93968fb00915f5a5c01f662da8da..4ca5a62d3ad2945667606a5c8716022a0a3e9267 100644 (file)
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -284,6 +284,7 @@ module KBO (B : Terms.Blob) = struct
         let r = aux t1 t2 in
         if r = XEQ then (
           match t1, t2 with
+         | Terms.Var i, Terms.Var j when i=j -> XEQ
           | Terms.Node (_::tl1), Terms.Node (_::tl2) -> cmp tl1 tl2
           | _, _ ->  XINCOMPARABLE
         ) else r 

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 3491f40196f9a21d8c522d564a49554a1b71be63..06d3251f77125e87c52a19e6cad9ac7e927ff174 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -199,7 +199,7 @@ module Paramod (B : Orderings.Blob) = struct
                | Some (bag,c1) -> bag,if c==c1 then c::acc else c::c1::acc)
           (bag,[]) g_actives 
       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, maxvar, new_goals = 
         List.fold_left 
           (fun (bag,m,acc) g -> 
@@ -314,7 +314,7 @@ module Paramod (B : Orderings.Blob) = struct
                   if noinfer then
                     let actives = 
                       current::fst actives,
-                      IDX.index_unit_clause (snd actives) current
+                      IDX.index_unit_clause maxvar (snd actives) current
                     in
                     bag,maxvar,actives,passives,g_actives,g_passives
                   else

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