| (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 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 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 *)
+(* else *)
+(* 0, EqualitySet.empty *)
+(* in *)
+ 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
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
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"
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 ->
projects / helm.git / commitdiff