open Inference;;
open Utils;;
+
(*
for debugging
let check_equation env equation msg =
(* equality-selection related globals *)
let use_fullred = ref true;;
-let weight_age_ratio = ref (* 5 *) 4;; (* settable by the user *)
-let weight_age_counter = ref !weight_age_ratio;;
-let symbols_ratio = ref (* 0 *) 3;;
+let weight_age_ratio = ref 5 (* 5 *);; (* settable by the user *)
+let weight_age_counter = ref !weight_age_ratio ;;
+let symbols_ratio = ref 0 (* 3 *);;
let symbols_counter = ref 0;;
(* non-recursive Knuth-Bendix term ordering by default *)
with Failure "hd" -> Pervasives.compare eq1 eq2
)
| res -> res
-end
+end
module EqualitySet = Set.Make(OrderedEquality);;
+exception Empty_list;;
+
+let passive_is_empty = function
+ | ([], _), ([], _), _ -> true
+ | _ -> false
+;;
+
+
+let size_of_passive ((_, ns), (_, ps), _) =
+ (EqualitySet.cardinal ns) + (EqualitySet.cardinal ps)
+;;
+
+
+let size_of_active (active_list, _) =
+ List.length active_list
+;;
+
+let age_factor = 0.01;;
+
+let min_elt weight l =
+ fst
+ (match l with
+ [] -> raise Empty_list
+ | a::tl ->
+ let wa = float_of_int (weight a) in
+ let x = ref 0. in
+ List.fold_left
+ (fun (current,w) arg ->
+ x:=!x +. 1.;
+ let w1 = weight arg in
+ let wa = (float_of_int w1) +. !x *. age_factor in
+ if wa < w then (arg,wa) else (current,w))
+ (a,wa) tl)
+;;
+
+(*
+let compare eq1 eq2 =
+ let w1, _, (ty, left, right, _), m1, _ = eq1 in
+ let w2, _, (ty', left', right', _), m2, _ = eq2 in
+ match Pervasives.compare w1 w2 with
+ | 0 -> (List.length m1) - (List.length m2)
+ | res -> res
+;;
+*)
(**
selects one equality from passive. The selection strategy is a combination
of weight, age and goal-similarity
*)
-let select env goals passive (active, _) =
+let rec select env goals passive (active, _) =
processed_clauses := !processed_clauses + 1;
let goal =
match (List.rev goals) with (_, goal::_)::_ -> goal | _ -> assert false
(Negative, hd),
((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
| [], (hd:EqualitySet.elt)::tl ->
+ let w,_,_,_,_ = hd in
let passive_table =
- Indexing.remove_index passive_table hd
- in
- (Positive, hd),
+ Indexing.remove_index passive_table hd
+ in (Positive, hd),
(([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table)
| _, _ -> assert false
)
- | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> (
- symbols_counter := !symbols_counter - 1;
+ | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) ->
+ (symbols_counter := !symbols_counter - 1;
let cardinality map =
TermMap.fold (fun k v res -> res + v) map 0
in
)
| _ ->
symbols_counter := !symbols_ratio;
- let set_selection set = EqualitySet.min_elt set in
+ let set_selection set = EqualitySet.min_elt set in
+ (* let set_selection l = min_elt (fun (w,_,_,_,_) -> w) l in *)
if EqualitySet.is_empty neg_set then
let current = set_selection pos_set in
let passive =
;;
-let passive_is_empty = function
- | ([], _), ([], _), _ -> true
- | _ -> false
-;;
-
-
-let size_of_passive ((_, ns), (_, ps), _) =
- (EqualitySet.cardinal ns) + (EqualitySet.cardinal ps)
-;;
-
-
-let size_of_active (active_list, _) =
- List.length active_list
-;;
-
-
(* removes from passive equalities that are estimated impossible to activate
within the current time limit *)
let prune_passive howmany (active, _) passive =
(** inference of new equalities between current and some in active *)
let infer env sign current (active_list, active_table) =
+ let (_,c,_) = env in
+ if Utils.debug_metas then
+ (ignore(Indexing.check_target c current "infer1");
+ ignore(List.map (function (_,current) -> Indexing.check_target c current "infer2") active_list));
let new_neg, new_pos =
match sign with
| Negative ->
let maxm, res =
Indexing.superposition_left !maxmeta env active_table current in
+ if Utils.debug_metas then
+ ignore(List.map
+ (function current ->
+ Indexing.check_target c current "sup-1") res);
maxmeta := maxm;
res, []
| Positive ->
let maxm, res =
Indexing.superposition_right !maxmeta env active_table current in
- maxmeta := maxm;
+ if Utils.debug_metas then
+ ignore(List.map
+ (function current ->
+ Indexing.check_target c current "sup0") res);
+ maxmeta := maxm;
let rec infer_positive table = function
| [] -> [], []
| (Negative, equality)::tl ->
let maxm, res =
Indexing.superposition_left !maxmeta env table equality in
maxmeta := maxm;
+ if Utils.debug_metas then
+ ignore(List.map
+ (function current ->
+ Indexing.check_target c current "supl") res);
let neg, pos = infer_positive table tl in
res @ neg, pos
| (Positive, equality)::tl ->
let maxm, res =
Indexing.superposition_right !maxmeta env table equality in
maxmeta := maxm;
+ if Utils.debug_metas then
+ ignore
+ (List.map
+ (function current ->
+ Indexing.check_target c current "sup2") res);
let neg, pos = infer_positive table tl in
neg, res @ pos
in
let curr_table = Indexing.index Indexing.empty current in
let neg, pos = infer_positive curr_table active_list in
+ if Utils.debug_metas then
+ ignore(List.map
+ (function current ->
+ Indexing.check_target c current "sup3") pos);
neg, res @ pos
in
derived_clauses := !derived_clauses + (List.length new_neg) +
(List.length new_pos);
match !maximal_retained_equality with
- | None -> new_neg, new_pos
+ | None ->
+ if Utils.debug_metas then
+ (ignore(List.map
+ (function current ->
+ Indexing.check_target c current "sup4") new_pos);
+ ignore(List.map
+ (function current ->
+ Indexing.check_target c current "sup5") new_neg));
+ new_neg, new_pos
| Some eq ->
+ ignore(assert false);
(* if we have a maximal_retained_equality, we can discard all equalities
"greater" than it, as they will never be reached... An equality is
greater than maximal_retained_equality if it is bigger
in
List.filter filterfun new_pos
in
- new_neg, new_pos
+ new_neg, new_pos
;;
(** simplifies current using active and passive *)
let forward_simplify env (sign, current) ?passive (active_list, active_table) =
+ let _, context, _ = env in
let pl, passive_table =
match passive with
| None -> [], None
and pp = List.map (fun e -> (Positive, e)) pp in
pn @ pp, Some pt
in
- let all = if pl = [] then active_list else active_list @ pl in
+ let all = if pl = [] then active_list else active_list @ pl in
let demodulate table current =
let newmeta, newcurrent =
Some (sign, newcurrent)
in
let res =
+ if Utils.debug_metas then
+ ignore (Indexing.check_target context current "demod0");
let res = demodulate active_table current in
+ if Utils.debug_metas then
+ ignore ((function None -> () | Some (_,x) ->
+ Indexing.check_target context x "demod1";()) res);
match res with
| None -> None
| Some (sign, newcurrent) ->
(** simplifies new using active and passive *)
let forward_simplify_new env (new_neg, new_pos) ?passive active =
+ if Utils.debug_metas then
+ begin
+ let m,c,u = env in
+ ignore(List.map
+ (fun current ->
+ Indexing.check_target c current "forward new neg") new_neg);
+ ignore(List.map
+ (fun current -> Indexing.check_target c current "forward new pos")
+ new_pos;)
+ end;
let t1 = Unix.gettimeofday () in
let active_list, active_table = active in
let new_neg, new_pos =
let new_neg = List.map (demodulate Negative active_table) new_neg
and new_pos = List.map (demodulate Positive active_table) new_pos in
- new_neg,new_pos
-
-(* PROVA
+ new_neg,new_pos
+(* PROVA
match passive_table with
| None -> new_neg, new_pos
| Some passive_table ->
| None ->
active, (make_passive [] []), newa, None
| Some passive ->
+ active, passive, newa, None
+(* prova
let passive, newp =
backward_simplify_passive env new_pos new_table min_weight passive in
- active, passive, newa, newp
+ active, passive, newa, newp *)
;;
+let close env new' given =
+ let new_pos, new_table, min_weight =
+ List.fold_left
+ (fun (l, t, w) e ->
+ let ew, _, _, _, _ = e in
+ (Positive, e)::l, Indexing.index t e, min ew w)
+ ([], Indexing.empty, 1000000) (snd new')
+ in
+ List.fold_left
+ (fun (n,p) (s,c) ->
+ let neg,pos = infer env s c (new_pos,new_table) in
+ neg@n,pos@p)
+ ([],[]) given
+;;
+
+let is_commutative_law eq =
+ let w, proof, (eq_ty, left, right, order), metas, args = snd eq in
+ match left,right with
+ Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1],
+ Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] ->
+ f1 = f2 && a1 = b2 && a2 = b1
+ | _ -> false
+;;
+
+let prova env new' active =
+ let given = List.filter is_commutative_law (fst active) in
+ let _ =
+ debug_print
+ (lazy
+ (Printf.sprintf "symmetric:\n%s\n"
+ (String.concat "\n"
+ ((List.map
+ (fun (s, e) -> (string_of_sign s) ^ " " ^
+ (string_of_equality ~env e))
+ (given)))))) in
+ close env new' given
+;;
+
(* returns an estimation of how many equalities in passive can be activated
within the current time limit *)
let get_selection_estimate () =
try
let subst, metasenv', _ =
let menv = metasenv @ metas @ gmetas in
- Inference.unification menv context eqterm gterm ugraph
+ Inference.unification metas gmetas context eqterm gterm ugraph
in
let newproof =
match proof with
(* given-clause algorithm with lazy reduction strategy *)
let rec given_clause dbd env goals theorems passive active =
+ let _,context,_ = env in
let goals = simplify_goals env goals active in
let ok, goals = activate_goal goals in
(* let theorems = simplify_theorems env theorems active in *)
else given_clause_aux dbd env goals theorems passive active
and given_clause_aux dbd env goals theorems passive active =
+ let _,context,_ = env in
let time1 = Unix.gettimeofday () in
-
+
let selection_estimate = get_selection_estimate () in
let kept = size_of_passive passive in
let passive =
given_clause dbd env goals theorems passive active
| false ->
let (sign, current), passive = select env (fst goals) passive active in
+ let names = List.map (HExtlib.map_option (fun (name,_) -> name)) context in
+ prerr_endline ("Selected = " ^
+ (CicPp.pp (Inference.term_of_equality current) names));
let time1 = Unix.gettimeofday () in
let res = forward_simplify env (sign, current) ~passive active in
let time2 = Unix.gettimeofday () in
(string_of_equality ~env current)));
let _, proof, _, _, _ = current in
ParamodulationSuccess (Some proof, env)
- ) else (
+ ) else (
debug_print
(lazy "\n================================================");
debug_print (lazy (Printf.sprintf "selected: %s %s"
(** given-clause algorithm with full reduction strategy *)
let rec given_clause_fullred dbd env goals theorems passive active =
- let goals = simplify_goals env goals ~passive active in
+ let goals = simplify_goals env goals ~passive active in
+ let _,context,_ = env in
let ok, goals = activate_goal goals in
(* let theorems = simplify_theorems env theorems ~passive active in *)
if ok then
+ let names = List.map (HExtlib.map_option (fun (name,_) -> name)) context in
+ let _, _, t = List.hd (snd (List.hd (fst goals))) in
+ let _ = prerr_endline ("goal activated = " ^ (CicPp.pp t names)) in
(* let _ = *)
(* debug_print *)
(* (lazy *)
| (_, [proof, _, _])::_ -> Some proof
| _ -> assert false
in
- ParamodulationSuccess (proof, env)
+ ( prerr_endline "esco qui";
+ let s = Printf.sprintf "actives:\n%s\n"
+ (String.concat "\n"
+ ((List.map
+ (fun (s, e) -> (string_of_sign s) ^ " " ^
+ (string_of_equality ~env e))
+ (fst active)))) in
+ let sp = Printf.sprintf "passives:\n%s\n"
+ (String.concat "\n"
+ (List.map
+ (string_of_equality ~env)
+ (let x,y,_ = passive in (fst x)@(fst y)))) in
+ prerr_endline s;
+ prerr_endline sp;
+ ParamodulationSuccess (proof, env))
else
given_clause_fullred_aux dbd env goals theorems passive active
else
else given_clause_fullred_aux dbd env goals theorems passive active
and given_clause_fullred_aux dbd env goals theorems passive active =
+ prerr_endline ("MAXMETA: " ^ string_of_int !maxmeta ^
+ " LOCALMAX: " ^ string_of_int !Indexing.local_max ^
+ " #ACTIVES: " ^ string_of_int (size_of_active active) ^
+ " #PASSIVES: " ^ string_of_int (size_of_passive passive));
+ if (size_of_active active) mod 54 = 0 then
+ (let s = Printf.sprintf "actives:\n%s\n"
+ (String.concat "\n"
+ ((List.map
+ (fun (s, e) -> (string_of_sign s) ^ " " ^
+ (string_of_equality ~env e))
+ (fst active)))) in
+ let sp = Printf.sprintf "passives:\n%s\n"
+ (String.concat "\n"
+ (List.map
+ (string_of_equality ~env)
+ (let x,y,_ = passive in (fst x)@(fst y)))) in
+ prerr_endline s;
+ prerr_endline sp);
let time1 = Unix.gettimeofday () in
-
+ let (_,context,_) = env in
let selection_estimate = get_selection_estimate () in
let kept = size_of_passive passive in
let passive =
given_clause_fullred dbd env goals theorems passive active
| false ->
let (sign, current), passive = select env (fst goals) passive active in
+ let names = List.map (HExtlib.map_option (fun (name,_) -> name)) context in
+ prerr_endline ("Selected = " ^ (string_of_sign sign) ^ " " ^
+ string_of_equality ~env current);
+ (* (CicPp.pp (Inference.term_of_equality current) names));*)
let time1 = Unix.gettimeofday () in
let res = forward_simplify env (sign, current) ~passive active in
let time2 = Unix.gettimeofday () in
let t1 = Unix.gettimeofday () in
let new' = infer env sign current active in
+ let _ =
+ match new' with
+ | neg, pos ->
+ debug_print
+ (lazy
+ (Printf.sprintf "new' (senza semplificare):\n%s\n"
+ (String.concat "\n"
+ ((List.map
+ (fun e -> "Negative " ^
+ (string_of_equality ~env e)) neg) @
+ (List.map
+ (fun e -> "Positive " ^
+ (string_of_equality ~env e)) pos)))))
+ in
let t2 = Unix.gettimeofday () in
infer_time := !infer_time +. (t2 -. t1);
-
let active =
if is_identity env current then active
else
let active, passive, newa, retained =
backward_simplify env new' ~passive active in
let t2 = Unix.gettimeofday () in
- backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
+ backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
match newa, retained with
| None, None -> active, passive, new'
| Some (n, p), None
| None, Some (n, p) ->
let nn, np = new' in
+ if Utils.debug_metas then
+ ignore (
+ List.map (fun x -> Indexing.check_target context x "simplify1")n;
+ List.map (fun x -> Indexing.check_target context x "simplify2")p);
simplify (nn @ n, np @ p) active passive
| Some (n, p), Some (rn, rp) ->
let nn, np = new' in
simplify (nn @ n @ rn, np @ p @ rp) active passive
in
let active, passive, new' = simplify new' active passive in
-
+(* pessima prova
+ let new1 = prova env new' active in
+ let new' = (fst new') @ (fst new1), (snd new') @ (snd new1) in
+ let _ =
+ match new1 with
+ | neg, pos ->
+ debug_print
+ (lazy
+ (Printf.sprintf "new1:\n%s\n"
+ (String.concat "\n"
+ ((List.map
+ (fun e -> "Negative " ^
+ (string_of_equality ~env e)) neg) @
+ (List.map
+ (fun e -> "Positive " ^
+ (string_of_equality ~env e)) pos)))))
+ in
+end prova *)
let k = size_of_passive passive in
if k < (kept - 1) then
processed_clauses := !processed_clauses + (kept - 1 - k);
in
(*try*)
let goal = Inference.BasicProof new_meta_goal, [], goal in
- let equalities = simplify_equalities env (equalities@library_equalities) in
+ let equalities = simplify_equalities env
+ (equalities@library_equalities) in
let active = make_active () in
let passive = make_passive [] equalities in
Printf.printf "\ncurrent goal: %s\n"
| ParamodulationSuccess (None, env) ->
Printf.printf "Success, but no proof?!?\n\n"
in
- Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
+ if Utils.time then
+ begin
+ prerr_endline
+ ((Printf.sprintf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
"forward_simpl_new_time: %.9f\n" ^^
"backward_simpl_time: %.9f\n")
- !infer_time !forward_simpl_time !forward_simpl_new_time
- !backward_simpl_time;
- Printf.printf "passive_maintainance_time: %.9f\n"
- !passive_maintainance_time;
- Printf.printf " successful unification/matching time: %.9f\n"
- !Indexing.match_unif_time_ok;
- Printf.printf " failed unification/matching time: %.9f\n"
- !Indexing.match_unif_time_no;
- Printf.printf " indexing retrieval time: %.9f\n"
- !Indexing.indexing_retrieval_time;
- Printf.printf " demodulate_term.build_newtarget_time: %.9f\n"
- !Indexing.build_newtarget_time;
- Printf.printf "derived %d clauses, kept %d clauses.\n"
- !derived_clauses !kept_clauses;
+ !infer_time !forward_simpl_time !forward_simpl_new_time
+ !backward_simpl_time) ^
+ (Printf.sprintf "beta_expand_time: %.9f\n"
+ !Indexing.beta_expand_time) ^
+ (Printf.sprintf "passive_maintainance_time: %.9f\n"
+ !passive_maintainance_time) ^
+ (Printf.sprintf " successful unification/matching time: %.9f\n"
+ !Indexing.match_unif_time_ok) ^
+ (Printf.sprintf " failed unification/matching time: %.9f\n"
+ !Indexing.match_unif_time_no) ^
+ (Printf.sprintf " indexing retrieval time: %.9f\n"
+ !Indexing.indexing_retrieval_time) ^
+ (Printf.sprintf " demodulate_term.build_newtarget_time: %.9f\n"
+ !Indexing.build_newtarget_time) ^
+ (Printf.sprintf "derived %d clauses, kept %d clauses.\n"
+ !derived_clauses !kept_clauses))
+ end
(*
with exc ->
print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
let reset_refs () =
maxmeta := 0;
+ Indexing.local_max := 100;
symbols_counter := 0;
weight_age_counter := !weight_age_ratio;
processed_clauses := 0;
passive_maintainance_time := 0.;
derived_clauses := 0;
kept_clauses := 0;
+ Indexing.beta_expand_time := 0.;
+ Inference.metas_of_proof_time := 0.;
;;
let saturate
let library_equalities = List.map snd library_equalities in
let t2 = Unix.gettimeofday () in
maxmeta := maxm+2;
- let equalities = simplify_equalities env (equalities@library_equalities) in
+ let equalities = simplify_equalities env (equalities@library_equalities) in
debug_print
(lazy
(Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)));
let tall = fs_time_info.build_all in
let tdemodulate = fs_time_info.demodulate in
let tsubsumption = fs_time_info.subsumption in
- debug_print (lazy (Printf.sprintf "\nTIME NEEDED: %.9f" time));
- debug_print (lazy (Printf.sprintf "\ntall: %.9f" tall));
- debug_print (lazy (Printf.sprintf "\ntdemod: %.9f" tdemodulate));
- debug_print (lazy (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption));
- debug_print (lazy (Printf.sprintf "\ninfer_time: %.9f" !infer_time));
- debug_print (lazy (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time));
- debug_print (lazy (Printf.sprintf "\nforward_simpl_new_times: %.9f" !forward_simpl_new_time));
- debug_print (lazy (Printf.sprintf "\nbackward_simpl_times: %.9f" !backward_simpl_time));
- debug_print (lazy (Printf.sprintf "\npassive_maintainance_time: %.9f" !passive_maintainance_time));
+ if Utils.time then
+ begin
+ prerr_endline (
+ (Printf.sprintf "\nTIME NEEDED: %.9f" time) ^
+ (Printf.sprintf "\ntall: %.9f" tall) ^
+ (Printf.sprintf "\ntdemod: %.9f" tdemodulate) ^
+ (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption) ^
+ (Printf.sprintf "\ninfer_time: %.9f" !infer_time) ^
+ (Printf.sprintf "\nbeta_expand_time: %.9f\n"
+ !Indexing.beta_expand_time) ^
+ (Printf.sprintf "\nmetas_of_proof: %.9f\n"
+ !Inference.metas_of_proof_time) ^
+ (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time) ^
+ (Printf.sprintf "\nforward_simpl_new_times: %.9f"
+ !forward_simpl_new_time) ^
+ (Printf.sprintf "\nbackward_simpl_times: %.9f" !backward_simpl_time) ^
+ (Printf.sprintf "\npassive_maintainance_time: %.9f"
+ !passive_maintainance_time))
+ end;
newstatus
| _ ->
raise (ProofEngineTypes.Fail (lazy "NO proof found"))
(* (string_of_equality e) *)
)
equalities))));
- debug_print (lazy "SIMPLYFYING EQUALITIES...");
+ debug_print (lazy "RETR: SIMPLYFYING EQUALITIES...");
let rec simpl e others others_simpl =
let (u, e) = e in
let active = List.map (fun (u, e) -> (Positive, e))
let goalterm = Cic.Meta (metano,irl) in
let initgoal = Inference.BasicProof goalterm, [], ty in
let env = (metasenv, context, CicUniv.empty_ugraph) in
- let equalities = simplify_equalities env (equalities@library_equalities) in
+ let equalities = simplify_equalities env (equalities@library_equalities) in
let table =
List.fold_left
(fun tbl eq -> Indexing.index tbl eq)
projects / helm.git / blobdiff