Reorganized foUtils, added Clauses module to avoid duplicate code around are_invertib...

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

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index f2151528f698df8472f17c2d608bb2e03a5729ed..89b390b07a11d3a9c4fc2f4f4f605c0eace95eac 100644 (file)
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -11,7 +11,7 @@
 
 (* $Id$ *)
 
-type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE
+type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE | XINVERTIBLE
 
 module type Blob =
   sig 
@@ -88,14 +88,15 @@ let compute_literal_weight l =
         let w, m = weight_of_term x in 
         weight_of_polynomial w m
     | Terms.Equation (l,r,_,Terms.Eq) 
-    | Terms.Equation (l,r,_,Terms.Incomparable) ->
+    | Terms.Equation (l,r,_,Terms.Incomparable) 
+    | Terms.Equation (l,r,_,Terms.Invertible) ->
         let wl, ml = weight_of_term l in 
         let wr, mr = weight_of_term r in 
         weight_of_polynomial (wl+wr) (ml@mr)
 ;;
 
 let compute_clause_weight (_,nl,pl,_,_) =
-  List.fold_left (fun acc lit -> compute_literal_weight lit + acc) 0 (nl@pl)
+  List.fold_left (fun acc (lit,_) -> compute_literal_weight lit + acc) 0 (nl@pl)
 
 let compute_goal_weight = compute_clause_weight;;
   
@@ -181,19 +182,31 @@ let compare_terms o x y =
       | XGT -> Terms.Gt
       | XLT -> Terms.Lt
       | XEQ -> Terms.Eq
+      | XINVERTIBLE -> Terms.Invertible
       | _ -> assert false
 ;;
 
+let are_invertible relocate alpha_eq l r =
+    let varlist = Terms.vars_of_term l in
+    let maxvar = List.fold_left max 0 varlist in
+    let _,_,subst = relocate maxvar varlist FoSubst.id_subst in
+    let l = FoSubst.apply_subst subst l in
+      try (ignore(alpha_eq l r);true) with
+         FoUnif.UnificationFailure _ -> false;;
+
 module NRKBO (B : Terms.Blob) = struct
   let name = "nrkbo"
   include B 
 
   module Pp = Pp.Pp(B)
+  module Unif = FoUnif.FoUnif(B)
+  module Utils = FoUtils.Utils(B)
 
   let eq_foterm = eq_foterm B.eq;;
 
+  let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
+
   let compute_clause_weight = compute_clause_weight;;
-  let compute_goal_weight = compute_goal_weight;;
   
   (* Riazanov: p. 40, relation >_n *)
   let nonrec_kbo t1 t2 =
@@ -204,7 +217,9 @@ module NRKBO (B : Terms.Blob) = struct
         if aux_ordering B.compare t1 t2 = XLT then XLT else XINCOMPARABLE
     | XGE -> 
         if aux_ordering B.compare t1 t2 = XGT then XGT else XINCOMPARABLE
-    | XEQ -> aux_ordering B.compare t1 t2
+    | XEQ -> let res = aux_ordering B.compare t1 t2 in
+       if res = XINCOMPARABLE && are_invertible t1 t2 then XINVERTIBLE
+       else res
     | res -> res
   ;;
 
@@ -222,9 +237,13 @@ module KBO (B : Terms.Blob) = struct
   include B 
 
   module Pp = Pp.Pp(B)
+  module Unif = FoUnif.FoUnif(B)
+  module Utils = FoUtils.Utils(B)
 
   let eq_foterm = eq_foterm B.eq;;
 
+  let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
+
   let compute_clause_weight = compute_clause_weight;;
   let compute_goal_weight = compute_goal_weight;;
 
@@ -267,6 +286,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 
@@ -287,9 +307,13 @@ module LPO (B : Terms.Blob) = struct
   include B 
 
   module Pp = Pp.Pp(B)
+  module Unif = FoUnif.FoUnif(B)
+  module Utils = FoUtils.Utils(B)
 
   let eq_foterm = eq_foterm B.eq;;
 
+  let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
+
   let compute_clause_weight = compute_clause_weight;;
   let compute_goal_weight = compute_goal_weight;;