From f820f75a0b94bcc6b6d31c9471c8921ce098427d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 4 May 2006 15:15:47 +0000 Subject: [PATCH] goal demodulated with new --- components/tactics/paramodulation/equality.ml | 16 +++- .../tactics/paramodulation/equality.mli | 4 + components/tactics/paramodulation/indexing.ml | 19 ++-- .../tactics/paramodulation/saturation.ml | 86 +++++++++++++++++-- 4 files changed, 105 insertions(+), 20 deletions(-) diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index 6c0b24327..c4aaa1ca4 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/components/tactics/paramodulation/equality.ml @@ -264,6 +264,12 @@ let mk_equality (weight,(newp,oldp),(ty,l,r,o),m) = eq ;; +let mk_tmp_equality (weight,(ty,l,r,o),m) = + let id = -1 in + uncomparable,weight,(Exact (Cic.Implicit None),NoProof),(ty,l,r,o),m,id +;; + + let open_equality (_,weight,proof,(ty,l,r,o),m,id) = (weight,proof,(ty,l,r,o),m,id) @@ -706,7 +712,7 @@ let wfo goalproof = let rec aux acc id = let p,_,_ = proof_of_id id in match p with - | Exact _ -> id :: acc + | Exact _ -> if (List.mem id acc) then acc else id :: acc | Step (_,(_,id1, (_,id2), _)) -> let acc = if not (List.mem id1 acc) then aux acc id1 else acc in let acc = if not (List.mem id2 acc) then aux acc id2 else acc in @@ -723,14 +729,18 @@ let string_of_id names id = Printf.sprintf "%d = %s: %s = %s" id (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names) | Step (_,(step,id1, (_,id2), _) ) -> - Printf.sprintf "%5d: %s %4d %4d %s = %s" id + Printf.sprintf "%6d: %s %6d %6d %s = %s" id (if step = SuperpositionRight then "SupR" else "Demo") id1 id2 (CicPp.pp l names) (CicPp.pp r names) with Not_found -> assert false let pp_proof names goalproof = - String.concat "\n" (List.map (string_of_id names) (wfo goalproof)) + String.concat "\n" (List.map (string_of_id names) (wfo goalproof)) ^ + "\ngoal is demodulated with " ^ + (String.concat " " + ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof))) +;; let build_goal_proof l initial = let proof = diff --git a/components/tactics/paramodulation/equality.mli b/components/tactics/paramodulation/equality.mli index ea0cefd55..2d7e48e5c 100644 --- a/components/tactics/paramodulation/equality.mli +++ b/components/tactics/paramodulation/equality.mli @@ -70,6 +70,10 @@ val mk_equality : (Cic.term * Cic.term * Cic.term * Utils.comparison) * Cic.metasenv -> equality + +val mk_tmp_equality : + int * (Cic.term * Cic.term * Cic.term * Utils.comparison) * Cic.metasenv -> + equality val open_equality : equality -> diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml index 584bf5c60..4ac1c94e2 100644 --- a/components/tactics/paramodulation/indexing.ml +++ b/components/tactics/paramodulation/indexing.ml @@ -639,7 +639,8 @@ let rec demodulation_equality ?from newmeta env table sign target = in if sign = Utils.Positive then (bo, - (Equality.Step (subst,(Equality.Demodulation,id,(pos,id'), + (Equality.Step (subst,(Equality.Demodulation, + id,(pos,id'), (*apply_subst subst*) (Cic.Lambda (name, ty, bo')))), Equality.ProofBlock ( subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof_old))) @@ -750,7 +751,7 @@ let rec demodulation_equality ?from newmeta env table sign target = (Equality.meta_convertibility_eq target newtarget) then newmeta, newtarget else - demodulation_equality newmeta env table sign newtarget + demodulation_equality ?from newmeta env table sign newtarget | None -> let res = demodulation_aux metasenv' context ugraph table 0 right in if Utils.debug_res then check_res res "demod result 1"; @@ -761,7 +762,7 @@ let rec demodulation_equality ?from newmeta env table sign target = (Equality.meta_convertibility_eq target newtarget) then newmeta, newtarget else - demodulation_equality newmeta env table sign newtarget + demodulation_equality ?from newmeta env table sign newtarget | None -> newmeta, target in @@ -1066,8 +1067,9 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = let what, other = if pos = Utils.Left then what, other else other, what in let newgoal, newproof = (* qua *) - let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in -(* let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in*) + let bo' = + Utils.guarded_simpl context (apply_subst s (S.subst other bo)) + in let name = C.Name "x" in incr sup_r_counter; let bo'' = @@ -1077,9 +1079,10 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = S.lift 1 eq_ty; l; r] in bo', - ( Equality.Step (s,(Equality.SuperpositionRight, - id,(pos,id'),(*apply_subst s*) (Cic.Lambda(name,ty,bo'')))), - Equality.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof2)) + (Equality.Step + (s,(Equality.SuperpositionRight, + id,(pos,id'),(Cic.Lambda(name,ty,bo'')))), + Equality.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof2)) in let newmeta, newequality = diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index f1cec900f..1cb6d3514 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -354,6 +354,50 @@ let infer env current (active_list, active_table) = List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos ;; +let check_for_deep_subsumption env active_table eq = + let _,_,(eq_ty, left, right, order),metas,id = Equality.open_equality eq in + if id = 14242 then assert false; + + let check deep l r = + let eqtmp = + Equality.mk_tmp_equality(0,(eq_ty,l,r,Utils.Incomparable),metas)in + match Indexing.subsumption env active_table eqtmp with + | None -> false + | Some (s,eq') -> + prerr_endline + ("\n\n " ^ Equality.string_of_equality ~env eq ^ + "\nis"^(if deep then " CONTEXTUALLY " else " ")^"subsumed by \n " ^ + Equality.string_of_equality ~env eq' ^ "\n\n"); + true + in + let rec aux b = function + | Cic.Rel n, Cic.Rel m -> if n = m then true else false + | ((Cic.Appl l) as left),((Cic.Appl l') as right) -> + check b left right || + (try + List.for_all2 (fun t t' -> aux true (t,t')) (List.tl l) (List.tl l') + with Invalid_argument _ -> false) + | (Cic.Meta _),_ + | _,(Cic.Meta _) -> false + | _ -> false + in + aux false (left,right) +;; + +(* +let check_for_deep env active_table eq = + match Indexing.subsumption env active_table eq with + | None -> false + | Some _ -> true +;; +*) + +let profiler = HExtlib.profile "check_for_deep";; + +let check_for_deep_subsumption env active_table eq = + profiler.HExtlib.profile (check_for_deep_subsumption env active_table) eq +;; + (* buttare via sign *) (** simplifies current using active and passive *) @@ -407,26 +451,35 @@ let forward_simplify env (sign,current) ?passive (active_list, active_table) = match res with | None -> None | Some c -> - (* immagino non funzioni piu'... *) if Indexing.in_index active_table c then None else match passive_table with | None -> + if check_for_deep_subsumption env active_table c then + None + else + res +(* if Indexing.subsumption env active_table c = None then res else None +*) | Some passive_table -> if Indexing.in_index passive_table c then None else - if Indexing.subsumption env active_table c = None then - if Indexing.subsumption env passive_table c = None then - res - else - None + if check_for_deep_subsumption env active_table c then + None + else +(* if Indexing.subsumption env active_table c = None then*) + (match Indexing.subsumption env passive_table c with + | None -> res + | Some (_,c') -> None (*Some c'*)) +(* else None +*) ;; type fs_time_info_t = { @@ -525,8 +578,8 @@ let rec simplify_goal env goal ?passive (active_list, active_table) = | None -> demodulate active_table goal | Some passive_table -> let changed, goal = demodulate active_table goal in - let changed', goal = demodulate passive_table goal in - (changed || changed'), goal +(* let changed', goal = demodulate passive_table goal in*) + (changed (*|| changed'*)), goal in changed, if not changed then @@ -634,15 +687,25 @@ let backward_simplify_passive env new_pos new_table min_weight passive = | _ -> ((pl, ps), passive_table), Some (newp) ;; +let build_table equations = + List.fold_left + (fun (l, t, w) e -> + let ew, _, _, _ , _ = Equality.open_equality e in + e::l, Indexing.index t e, min ew w) + ([], Indexing.empty, 1000000) equations +;; + let backward_simplify env new' ?passive active = - let new_pos, new_table, min_weight = + let new_pos, new_table, min_weight = build_table new' in +(* List.fold_left (fun (l, t, w) e -> let ew, _, _, _ , _ = Equality.open_equality e in e::l, Indexing.index t e, min ew w) ([], Indexing.empty, 1000000) new' in +*) let active, newa = backward_simplify_active env new_pos new_table min_weight active in match passive with @@ -1103,6 +1166,11 @@ and given_clause_fullred_aux dbd env goals theorems passive active = simplify (new' @ p @ rp) active passive in let active, _, new' = simplify new' active passive in + let goals = + let a,b,_ = build_table new' in + simplify_goals env goals ~passive (a,b) + in + (* pessima prova let new1 = prova env new' active in let new' = (fst new') @ (fst new1), (snd new') @ (snd new1) in -- 2.39.2