From a41f941ef133b7b8dcdf306d63f43f7bfb8d5275 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 19 Jun 2006 13:06:10 +0000 Subject: [PATCH] some experiments --- .../tactics/paramodulation/saturation.ml | 88 +++++++++++++++---- 1 file changed, 69 insertions(+), 19 deletions(-) diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index b50e0a49f..67a328275 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 @@ -1048,10 +1090,12 @@ 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 + *) match check_if_goals_set_is_solved env active goals with | Some p -> prerr_endline @@ -1064,7 +1108,8 @@ let given_clause (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 *) + (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *) + (* let passive = let selection_estimate = iterations_left iterno in let kept = size_of_passive passive in @@ -1077,6 +1122,7 @@ let given_clause 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! *) @@ -1084,9 +1130,11 @@ let given_clause begin let goals = infer_goal_set env active goals in 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)); + let _,_,goaltype = List.hd (fst goals) in + 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)); (* SIMPLIFICATION OF CURRENT *) @@ -1098,6 +1146,7 @@ let given_clause | Some current -> (* GENERATION OF NEW EQUATIONS *) prerr_endline "infer"; + let _,_,_,_,id = Equality.open_equality current in let new' = infer eq_uri env current active in prerr_endline "infer goal"; let goals = infer_goal_set_with_current env current goals in @@ -1404,7 +1453,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 = -- 2.39.2