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
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;;
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
+ (* 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
| _ -> 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
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 =
;;
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
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
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<Saturation.>> ^ Indexing.get_stats () ^ Inference.get_stats ();;
+ <:show<Saturation.>> ^ Indexing.get_stats () ^ Inference.get_stats () ^
+ Equality.get_stats ();;