From 87f1e71f269122c42c02971c82406767e3395ca5 Mon Sep 17 00:00:00 2001 From: denes Date: Wed, 22 Jul 2009 15:43:57 +0000 Subject: [PATCH] Fixed test for invertibility --- helm/software/components/ng_paramodulation/orderings.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml index 4c6e0a977..7743e3726 100644 --- a/helm/software/components/ng_paramodulation/orderings.ml +++ b/helm/software/components/ng_paramodulation/orderings.ml @@ -249,12 +249,14 @@ let relocate maxvar varlist subst = ;; let are_invertible l r = - let varlist = Terms.vars_of_term l in + let varlist = (Terms.vars_of_term l)@(Terms.vars_of_term r) 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 + let newl = FoSubst.apply_subst subst l in + let newr = FoSubst.apply_subst subst r in + try (let subst = alpha_eq l newr in eq_foterm newl (FoSubst.apply_subst subst r)) with UnificationFailure _ -> false +;; let compute_unit_clause_weight = compute_unit_clause_weight;; let compute_goal_weight = compute_goal_weight;; -- 2.39.2