open Inference;;
open Utils;;
+
(* profiling statistics... *)
let infer_time = ref 0.;;
let forward_simpl_time = ref 0.;;
let maximal_retained_equality = ref None;;
(* equality-selection related globals *)
+let use_fullred = ref false;;
let weight_age_ratio = ref 0;; (* settable by the user from the command line *)
let weight_age_counter = ref !weight_age_ratio;;
let symbols_ratio = ref 0;;
(Negative, hd),
((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
| [], hd::tl ->
- let passive_table = Indexing.remove_index passive_table hd in
+ let passive_table =
+ Indexing.remove_index passive_table hd
+(* if !use_fullred then Indexing.remove_index passive_table hd *)
+(* else passive_table *)
+ in
(Positive, hd),
(([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table)
| _, _ -> assert false
| (Negative, e)::_ ->
let symbols = symbols_of_equality e in
let card = cardinality symbols in
+ let foldfun k v (r1, r2) =
+ if TermMap.mem k symbols then
+ let c = TermMap.find k symbols in
+ let c1 = abs (c - v) in
+ let c2 = v - c1 in
+ r1 + c2, r2 + c1
+ else
+ r1, r2 + v
+ in
let f equality (i, e) =
let common, others =
- TermMap.fold
- (fun k v (r1, r2) ->
- if TermMap.mem k symbols then
- let c = TermMap.find k symbols in
- let c1 = abs (c - v) in
- let c2 = v - c1 in
- r1 + c2, r2 + c1
- else
- r1, r2 + v)
- (symbols_of_equality equality) (0, 0)
+ TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
in
let c = others + (abs (common - card)) in
if c < i then (c, equality)
let e1 = EqualitySet.min_elt pos_set in
let initial =
let common, others =
- TermMap.fold
- (fun k v (r1, r2) ->
- if TermMap.mem k symbols then
- let c = TermMap.find k symbols in
- let c1 = abs (c - v) in
- let c2 = v - (abs (c - v)) in
- r1 + c1, r2 + c2
- else
- r1, r2 + v)
- (symbols_of_equality e1) (0, 0)
+ TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
in
(others + (abs (common - card))), e1
in
let _, current = EqualitySet.fold f pos_set initial in
(* Printf.printf "\nsymbols-based selection: %s\n\n" *)
(* (string_of_equality ~env current); *)
- let passive_table = Indexing.remove_index passive_table current in
+ let passive_table =
+ Indexing.remove_index passive_table current
+(* if !use_fullred then Indexing.remove_index passive_table current *)
+(* else passive_table *)
+ in
(Positive, current),
(([], neg_set),
(remove current pos_list, EqualitySet.remove current pos_set),
passive_table)
| _ ->
let current = EqualitySet.min_elt pos_set in
+ let passive_table =
+ Indexing.remove_index passive_table current
+(* if !use_fullred then Indexing.remove_index passive_table current *)
+(* else passive_table *)
+ in
let passive =
(neg_list, neg_set),
(remove current pos_list, EqualitySet.remove current pos_set),
- Indexing.remove_index passive_table current
+ passive_table
in
(Positive, current), passive
)
(neg_list, neg_set),
(remove current pos_list, EqualitySet.remove current pos_set),
Indexing.remove_index passive_table current
+(* if !use_fullred then Indexing.remove_index passive_table current *)
+(* else passive_table *)
in
(Positive, current), passive
else
let set_of equalities =
List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
in
- let table = Indexing.empty_table () in
+ let table =
+ List.fold_left (fun tbl e -> Indexing.index tbl e)
+ (Indexing.empty_table ()) pos
+(* if !use_fullred then *)
+(* List.fold_left (fun tbl e -> Indexing.index tbl e) *)
+(* (Indexing.empty_table ()) pos *)
+(* else *)
+(* Indexing.empty_table () *)
+ in
(neg, set_of neg),
(pos, set_of pos),
- List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
+ table
;;
let ok set equality = not (EqualitySet.mem equality set) in
let neg = List.filter (ok neg_set) new_neg
and pos = List.filter (ok pos_set) new_pos in
+ let table =
+ List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
+(* if !use_fullred then *)
+(* List.fold_left (fun tbl e -> Indexing.index tbl e) table pos *)
+(* else *)
+(* table *)
+ in
let add set equalities =
List.fold_left (fun s e -> EqualitySet.add e s) set equalities
in
(neg @ neg_list, add neg_set neg),
(pos_list @ pos, add pos_set pos),
- List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
+ table
;;
;;
-let prune_passive (((nl, ns), (pl, ps), tbl) as passive) =
- let f =
- int_of_float ((!time_limit -. !elapsed_time) /.
- (!elapsed_time *. (float_of_int !weight_age_ratio)))
+let prune_passive howmany (active, _) passive =
+ let (nl, ns), (pl, ps), tbl = passive in
+ let howmany = float_of_int howmany
+ and ratio = float_of_int !weight_age_ratio in
+ let in_weight = int_of_float (howmany *. ratio /. (ratio +. 1.))
+ and in_age = int_of_float (howmany /. (ratio +. 1.)) in
+ Printf.printf "in_weight: %d, in_age: %d\n" in_weight in_age;
+ let symbols, card =
+ match active with
+ | (Negative, e)::_ ->
+ let symbols = symbols_of_equality e in
+ let card = TermMap.fold (fun k v res -> res + v) symbols 0 in
+ Some symbols, card
+ | _ -> None, 0
in
- let in_weight = !processed_clauses * !weight_age_ratio * f
- and in_age = !processed_clauses * f in
- let rec pickw w s =
- if w > 0 then
- try
- let e = EqualitySet.min_elt s in
- let w, s' = pickw (w-1) (EqualitySet.remove e s) in
- w, EqualitySet.add e s'
- with Not_found ->
- w, s
+ let counter = ref !symbols_ratio in
+ let rec pickw w ns ps =
+ if w > 0 then
+ if not (EqualitySet.is_empty ns) then
+ let e = EqualitySet.min_elt ns in
+ let ns', ps = pickw (w-1) (EqualitySet.remove e ns) ps in
+ EqualitySet.add e ns', ps
+ else if !counter > 0 then
+ let _ =
+ counter := !counter - 1;
+ if !counter = 0 then counter := !symbols_ratio
+ in
+ match symbols with
+ | None ->
+ let e = EqualitySet.min_elt ps in
+ let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
+ ns, EqualitySet.add e ps'
+ | Some symbols ->
+ let foldfun k v (r1, r2) =
+ if TermMap.mem k symbols then
+ let c = TermMap.find k symbols in
+ let c1 = abs (c - v) in
+ let c2 = v - c1 in
+ r1 + c2, r2 + c1
+ else
+ r1, r2 + v
+ in
+ let f equality (i, e) =
+ let common, others =
+ TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
+ in
+ let c = others + (abs (common - card)) in
+ if c < i then (c, equality)
+ else (i, e)
+ in
+ let e1 = EqualitySet.min_elt ps in
+ let initial =
+ let common, others =
+ TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
+ in
+ (others + (abs (common - card))), e1
+ in
+ let _, e = EqualitySet.fold f ps initial in
+ let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
+ ns, EqualitySet.add e ps'
+ else
+ let e = EqualitySet.min_elt ps in
+ let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
+ ns, EqualitySet.add e ps'
else
- 0, EqualitySet.empty
+ EqualitySet.empty, EqualitySet.empty
in
- let in_weight, ns = pickw in_weight ns in
- let _, ps = pickw in_weight ps in
+(* let in_weight, ns = pickw in_weight ns in *)
+(* let _, ps = pickw in_weight ps in *)
+ let ns, ps = pickw in_weight ns ps in
let rec picka w s l =
if w > 0 then
match l with
maximal_retained_equality := Some (EqualitySet.max_elt ps);
let tbl =
EqualitySet.fold
- (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) in
+ (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ())
+(* if !use_fullred then *)
+(* EqualitySet.fold *)
+(* (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) *)
+(* else *)
+(* tbl *)
+ in
(nl, ns), (pl, ps), tbl
;;
and pp = List.map (fun e -> (Positive, e)) pp in
pn @ pp, Some pt
in
- let all = active_list @ pl in
- let rec find_duplicate sign current = function
- | [] -> false
- | (s, eq)::tl when s = sign ->
- if meta_convertibility_eq current eq then true
- else find_duplicate sign current tl
- | _::tl -> find_duplicate sign current tl
- in
+ let all = if pl = [] then active_list else active_list @ pl in
+
+(* let rec find_duplicate sign current = function *)
+(* | [] -> false *)
+(* | (s, eq)::tl when s = sign -> *)
+(* if meta_convertibility_eq current eq then true *)
+(* else find_duplicate sign current tl *)
+(* | _::tl -> find_duplicate sign current tl *)
+(* in *)
let demodulate table current =
let newmeta, newcurrent =
Indexing.demodulation !maxmeta env table current in
in
match res with
| None -> None
- | Some (s, c) ->
- if find_duplicate s c all then
+ | Some (Negative, c) ->
+ let ok = not (
+ List.exists
+ (fun (s, eq) -> s = Negative && meta_convertibility_eq eq c)
+ all)
+ in
+ if ok then res else None
+ | Some (Positive, c) ->
+ if Indexing.in_index active_table c then
None
else
- res
+ match passive_table with
+ | None -> res
+ | Some passive_table ->
+ if Indexing.in_index passive_table c then None else res
+
+(* | Some (s, c) -> if find_duplicate s c all then None else res *)
+
(* if s = Utils.Negative then *)
(* res *)
(* else *)
in
let new_pos = EqualitySet.elements new_pos_set in
- let subs =
- match passive_table with
- | None ->
- (fun e -> not (Indexing.subsumption env active_table e))
- | Some passive_table ->
- (fun e -> not ((Indexing.subsumption env active_table e) ||
- (Indexing.subsumption env passive_table e)))
- in
+(* let subs = *)
+(* match passive_table with *)
+(* | None -> *)
+(* (fun e -> not (Indexing.subsumption env active_table e)) *)
+(* | Some passive_table -> *)
+(* (fun e -> not ((Indexing.subsumption env active_table e) || *)
+(* (Indexing.subsumption env passive_table e))) *)
+(* in *)
let t1 = Unix.gettimeofday () in
let t2 = Unix.gettimeofday () in
fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1);
- new_neg, new_pos
+ let is_duplicate =
+ match passive_table with
+ | None -> (fun e -> not (Indexing.in_index active_table e))
+ | Some passive_table ->
+ (fun e -> not ((Indexing.in_index active_table e) ||
+ (Indexing.in_index passive_table e)))
+ in
+ new_neg, List.filter is_duplicate new_pos
+
+(* new_neg, new_pos *)
+
(* let res = *)
(* (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
(* List.filter (fun e -> not (List.exists (f Positive e) all)) 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.)))
;;
let selection_estimate = get_selection_estimate () in
let kept = size_of_passive passive in
let passive =
- if !time_limit = 0. then
+ if !time_limit = 0. || !processed_clauses = 0 then
passive
- else if !elapsed_time > !time_limit then
+ else if !elapsed_time > !time_limit then (
+ Printf.printf "Time limit (%.2f) reached: %.2f\n"
+ !time_limit !elapsed_time;
make_passive [] []
- else if kept > selection_estimate then
- prune_passive passive
- else
+ ) else if kept > selection_estimate then (
+ Printf.printf ("Too many passive equalities: pruning... (kept: %d, " ^^
+ "selection_estimate: %d)\n") kept selection_estimate;
+ prune_passive selection_estimate active passive
+ ) else
passive
in
Success (proof, env)
else
let t1 = Unix.gettimeofday () in
- let new' = forward_simplify_new env new' active in
+ let new' = forward_simplify_new env new' (* ~passive *) active in
let t2 = Unix.gettimeofday () in
let _ =
forward_simpl_time := !forward_simpl_time +. (t2 -. t1)
let rec given_clause_fullred env passive active =
+ let selection_estimate = get_selection_estimate () in
+ let kept = size_of_passive passive in
+ let passive =
+ if !time_limit = 0. || !processed_clauses = 0 then
+ passive
+ else if !elapsed_time > !time_limit then (
+ Printf.printf "Time limit (%.2f) reached: %.2f\n"
+ !time_limit !elapsed_time;
+ make_passive [] []
+ ) else if kept > selection_estimate then (
+ Printf.printf ("Too many passive equalities: pruning... (kept: %d, " ^^
+ "selection_estimate: %d)\n") kept selection_estimate;
+ prune_passive selection_estimate active passive
+ ) else
+ passive
+ in
+
match passive_is_empty passive with
| true -> Failure
| false ->
simplify (nn @ n @ rn, np @ p @ rp) active passive
in
let active, passive, new' = simplify new' active passive in
+
+ let k = size_of_passive passive in
+ if k < (kept - 1) then
+ processed_clauses := !processed_clauses + (kept - 1 - k);
+
let _ =
Printf.printf "active:\n%s\n"
(String.concat "\n"
let start = Unix.gettimeofday () in
print_endline "GO!";
start_time := Unix.gettimeofday ();
- let res = !given_clause_ref env passive active in
+ let res =
+ (if !use_fullred then given_clause_fullred else given_clause)
+ env passive active
+ in
let finish = Unix.gettimeofday () in
match res with
| Failure ->
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 ("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;
+(* 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"
with exc ->
and set_conf f = configuration_file := f
and set_lpo () = Utils.compare_terms := lpo
and set_kbo () = Utils.compare_terms := nonrec_kbo
- and set_fullred () = given_clause_ref := given_clause_fullred
+ and set_fullred () = use_fullred := true
and set_time_limit v = time_limit := float_of_int v
in
Arg.parse [
projects / helm.git / blobdiff