From: denes Date: Fri, 31 Jul 2009 17:18:30 +0000 (+0000) Subject: Fixed nasty bug in superposition and freshing of clauses X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f2039f5c9e68dc69c86c77758bc521acd30e973f;p=helm.git Fixed nasty bug in superposition and freshing of clauses --- diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend index 489a80a1a..8ffa24a0f 100644 --- a/helm/software/components/ng_paramodulation/.depend +++ b/helm/software/components/ng_paramodulation/.depend @@ -3,7 +3,7 @@ foSubst.cmi: terms.cmi foUtils.cmi: terms.cmi foUnif.cmi: terms.cmi orderings.cmi: terms.cmi -clauses.cmi: orderings.cmi +clauses.cmi: terms.cmi orderings.cmi index.cmi: terms.cmi orderings.cmi superposition.cmi: terms.cmi orderings.cmi index.cmi stats.cmi: terms.cmi orderings.cmi @@ -21,22 +21,26 @@ foUtils.cmo: terms.cmi foSubst.cmi foUtils.cmi foUtils.cmx: terms.cmx foSubst.cmx foUtils.cmi foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi -orderings.cmo: terms.cmi pp.cmi foUnif.cmi foSubst.cmi orderings.cmi -orderings.cmx: terms.cmx pp.cmx foUnif.cmx foSubst.cmx orderings.cmi -clauses.cmo: terms.cmi orderings.cmi foUtils.cmi foSubst.cmi clauses.cmi -clauses.cmx: terms.cmx orderings.cmx foUtils.cmx foSubst.cmx clauses.cmi -index.cmo: terms.cmi orderings.cmi foUtils.cmi index.cmi -index.cmx: terms.cmx orderings.cmx foUtils.cmx index.cmi +orderings.cmo: terms.cmi pp.cmi foUtils.cmi foUnif.cmi foSubst.cmi \ + orderings.cmi +orderings.cmx: terms.cmx pp.cmx foUtils.cmx foUnif.cmx foSubst.cmx \ + orderings.cmi +clauses.cmo: terms.cmi orderings.cmi foUtils.cmi foUnif.cmi foSubst.cmi \ + clauses.cmi +clauses.cmx: terms.cmx orderings.cmx foUtils.cmx foUnif.cmx foSubst.cmx \ + clauses.cmi +index.cmo: terms.cmi orderings.cmi foUtils.cmi clauses.cmi index.cmi +index.cmx: terms.cmx orderings.cmx foUtils.cmx clauses.cmx index.cmi superposition.cmo: terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \ - foUnif.cmi foSubst.cmi superposition.cmi + foUnif.cmi foSubst.cmi clauses.cmi superposition.cmi superposition.cmx: terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \ - foUnif.cmx foSubst.cmx superposition.cmi + foUnif.cmx foSubst.cmx clauses.cmx superposition.cmi stats.cmo: terms.cmi pp.cmi stats.cmi stats.cmx: terms.cmx pp.cmx stats.cmi paramod.cmo: terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \ - foUtils.cmi foUnif.cmi paramod.cmi + foUtils.cmi foUnif.cmi clauses.cmi paramod.cmi paramod.cmx: terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \ - foUtils.cmx foUnif.cmx paramod.cmi + foUtils.cmx foUnif.cmx clauses.cmx paramod.cmi nCicBlob.cmo: terms.cmi foUtils.cmi nCicBlob.cmi nCicBlob.cmx: terms.cmx foUtils.cmx nCicBlob.cmi cicBlob.cmo: terms.cmi cicBlob.cmi diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 4a6886205..8bbf6e160 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -12,7 +12,7 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) let debug s = prerr_endline (Lazy.force s) ;; -(* let debug _ = ();; *) +let debug _ = ();; let monster = 100;; @@ -66,14 +66,16 @@ module Paramod (B : Orderings.Blob) = struct let add_passive_clause ?(bonus_weight=0) (passives_w,passives_a) cl = let (w,cl) = Clauses.mk_passive_clause cl in - let cl = (w+bonus_weight,cl) in - WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a + (* let cl = (w+bonus_weight,cl) in *) + let cl = if bonus_weight = 0 then (w,cl) else (0,cl) in + WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a ;; let add_passive_goal ?(bonus_weight=0) (passives_w,passives_a) g = let (w,g) = Clauses.mk_passive_goal g in - let g = (w+bonus_weight,g) in - WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a + (* let g = (w+bonus_weight,g) in *) + let g = if bonus_weight = 0 then (w,g) else (0,g) in + WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a ;; let remove_passive_clause (passives_w,passives_a) cl = diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 63507aea6..51269d2b3 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -24,7 +24,7 @@ module Superposition (B : Orderings.Blob) = exception Success of B.t Terms.bag * int * B.t Terms.clause let debug s = prerr_endline (Lazy.force s);; - (* let debug _ = ();; *) + let debug _ = ();; let enable = true;; let rec list_first f = function @@ -118,10 +118,10 @@ module Superposition (B : Orderings.Blob) = let vl = Clauses.vars_of_clause cl in let cl,maxvar = if fresh then Clauses.fresh_clause ~subst maxvar (0, nlit, plit, vl, proof) - else cl,maxvar + else (0,nlit,plit,vl,proof),maxvar in let bag, cl = - Terms.add_to_bag (0, nlit, plit, vl, proof) bag + Terms.add_to_bag cl bag in Some (bag, maxvar, cl, literal) else @@ -287,6 +287,7 @@ module Superposition (B : Orderings.Blob) = | _ -> false let fold_build_new_clause bag maxvar id rule filter res clause_ctx = + debug (lazy (string_of_int (List.length res))); let (bag, maxvar), res = HExtlib.filter_map_acc (fun (bag, maxvar) (t,subst,id2,pos,dir) -> @@ -334,6 +335,7 @@ module Superposition (B : Orderings.Blob) = let is_subsumed ~unify bag maxvar (id, nlit, plit, vl, _) table = match nlit,plit with + | [Terms.Equation (l,r,ty,_) ,_],[] | [],[Terms.Equation (l,r,ty,_) ,_]-> (match rewrite_eq ~unify l r ty vl table with | None -> None @@ -566,7 +568,6 @@ module Superposition (B : Orderings.Blob) = if no_demod then bag, clause else demodulate bag clause table in if List.exists (Clauses.are_alpha_eq_cl clause) g_actives then None else - (debug (lazy (Pp.pp_clause clause)); if (is_goal_trivial clause) then raise (Success (bag, maxvar, clause)) else @@ -583,7 +584,7 @@ module Superposition (B : Orderings.Blob) = | None -> Some (bag,clause) | Some (bag,maxvar,cl,subst) -> prerr_endline "Goal subsumed"; - raise (Success (bag,maxvar,cl))) + raise (Success (bag,maxvar,cl)) (* else match is_subsumed ~unify:true bag maxvar clause table with | None -> Some (bag, clause) @@ -603,11 +604,13 @@ module Superposition (B : Orderings.Blob) = (* this is OK for both the sup_left and sup_right inference steps *) let superposition table varlist is_pos subterm pos context = let cands = IDX.DT.retrieve_unifiables table subterm in - HExtlib.filter_map + let res = HExtlib.filter_map (fun (dir, is_cand_pos, _, (id,nlit,plit,vl,_ (*as uc*))) -> match nlit,plit with | [],[Terms.Equation (l,r,_,o),_] -> (let side, newside = if dir=Terms.Left2Right then l,r else r,l in + debug (lazy (Pp.pp_foterm subterm)); + debug (lazy (Pp.pp_foterm side)); try let subst = Unif.unification (* (varlist@vl)*) [] subterm side @@ -620,14 +623,16 @@ module Superposition (B : Orderings.Blob) = if o <> Terms.Lt && o <> Terms.Eq then Some (context newside, subst, id, pos, dir) else - ((*prerr_endline ("Filtering: " ^ - Pp.pp_foterm side ^ " =(< || =)" ^ - Pp.pp_foterm newside);*)None) + (debug (lazy "Filtering out..."); None) else Some (context newside, subst, id, pos, dir) with FoUnif.UnificationFailure _ -> None) | _ -> assert false) (IDX.ClauseSet.elements cands) + in + debug (lazy (string_of_int (List.length (IDX.ClauseSet.elements cands)) ^ " candidates")); + debug (lazy (string_of_int (List.length res) ^ " results")); + res ;; (* Superposes selected equation with equalities in table *) @@ -765,7 +770,7 @@ module Superposition (B : Orderings.Blob) = List.fold_left (superpose_literal id vl atable false) (bag,maxvar,[],List.tl nlit,[]) nlit in - debug (lazy "Superposed goal with active clauses"); + debug (lazy (string_of_int (List.length new_goals) ^ " new goals")); (* We simplify the new goals with active clauses *) let bag, new_goals = List.fold_left