From 2d3494c5c68a48b663eed55c1ac55f3c8f832820 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 25 Mar 2010 08:36:02 +0000 Subject: [PATCH] Extension of demod to arbtrary predicates (not just equalities). From: asperti --- helm/software/components/ng_paramodulation/nCicProof.ml | 3 +-- helm/software/components/ng_paramodulation/paramod.ml | 8 +++++--- .../components/ng_paramodulation/superposition.ml | 7 ++++++- 3 files changed, 12 insertions(+), 6 deletions(-) diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml index df6f949b6..c5290694b 100644 --- a/helm/software/components/ng_paramodulation/nCicProof.ml +++ b/helm/software/components/ng_paramodulation/nCicProof.ml @@ -218,7 +218,6 @@ let debug c _ = c;; in aux ft (List.rev pl) ;; - (* we should better split forward and backward rewriting *) let mk_proof ?(demod=false) (bag : NCic.term Terms.bag) mp subst steps = let module NCicBlob = NCicBlob.NCicBlob( @@ -254,7 +253,7 @@ let debug c _ = c;; let get_literal id = let (_, lit, vl, proof),_,_ = Terms.get_from_bag id bag in let lit =match lit with - | Terms.Predicate t -> assert false + | Terms.Predicate t -> t (* assert false *) | Terms.Equation (l,r,ty,_) -> Terms.Node [ Terms.Leaf eqP(); ty; l; r] in diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 7fc13b504..86a964c14 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -567,10 +567,12 @@ module Paramod (B : Orderings.Blob) = struct let demod s goal = let bag,maxvar,actives,passives,g_actives,g_passives = s in let (bag,maxvar), g = mk_goal (bag,maxvar) goal in + let bag, ((i,_,_,_) as g1) = Sup.demodulate bag g (snd actives) in + if g1 = g then GaveUp else compute_result bag i [] +(* if Terms.is_eq_clause g then - let bag, ((i,_,_,_) as g1) = Sup.demodulate bag g (snd actives) in - if g1 = g then GaveUp else compute_result bag i [] - else GaveUp + + else GaveUp *) let fast_eq_check s goal = let (_,_,_,_,_,g_passives) as s = initialize_goal s goal in diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index c5bb640a2..42cf063b6 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -272,7 +272,12 @@ module Superposition (B : Orderings.Blob) = let rec demodulate bag (id, literal, vl, pr) table = debug (lazy ("demodulate " ^ (string_of_int id))); match literal with - | Terms.Predicate t -> assert false + | Terms.Predicate t -> (* assert false *) + let bag,_,id1 = + visit bag [] (fun x -> x) id t (ctx_demod table vl) + in + let cl,_,_ = Terms.get_from_bag id1 bag in + bag,cl | Terms.Equation (l,r,ty,_) -> let bag,l,id1 = visit bag [2] -- 2.39.2