From 8e4367191fdfd125596658e35d4b99cd3047a5bc Mon Sep 17 00:00:00 2001 From: denes Date: Wed, 22 Jul 2009 13:14:51 +0000 Subject: [PATCH] Fixes --- .../components/ng_paramodulation/index.ml | 1 + .../components/ng_paramodulation/orderings.ml | 46 ++++++++++++++++++- 2 files changed, 46 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml index 633c32854..beb3aed86 100644 --- a/helm/software/components/ng_paramodulation/index.ml +++ b/helm/software/components/ng_paramodulation/index.ml @@ -86,6 +86,7 @@ module Index(B : Orderings.Blob) = struct = Make(FotermIndexable)(ClauseSet) let index_literal t c is_pos pos = function + | Terms.Equation (l,_,_,Terms.Invertible) | Terms.Equation (l,_,_,Terms.Gt) -> DT.index t l (Terms.Left2Right,is_pos,pos,c) | Terms.Equation (_,r,_,Terms.Lt) -> diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml index f8e1d4231..47f6b4512 100644 --- a/helm/software/components/ng_paramodulation/orderings.ml +++ b/helm/software/components/ng_paramodulation/orderings.ml @@ -194,8 +194,52 @@ module NRKBO (B : Terms.Blob) = struct let eq_foterm = eq_foterm B.eq;; +exception UnificationFailure of string Lazy.t;; + + +(* DUPLICATE CODE FOR TESTS (see FoUnif) *) + let alpha_eq s t = + let rec equiv subst s t = + let s = match s with Terms.Var i -> FoSubst.lookup i subst | _ -> s + and t = match t with Terms.Var i -> FoSubst.lookup i subst | _ -> t + + in + match s, t with + | s, t when eq_foterm s t -> subst + | Terms.Var i, Terms.Var j + when (not (List.exists (fun (_,k) -> k=t) subst)) -> + let subst = FoSubst.build_subst i t subst in + subst + | Terms.Node l1, Terms.Node l2 -> ( + try + List.fold_left2 + (fun subst' s t -> equiv subst' s t) + subst l1 l2 + with Invalid_argument _ -> + raise (UnificationFailure (lazy "Inference.unification.unif")) + ) + | _, _ -> + raise (UnificationFailure (lazy "Inference.unification.unif")) + in + equiv FoSubst.id_subst s t +;; + +let relocate maxvar varlist subst = + List.fold_right + (fun i (maxvar, varlist, s) -> + maxvar+1, maxvar::varlist, FoSubst.build_subst i (Terms.Var maxvar) s) + varlist (maxvar+1, [], subst) + ;; + + let are_invertible 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 + UnificationFailure _ -> false + let compute_clause_weight = compute_clause_weight;; - let compute_goal_weight = compute_goal_weight;; (* Riazanov: p. 40, relation >_n *) let nonrec_kbo t1 t2 = -- 2.39.2