let time_limit = ref 0.;; (* in seconds, settable by the user... *)
let start_time = ref 0.;; (* time at which the execution started *)
let elapsed_time = ref 0.;;
-let maximal_retained_equality = ref None;;
+let maximal_weight = ref None;;
+(* let maximal_retained_equality = ref None;; *)
(* equality-selection related globals *)
let use_fullred = ref false;;
let symbols_ratio = ref 0;;
let symbols_counter = ref 0;;
+(* statistics... *)
+let derived_clauses = ref 0;;
+let kept_clauses = ref 0;;
+
(* index of the greatest Cic.Meta created - TODO: find a better way! *)
let maxmeta = ref 0;;
;;
+let weight_of_equality (_, (ty, left, right, _), _, _) =
+ let weight_of t = fst (weight_of_term ~consider_metas:false t) in
+ (weight_of ty) + (weight_of left) + (weight_of right)
+;;
+
+
module OrderedEquality = struct
type t = Inference.equality
let weight_of t = fst (weight_of_term ~consider_metas:false t) in
let w1 = (weight_of ty) + (weight_of left) + (weight_of right)
and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in
+(* let w1 = weight_of_equality eq1 *)
+(* and w2 = weight_of_equality eq2 in *)
match Pervasives.compare w1 w2 with
| 0 -> Pervasives.compare eq1 eq2
| res -> res
;;
+let size_of_active (active_list, _) =
+ List.length active_list
+;;
+
+
let prune_passive howmany (active, _) passive =
let (nl, ns), (pl, ps), tbl = passive in
let howmany = float_of_int howmany
let w, s, l = picka w s tl in
w, s, hd::l
else
- 0, s, []
+ 0, s, l
in
let in_age, ns, nl = picka in_age ns nl in
let _, ps, pl = picka in_age ps pl in
if not (EqualitySet.is_empty ps) then
- maximal_retained_equality := Some (EqualitySet.max_elt ps);
+ maximal_weight := Some (weight_of_equality (EqualitySet.max_elt ps));
+(* maximal_retained_equality := Some (EqualitySet.max_elt ps); *)
let tbl =
EqualitySet.fold
(fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ())
let neg, pos = infer_positive curr_table active_list in
neg, res @ pos
in
- match !maximal_retained_equality with
+ derived_clauses := !derived_clauses + (List.length new_neg) +
+ (List.length new_pos);
+ match !maximal_weight(* !maximal_retained_equality *) with
| None -> new_neg, new_pos
- | Some eq ->
+ | Some w (* eq *) ->
let new_pos =
- List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos in
+ List.filter (fun e -> (weight_of_equality e) <= w (* OrderedEquality.compare e eq <= 0 *)) new_pos in
new_neg, new_pos
;;
let get_selection_estimate () =
elapsed_time := (Unix.gettimeofday ()) -. !start_time;
+(* !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *)
int_of_float (
ceil ((float_of_int !processed_clauses) *.
- (!time_limit /. !elapsed_time -. 1.)))
+ ((!time_limit *. 2.) /. !elapsed_time -. 1.)))
;;
) else
passive
in
+
+ kept_clauses := (size_of_passive passive) + (size_of_active active);
match passive_is_empty passive with
| true -> Failure
in
nn @ al @ pp, tbl
in
- let _ =
- Printf.printf "active:\n%s\n"
- (String.concat "\n"
- ((List.map
- (fun (s, e) -> (string_of_sign s) ^ " " ^
- (string_of_equality ~env e)) (fst active))));
- print_newline ();
- in
- let _ =
- match new' with
- | neg, pos ->
- Printf.printf "new':\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)));
- print_newline ();
- in
+(* let _ = *)
+(* Printf.printf "active:\n%s\n" *)
+(* (String.concat "\n" *)
+(* ((List.map *)
+(* (fun (s, e) -> (string_of_sign s) ^ " " ^ *)
+(* (string_of_equality ~env e)) (fst active)))); *)
+(* print_newline (); *)
+(* in *)
+(* let _ = *)
+(* match new' with *)
+(* | neg, pos -> *)
+(* Printf.printf "new':\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))); *)
+(* print_newline (); *)
+(* in *)
match contains_empty env new' with
| false, _ ->
let active =
al @ [(sign, current)], Indexing.index tbl current
in
let passive = add_to_passive passive new' in
- let (_, ns), (_, ps), _ = passive in
- Printf.printf "passive:\n%s\n"
- (String.concat "\n"
- ((List.map (fun e -> "Negative " ^
- (string_of_equality ~env e))
- (EqualitySet.elements ns)) @
- (List.map (fun e -> "Positive " ^
- (string_of_equality ~env e))
- (EqualitySet.elements ps))));
- print_newline ();
+(* let (_, ns), (_, ps), _ = passive in *)
+(* Printf.printf "passive:\n%s\n" *)
+(* (String.concat "\n" *)
+(* ((List.map (fun e -> "Negative " ^ *)
+(* (string_of_equality ~env e)) *)
+(* (EqualitySet.elements ns)) @ *)
+(* (List.map (fun e -> "Positive " ^ *)
+(* (string_of_equality ~env e)) *)
+(* (EqualitySet.elements ps)))); *)
+(* print_newline (); *)
given_clause env passive active
| true, proof ->
Success (proof, env)
env passive active
in
let finish = Unix.gettimeofday () in
- match res with
- | Failure ->
- Printf.printf "NO proof found! :-(\n\n"
- | Success (Some proof, env) ->
- Printf.printf "OK, found a proof!:\n%s\n%.9f\n"
- (PP.pp proof (names_of_context context))
- (finish -. start);
- Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
- "backward_simpl_time: %.9f\n")
- !infer_time !forward_simpl_time !backward_simpl_time;
+ let _ =
+ match res with
+ | Failure ->
+ Printf.printf "NO proof found! :-(\n\n"
+ | Success (Some proof, env) ->
+ Printf.printf "OK, found a proof!:\n%s\n%.9f\n"
+ (PP.pp proof (names_of_context context))
+ (finish -. start);
(* Printf.printf ("forward_simpl_details:\n build_all: %.9f\n" ^^ *)
(* " demodulate: %.9f\n subsumption: %.9f\n") *)
(* fs_time_info.build_all fs_time_info.demodulate *)
(* fs_time_info.subsumption; *)
- | Success (None, env) ->
- Printf.printf "Success, but no proof?!?\n\n"
+ | Success (None, env) ->
+ Printf.printf "Success, but no proof?!?\n\n"
+ in
+ Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
+ "backward_simpl_time: %.9f\n")
+ !infer_time !forward_simpl_time !backward_simpl_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 "derived %d clauses, kept %d clauses.\n"
+ !derived_clauses !kept_clauses;
with exc ->
print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
raise exc