From d807d5e4fa129504669f775f4f832a1a7eb920a0 Mon Sep 17 00:00:00 2001 From: denes Date: Thu, 9 Jul 2009 12:03:59 +0000 Subject: [PATCH] Fixed check for condition iv p.33 (Riazzanov) --- .../ng_paramodulation/superposition.ml | 36 ++++++++++++------- 1 file changed, 23 insertions(+), 13 deletions(-) diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 86c77a7c0..1a5880434 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -103,7 +103,7 @@ module Superposition (B : Terms.Blob) = let build_clause bag filter rule t subst id id2 pos dir = let proof = Terms.Step(rule,id,id2,dir,pos,subst) in let t = Subst.apply_subst subst t in - if filter t then + if filter subst then let literal = match t with | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq -> @@ -655,18 +655,28 @@ module Superposition (B : Terms.Blob) = (all_positions [2] (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) l (superposition table vl)) - | Terms.Equation (l,r,ty,Terms.Incomparable) -> - fold_build_new_clause bag maxvar id Terms.Superposition - (function (* Riazanov: p.33 condition (iv) *) - | Terms.Node [Terms.Leaf eq; ty; l; r ] when B.eq B.eqP eq -> - Order.compare_terms l r <> Terms.Eq - | _ -> assert false) - ((all_positions [3] - (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) - r (superposition table vl)) @ - (all_positions [2] - (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) - l (superposition table vl))) + | Terms.Equation (l,r,ty,Terms.Incomparable) -> + let filtering avoid subst = (* Riazanov: p.33 condition (iv) *) + let l = Subst.apply_subst subst l in + let r = Subst.apply_subst subst r in + let o = Order.compare_terms l r in + o <> avoid && o <> Terms.Eq + in + let bag, maxvar,r_terms = + fold_build_new_clause bag maxvar id Terms.Superposition + (filtering Terms.Gt) + (all_positions [3] + (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) + r (superposition table vl)) + in + let bag, maxvar, l_terms = + fold_build_new_clause bag maxvar id Terms.Superposition + (filtering Terms.Lt) + (all_positions [2] + (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) + r (superposition table vl)) + in + bag, maxvar, r_terms @ l_terms | _ -> assert false ;; -- 2.39.2