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
+*)
+ 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
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
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 =