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
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
;;
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
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
else if Unix.gettimeofday () > max_time then
(ParamodulationFailure "No more time to spend")
else
+ (*
let _ = prerr_endline "simpl goal with active" in
let _ = <:start<simplify goal set active>> in
- let goals = simplify_goal_set env goals passive active in
+ let goals = simplify_goal_set env goals passive active in
let _ = <:stop<simplify goal set active>> in
+ *)
match check_if_goals_set_is_solved env active goals with
| Some p ->
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 *)
+ (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *)
+ (*
let passive =
let selection_estimate = iterations_left iterno in
let kept = size_of_passive passive in
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! *)
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 *)
| 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
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 =
projects / helm.git / commitdiff