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 f8e1d423153049358926583872708027b1453b22..89b390b07a11d3a9c4fc2f4f4f605c0eace95eac 100644 (file)
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -186,16 +186,27 @@ let compare_terms o x y =
       | _ -> 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 =
@@ -226,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;;
 
@@ -292,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;;