From 320c0f89a7e31e996b6eff2b4165eb74e8141cec Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 23 Mar 2010 15:48:42 +0000 Subject: [PATCH] Fixed a few bugs From: asperti --- .../components/ng_paramodulation/nCicProof.ml | 35 +++++++++++++++---- .../components/ng_paramodulation/paramod.ml | 18 +++++++--- .../ng_paramodulation/superposition.ml | 7 +++- 3 files changed, 48 insertions(+), 12 deletions(-) diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml index 781b6bf08..df6f949b6 100644 --- a/helm/software/components/ng_paramodulation/nCicProof.ml +++ b/helm/software/components/ng_paramodulation/nCicProof.ml @@ -207,7 +207,7 @@ let debug c _ = c;; List.fold_left (fun (i,acc) t -> i+1, - let f = extract amount vl f in + let f = extract amount vl f in if i = n then let imp = NCic.Implicit `Term in NCic.Appl (dag::imp::imp::imp(* f *)::imp::imp:: @@ -218,7 +218,7 @@ let debug c _ = c;; in aux ft (List.rev pl) ;; - (* we should better split forward and backard rewriting *) + (* 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( @@ -264,6 +264,26 @@ let debug c _ = c;; let lit,_,_ = get_literal mp in let lit = Subst.apply_subst subst lit in extract 0 [] lit in + (* composition of all subst acting on goal *) + let res_subst = + let rec rsaux ongoal acc = + function + | [] -> acc (* is the final subst for refl *) + | id::tl when ongoal -> + let lit,vl,proof = get_literal id in + (match proof with + | Terms.Exact _ -> rsaux ongoal acc tl + | Terms.Step (_, _, _, _, _, s) -> + rsaux ongoal (s@acc) tl) + | id::tl -> + (* subst is the the substitution for refl *) + rsaux (id=mp) subst tl + in + let r = rsaux false [] steps in + (* prerr_endline ("res substitution: " ^ Pp.pp_substitution r); + prerr_endline ("\n" ^ "subst: " ^ Pp.pp_substitution subst); *) + r + in let rec aux ongoal seen = function | [] -> NCic.Rel 1 | id :: tl -> @@ -305,10 +325,12 @@ let debug c _ = c;; let id, id1,(lit,vl,proof) = if ongoal then let lit,vl,proof = get_literal id1 in - id1,id,(Subst.apply_subst subst lit, - Subst.filter subst vl, proof) + id1,id,(Subst.apply_subst res_subst lit, + Subst.filter res_subst vl, proof) else id,id1,(lit,vl,proof) in - let vl = if ongoal then [] else vl in + (* free variables remaining in the goal should not + be abstracted: we do not want to prove a generalization *) + let vl = if ongoal then [] else vl in let proof_of_id id = let vars = List.rev (vars_of id seen) in let args = List.map (Subst.apply_subst subst) vars in @@ -388,7 +410,8 @@ let debug c _ = c;; let body = aux ongoal ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl in - if NCicUntrusted.count_occurrences [] 0 body <= 1 then + let occ= NCicUntrusted.count_occurrences [] 1 body in + if occ <= 1 then NCicSubstitution.subst ~avoid_beta_redexes:true ~no_implicit:false (close_with_lambdas vl rewrite_step) body diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index de32ab5dd..7fc13b504 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -202,6 +202,12 @@ module Paramod (B : Orderings.Blob) = struct else WeightPassiveSet.min_elt passives_w ;; + let mk_unit_clause bag maxvar (t,ty) = + let c, maxvar = Utils.mk_unit_clause maxvar (B.embed ty) (B.embed t) in + let bag, c = Terms.add_to_bag c bag in + (bag, maxvar), c + ;; + let mk_clause bag maxvar (t,ty) = let (proof,ty) = B.saturate t ty in let c, maxvar = Utils.mk_unit_clause maxvar ty proof in @@ -210,9 +216,11 @@ module Paramod (B : Orderings.Blob) = struct ;; let mk_passive (bag,maxvar) = mk_clause bag maxvar;; + let mk_goal (bag,maxvar) = mk_clause bag maxvar;; + let initialize_goal (bag,maxvar,actives,passives,_,_) t = - let (bag,maxvar), g = mk_goal (bag,maxvar) t in + let (bag,maxvar), g = mk_unit_clause bag maxvar t in let g_passives = g_passive_empty_set in (* if the goal is not an equation we returns an empty passive set *) @@ -268,7 +276,7 @@ module Paramod (B : Orderings.Blob) = struct (List.map Pp.pp_unit_clause actives_l))) ^ ("Passives:" ^(String.concat ";\n" - (List.map (fun _,cl -> Pp.pp_unit_clause cl) + (List.map (fun (_,cl) -> Pp.pp_unit_clause cl) (IDX.ClauseSet.elements wset)))) ;; @@ -287,7 +295,7 @@ module Paramod (B : Orderings.Blob) = struct * P' = P + new' *) debug (lazy "Forward infer step..."); debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives))))); - debug (lazy (pp_clauses actives passives)); + noprint (lazy (pp_clauses actives passives)); match Sup.keep_simplified current actives bag maxvar with | _,None -> s @@ -356,7 +364,7 @@ module Paramod (B : Orderings.Blob) = struct let _ = noprint (lazy ("Passives:" ^(String.concat ";\n" - (List.map (fun _,cl -> Pp.pp_unit_clause cl) + (List.map (fun (_,cl) -> Pp.pp_unit_clause cl) (IDX.ClauseSet.elements wset))))) in let g_passives = WeightPassiveSet.fold @@ -566,7 +574,7 @@ let demod s goal = let fast_eq_check s goal = let (_,_,_,_,_,g_passives) as s = initialize_goal s goal in - if is_passive_g_set_empty g_passives then Error "not an equation" + if is_passive_g_set_empty g_passives then Error "not an equation" else try goal_narrowing 0 2 None s diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index f38acb536..c5bb640a2 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -412,6 +412,7 @@ module Superposition (B : Orderings.Blob) = match acc with | None -> None | Some(bag,maxvar,(id,lit,vl,p),subst) -> + (* prerr_endline ("input subst = "^Pp.pp_substitution subst); *) let l = Subst.apply_subst subst l in let r = Subst.apply_subst subst r in try @@ -426,6 +427,8 @@ module Superposition (B : Orderings.Blob) = with FoUnif.UnificationFailure _ -> match rewrite_eq ~unify l r ty vl table with | Some (id2, dir, subst1) -> + (* prerr_endline ("subst1 = "^Pp.pp_substitution subst1); + prerr_endline ("old subst = "^Pp.pp_substitution subst);*) let newsubst = Subst.concat subst1 subst in let id_t = FoSubst.apply_subst newsubst @@ -437,7 +440,9 @@ module Superposition (B : Orderings.Blob) = subst1 id id2 (pos@[2]) dir with | Some ((bag, maxvar), c), r -> - let newsubst = Subst.concat r newsubst in + (* prerr_endline ("r = "^Pp.pp_substitution r); *) + let newsubst = Subst.flat + (Subst.concat r subst) in Some(bag,maxvar,c,newsubst) | None, _ -> assert false) | None -> -- 2.39.2