From ad4ab0b27cf44913b82c32f9405a7c87719d77ef Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Sun, 19 Jun 2005 12:42:08 +0000 Subject: [PATCH] limited-resource-strategy implementation (now working!) --- helm/ocaml/paramodulation/saturation.ml | 170 +++++++++++++++++------- 1 file changed, 124 insertions(+), 46 deletions(-) diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index aebb04775..c45124338 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -107,18 +107,18 @@ let select env passive (active, _) = | (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) @@ -127,16 +127,7 @@ let select env passive (active, _) = 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 @@ -220,26 +211,87 @@ let size_of_passive ((_, ns), (_, ps), _) = ;; -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 @@ -567,13 +619,17 @@ let rec given_clause env passive active = 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 @@ -685,6 +741,23 @@ let rec given_clause env passive active = 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 -> @@ -739,6 +812,11 @@ let rec given_clause_fullred env passive active = 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" @@ -834,10 +912,10 @@ let main () = 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 -> -- 2.39.2