X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=f81556c8f997e7088fbfe006b3552fdec48c8132;hb=3b7bfb05e6fc1a2ac6864d8f7d959fcda0597d21;hp=b50e0a49f09fdafdaea42c51db772a880a58422c;hpb=50844b0116c863862434c7c673c5caaf6ff78cdf;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index b50e0a49f..f81556c8f 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -213,7 +213,17 @@ let rec select env (goals,_) passive = passive_table)) | _ -> symbols_counter := !symbols_ratio; - let current = EqualitySet.min_elt pos_set in + let my_min e1 e2 = + let w1,_,_,_,_ = Equality.open_equality e1 in + let w2,_,_,_,_ = Equality.open_equality e2 in + if w1 < w2 then e1 else e2 + in + let rec my_min_elt min = function + | [] -> min + | hd::tl -> my_min_elt (my_min hd min) tl + in + (* let current = EqualitySet.min_elt pos_set in *) + let current = my_min_elt (List.hd pos_list) (List.tl pos_list) in let passive_table = Indexing.remove_index passive_table current in @@ -958,7 +968,9 @@ let simplify_goal_set env goals passive active = List.fold_left (fun acc goal -> match simplify_goal env goal ~passive active with - | _, g -> if find g acc then acc else g::acc) + | changed, g -> + if changed then prerr_endline "???????????????cambiato ancora"; + if find g acc then acc else g::acc) (* active_goals active_goals *) [] active_goals in @@ -973,7 +985,7 @@ let simplify_goal_set env goals passive active = ;; let check_if_goals_set_is_solved env active goals = - let active_goals, passive_goals = goals in + let active_goals, passive_goals = goals in List.fold_left (fun proof goal -> match proof with @@ -985,29 +997,59 @@ let check_if_goals_set_is_solved env active goals = None active_goals ;; +let infer_goal_set env active goals = + let active_goals, passive_goals = goals in + let rec aux = function + | [] -> goals + | hd::tl -> + let changed,selected = simplify_goal env hd active in + if changed then + prerr_endline ("--------------- goal semplificato"); + let (_,_,t1) = selected in + if (List.exists + (fun (_,_,t) -> + Equality.meta_convertibility t t1) + active_goals) then aux tl + else + let passive_goals = tl in + let new_passive_goals = + if Utils.metas_of_term t1 = [] then passive_goals + else + let new' = + Indexing.superposition_left env (snd active) selected in + passive_goals @ new' + in + selected::active_goals, new_passive_goals + in + aux passive_goals +;; + +(* old let infer_goal_set env active goals = let active_goals, passive_goals = goals in let rec aux = function | [] -> goals | ((_,_,t1) as hd)::tl when - not (List.exists - (fun (_,_,t) -> Equality.meta_convertibility t t1) - active_goals) + not (List.exists + (fun (_,_,t) -> + Equality.meta_convertibility t t1) + active_goals) -> let selected = hd in let passive_goals = tl in - let _,_,ty = selected in - let new' = - if CicUtil.is_meta_closed ty then - [] - else - Indexing.superposition_left env (snd active) selected + let new_passive_goals = + if CicUtil.is_meta_closed t1 then + passive_goals + else + let new' = Indexing.superposition_left env (snd active) selected in + passive_goals @ new' in - selected::active_goals, passive_goals @ new' + selected::active_goals, new_passive_goals | _::tl -> aux tl in aux passive_goals ;; +*) let infer_goal_set_with_current env current goals = let active_goals, passive_goals = goals in @@ -1020,7 +1062,16 @@ let infer_goal_set_with_current env current goals = passive_goals active_goals ;; +let ids_of_goal g = + let p,_,_ = g in + let ids = List.map (fun _,_,i,_,_ -> i) p in + ids +;; +let ids_of_goal_set (ga,gp) = + List.flatten (List.map ids_of_goal ga) @ + List.flatten (List.map ids_of_goal gp) +;; let size_of_goal_set_a (l,_) = List.length l;; let size_of_goal_set_p (_,l) = List.length l;; @@ -1048,47 +1099,62 @@ let given_clause else if Unix.gettimeofday () > max_time then (ParamodulationFailure "No more time to spend") else +(* let _ = prerr_endline "simpl goal with active" in let _ = <:start> in - let goals = simplify_goal_set env goals passive active in + let goals = simplify_goal_set env goals passive active in let _ = <:stop> in +*) + let _ = + prerr_endline + (Printf.sprintf "%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)\n" + iterno (size_of_active active) (size_of_passive passive) + (size_of_goal_set_a goals) (size_of_goal_set_p goals)) + in + (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *) + let passive = + let selection_estimate = iterations_left iterno in + let kept = size_of_passive passive in + if kept > selection_estimate then + begin + (*Printf.eprintf "Too many passive equalities: pruning..."; + prune_passive selection_estimate active*) passive + end + else + passive + in + kept_clauses := (size_of_passive passive) + (size_of_active active); + let goals = infer_goal_set env active goals in match check_if_goals_set_is_solved env active goals with | Some p -> prerr_endline (Printf.sprintf "Found a proof in: %f\n" (Unix.gettimeofday() -. initial_time)); -(* assert false;*) ParamodulationSuccess p | None -> - prerr_endline - (Printf.sprintf "%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)\n" - iterno (size_of_active active) (size_of_passive passive) - (size_of_goal_set_a goals) (size_of_goal_set_p goals)); - (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *) - let passive = - let selection_estimate = iterations_left iterno in - let kept = size_of_passive passive in - if kept > selection_estimate then - begin - (*Printf.eprintf "Too many passive equalities: pruning..."; - prune_passive selection_estimate active*) passive - end - else - passive - in - kept_clauses := (size_of_passive passive) + (size_of_active active); (* SELECTION *) if passive_is_empty passive then ParamodulationFailure "No more passive"(*maybe this is a success! *) else begin - let goals = infer_goal_set env active goals in + (* COLLECTION OF GARBAGED EQUALITIES *) + if iterno mod 40 = 0 then + begin + let active = List.map Equality.id_of (fst active) in + let passive = List.map Equality.id_of (fst (fst passive)) in + let goal = ids_of_goal_set goals in + Equality.collect active passive goal + end; let current, passive = select env goals passive in - let _,_,goaltype = List.hd (fst goals) in - prerr_endline (Printf.sprintf "Current goal = %s\n" - (CicPp.pp goaltype names)); - prerr_endline (Printf.sprintf "Selected = %s\n" - (Equality.string_of_equality ~env current)); + let _ = + List.iter + (fun _,_,g -> + prerr_endline (Printf.sprintf "Current goal = %s\n" + (CicPp.pp g names))) + (fst goals); + prerr_endline (Printf.sprintf "Selected = %s\n" + (Equality.string_of_equality ~env current)) + in (* SIMPLIFICATION OF CURRENT *) let res = forward_simplify eq_uri env (Positive, current) active @@ -1388,6 +1454,12 @@ let eq_of_goal = function | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality "))) ;; +let eq_and_ty_of_goal = function + | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri -> + uri,t + | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality "))) +;; + let saturate dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = let module C = Cic in @@ -1404,7 +1476,8 @@ let saturate let eq_indexes, equalities, maxm = find_equalities context proof in let ugraph = CicUniv.empty_ugraph in let env = (metasenv, context, ugraph) in - let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, type_of_goal in + let cleaned_goal = Utils.remove_local_context type_of_goal in + let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in let res, time = let t1 = Unix.gettimeofday () in let lib_eq_uris, library_equalities, maxm = @@ -1752,7 +1825,6 @@ let main_demod_equalities dbd term metasenv ugraph = ;; let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) = - let module I = Inference in let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let eq_uri = eq_of_goal ty in @@ -1760,7 +1832,7 @@ let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) = Inference.find_equalities context proof in let lib_eq_uris, library_equalities, maxm = - I.find_library_equalities dbd context (proof, goal) (maxm+2) in + Inference.find_library_equalities dbd context (proof, goal) (maxm+2) in if library_equalities = [] then prerr_endline "VUOTA!!!"; let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let library_equalities = List.map snd library_equalities in @@ -1804,6 +1876,75 @@ let demodulate_tac ~dbd ~pattern = ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern) ;; +let rec find_in_ctx i name = function + | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name))) + | Some (Cic.Name name', _)::tl when name = name' -> i + | _::tl -> find_in_ctx (i+1) name tl +;; + +let rec position_of i x = function + | [] -> assert false + | j::tl when j <> x -> position_of (i+1) x tl + | _ -> i +;; + +let superposition_tac ~what ~other ~subterms_only ~demodulate status = + reset_refs(); + let proof,goalno = status in + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = CicUtil.lookup_meta goalno metasenv in + let eq_uri,tty = eq_and_ty_of_goal ty in + let env = (metasenv, context, CicUniv.empty_ugraph) in + let names = names_of_context context in + let eq_index, equalities, maxm = find_equalities context proof in + let what = find_in_ctx 1 what context in + let other = find_in_ctx 1 other context in + let eq_what = List.nth equalities (position_of 0 what eq_index) in + let eq_other = List.nth equalities (position_of 0 other eq_index) in + let index = Indexing.index Indexing.empty eq_other in + let maxm, eql = + Indexing.superposition_right + ~subterms_only eq_uri maxm env index eq_what + in + prerr_endline ("Superposition right:"); + prerr_endline ("\n eq: " ^ Equality.string_of_equality eq_what ~env); + prerr_endline ("\n table: " ^ Equality.string_of_equality eq_other ~env); + prerr_endline ("\n result: "); + List.iter (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql; + prerr_endline ("\n result (cut&paste): "); + List.iter + (fun e -> + let t = Equality.term_of_equality eq_uri e in + prerr_endline (CicPp.pp t names)) + eql; + if demodulate then + begin + let table = List.fold_left Indexing.index Indexing.empty equalities in + let maxm,eql = + List.fold_left + (fun (maxm,acc) e -> + let maxm,eq = + Indexing.demodulation_equality + eq_uri maxm env table Utils.Positive e + in + maxm,eq::acc) + (maxm,[]) eql + in + let eql = List.rev eql in + prerr_endline ("\n result [demod]: "); + List.iter + (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql; + prerr_endline ("\n result [demod] (cut&paste): "); + List.iter + (fun e -> + let t = Equality.term_of_equality eq_uri e in + prerr_endline (CicPp.pp t names)) + eql; + end; + proof,[goalno] +;; + let get_stats () = - <:show> ^ Indexing.get_stats () ^ Inference.get_stats ();; + <:show> ^ Indexing.get_stats () ^ Inference.get_stats () ^ + Equality.get_stats ();;