From 0590a3073dae55f31e79c71e3ed2a4d66a851a0d Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 9 Dec 2009 15:47:38 +0000 Subject: [PATCH] Minor fixing for last chance --- .../components/ng_paramodulation/superposition.ml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 6a2950b0e..fad0a12d2 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -342,7 +342,6 @@ module Superposition (B : Orderings.Blob) = in bag, maxvar, res ;; - let rewrite_eq ~unify l r ty vl table = let retrieve = if unify then IDX.DT.retrieve_unifiables @@ -613,7 +612,10 @@ module Superposition (B : Orderings.Blob) = then raise (Success (bag, maxvar, clause)) else let (id,lit,vl,_) = clause in - if vl = [] then Some (bag,clause) + (* this optimization makes sense only if we demodulated, since in + that case the clause should have been turned into an identity *) + if (vl = [] && not(no_demod)) + then Some (bag,clause) else let l,r,ty = match lit with @@ -624,15 +626,15 @@ module Superposition (B : Orderings.Blob) = table (Some(bag,maxvar,clause,Subst.id_subst)) with | None -> Some (bag,clause) | Some (bag,maxvar,cl,subst) -> - prerr_endline "Goal subsumed"; - raise (Success (bag,maxvar,cl)) + debug (lazy "Goal subsumed"); + raise (Success (bag,maxvar,cl))) (* - else match is_subsumed ~unify:true bag maxvar clause table with + match is_subsumed ~unify:true bag maxvar clause table with | None -> Some (bag, clause) | Some ((bag,maxvar),c) -> prerr_endline "Goal subsumed"; raise (Success (bag,maxvar,c)) -*) +*) ;; let prof_simplify_goal = HExtlib.profile ~enable "simplify_goal";; -- 2.39.2