From eb29eb8e516abf6791aadc91d1ba7ea2e403614f Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Sun, 19 Jun 2005 10:09:42 +0000 Subject: [PATCH] path indexing integration, limited-resource-strategy implementation (not yet working) --- helm/ocaml/paramodulation/saturation.ml | 250 +++++++++++++++++------- 1 file changed, 183 insertions(+), 67 deletions(-) diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 25314a100..aebb04775 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -1,6 +1,28 @@ open Inference;; open Utils;; +(* profiling statistics... *) +let infer_time = ref 0.;; +let forward_simpl_time = ref 0.;; +let backward_simpl_time = ref 0.;; + +(* limited-resource-strategy related globals *) +let processed_clauses = ref 0;; (* number of equalities selected so far... *) +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;; + +(* equality-selection related globals *) +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;; +let symbols_counter = ref 0;; + +(* index of the greatest Cic.Meta created - TODO: find a better way! *) +let maxmeta = ref 0;; + + type result = | Failure | Success of Cic.term option * environment @@ -33,8 +55,7 @@ let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) = ;; -module OrderedEquality = -struct +module OrderedEquality = struct type t = Inference.equality let compare eq1 eq2 = @@ -54,14 +75,9 @@ end module EqualitySet = Set.Make(OrderedEquality);; -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;; -let symbols_counter = ref 0;; - - let select env passive (active, _) = + processed_clauses := !processed_clauses + 1; + let (neg_list, neg_set), (pos_list, pos_set), passive_table = passive in let remove eq l = List.filter (fun e -> e <> eq) l @@ -104,8 +120,6 @@ let select env passive (active, _) = r1, r2 + v) (symbols_of_equality equality) (0, 0) in -(* Printf.printf "equality: %s, common: %d, others: %d\n" *) -(* (string_of_equality ~env equality) common others; *) let c = others + (abs (common - card)) in if c < i then (c, equality) else (i, e) @@ -135,7 +149,7 @@ let select env passive (active, _) = (remove current pos_list, EqualitySet.remove current pos_set), passive_table) | _ -> - let current = EqualitySet.min_elt pos_set in + let current = EqualitySet.min_elt pos_set in let passive = (neg_list, neg_set), (remove current pos_list, EqualitySet.remove current pos_set), @@ -169,7 +183,7 @@ let make_passive neg pos = let set_of equalities = List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities in - let table = Hashtbl.create (List.length pos) in + let table = Indexing.empty_table () in (neg, set_of neg), (pos, set_of pos), List.fold_left (fun tbl e -> Indexing.index tbl e) table pos @@ -177,7 +191,7 @@ let make_passive neg pos = let make_active () = - [], Hashtbl.create 1 + [], Indexing.empty_table () ;; @@ -201,33 +215,87 @@ let passive_is_empty = function ;; -(* TODO: find a better way! *) -let maxmeta = ref 0;; +let size_of_passive ((_, ns), (_, ps), _) = + (EqualitySet.cardinal ns) + (EqualitySet.cardinal 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))) + 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 + else + 0, EqualitySet.empty + in + let in_weight, ns = pickw in_weight ns in + let _, ps = pickw in_weight ps in + let rec picka w s l = + if w > 0 then + match l with + | [] -> w, s, [] + | hd::tl when not (EqualitySet.mem hd s) -> + let w, s, l = picka (w-1) s tl in + w, EqualitySet.add hd s, hd::l + | hd::tl -> + let w, s, l = picka w s tl in + w, s, hd::l + else + 0, s, [] + 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); + let tbl = + EqualitySet.fold + (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) in + (nl, ns), (pl, ps), tbl +;; + let infer env sign current (active_list, active_table) = - match sign with - | Negative -> - Indexing.superposition_left env active_table current, [] - | Positive -> - let maxm, res = - Indexing.superposition_right !maxmeta env active_table current in - maxmeta := maxm; - let rec infer_positive table = function - | [] -> [], [] - | (Negative, equality)::tl -> - let res = Indexing.superposition_left env table equality in - 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; - let neg, pos = infer_positive table tl in - neg, res @ pos - in - let curr_table = Indexing.index (Hashtbl.create 1) current in - let neg, pos = infer_positive curr_table active_list in - neg, res @ pos + let new_neg, new_pos = + match sign with + | Negative -> + Indexing.superposition_left env active_table current, [] + | Positive -> + let maxm, res = + Indexing.superposition_right !maxmeta env active_table current in + maxmeta := maxm; + let rec infer_positive table = function + | [] -> [], [] + | (Negative, equality)::tl -> + let res = Indexing.superposition_left env table equality in + 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; + let neg, pos = infer_positive table tl in + neg, res @ pos + in + let curr_table = Indexing.index (Indexing.empty_table ()) current in + let neg, pos = infer_positive curr_table active_list in + neg, res @ pos + in + match !maximal_retained_equality with + | None -> new_neg, new_pos + | Some eq -> + let new_pos = + List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos in + new_neg, new_pos ;; @@ -287,12 +355,28 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = if find_duplicate s c all then None else - let pred (sign, eq) = - if sign <> s then false - else subsumption env c eq - in - if List.exists pred all then None - else res + res +(* if s = Utils.Negative then *) +(* res *) +(* else *) +(* if Indexing.subsumption env active_table c then *) +(* None *) +(* else ( *) +(* match passive_table with *) +(* | None -> res *) +(* | Some passive_table -> *) +(* if Indexing.subsumption env passive_table c then *) +(* None *) +(* else *) +(* res *) +(* ) *) + +(* let pred (sign, eq) = *) +(* if sign <> s then false *) +(* else subsumption env c eq *) +(* in *) +(* if List.exists pred all then None *) +(* else res *) ;; type fs_time_info_t = { @@ -326,22 +410,13 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = maxmeta := newmeta; newtarget in - let f sign' target (sign, eq) = - if sign <> sign' then false - else subsumption env target eq - in +(* let f sign' target (sign, eq) = *) +(* if sign <> sign' then false *) +(* else subsumption env target eq *) +(* in *) let t1 = Unix.gettimeofday () in - let new_neg, new_pos = - (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) - in - - let t2 = Unix.gettimeofday () in - fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1); - let t1 = Unix.gettimeofday () in - let new_neg, new_pos = let new_neg = List.map (demodulate active_table) new_neg and new_pos = List.map (demodulate active_table) new_pos in @@ -362,6 +437,31 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = EqualitySet.empty new_pos 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 t1 = Unix.gettimeofday () in + +(* let new_neg, new_pos = *) +(* List.filter subs new_neg, *) +(* List.filter subs new_pos *) +(* in *) + +(* let new_neg, new_pos = *) +(* (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) *) +(* in *) + + let t2 = Unix.gettimeofday () in + fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1); + new_neg, new_pos (* let res = *) (* (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *) @@ -376,7 +476,7 @@ let backward_simplify_active env (new_neg, new_pos) active = let new_pos, new_table = List.fold_left (fun (l, t) e -> (Positive, e)::l, Indexing.index t e) - ([], Hashtbl.create (List.length new_pos)) new_pos + ([], Indexing.empty_table ()) new_pos in let active_list, newa = List.fold_right @@ -400,7 +500,7 @@ let backward_simplify_active env (new_neg, new_pos) active = res, tbl else (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq) - active_list ([], Hashtbl.create (List.length active_list)), + active_list ([], Indexing.empty_table ()), List.fold_right (fun (s, eq) (n, p) -> if (s <> Negative) && (is_identity env eq) then @@ -420,7 +520,7 @@ let backward_simplify_passive env (new_neg, new_pos) passive = let new_pos, new_table = List.fold_left (fun (l, t) e -> (Positive, e)::l, Indexing.index t e) - ([], Hashtbl.create (List.length new_pos)) new_pos + ([], Indexing.empty_table ()) new_pos in let (nl, ns), (pl, ps), passive_table = passive in let f sign equality (resl, ress, newn) = @@ -437,7 +537,7 @@ let backward_simplify_passive env (new_neg, new_pos) passive = and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in let passive_table = List.fold_left - (fun tbl e -> Indexing.index tbl e) (Hashtbl.create (List.length pl)) pl + (fun tbl e -> Indexing.index tbl e) (Indexing.empty_table ()) pl in match newn, newp with | [], [] -> ((nl, ns), (pl, ps), passive_table), None @@ -457,12 +557,26 @@ let backward_simplify env new' ?passive active = ;; -let infer_time = ref 0.;; -let forward_simpl_time = ref 0.;; -let backward_simpl_time = ref 0.;; +let get_selection_estimate () = + elapsed_time := (Unix.gettimeofday ()) -. !start_time; + !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) +;; 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 + passive + else if !elapsed_time > !time_limit then + make_passive [] [] + else if kept > selection_estimate then + prune_passive passive + else + passive + in + match passive_is_empty passive with | true -> Failure | false -> @@ -707,6 +821,7 @@ let main () = print_endline "--------------------------------------------------"; let start = Unix.gettimeofday () in print_endline "GO!"; + start_time := Unix.gettimeofday (); let res = !given_clause_ref env passive active in let finish = Unix.gettimeofday () in match res with @@ -727,6 +842,7 @@ let main () = Printf.printf "Success, but no proof?!?\n\n" with exc -> print_endline ("EXCEPTION: " ^ (Printexc.to_string exc)); + raise exc ;; @@ -739,7 +855,7 @@ let _ = 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_use_index v = Indexing.use_index := v + and set_time_limit v = time_limit := float_of_int v in Arg.parse [ "-f", Arg.Unit set_fullred, "Use full-reduction strategy"; @@ -755,7 +871,7 @@ let _ = "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)"; - "-i", Arg.Bool set_use_index, "Use indexing yes/no (default: yes)"; + "-l", Arg.Int set_time_limit, "Time limit (in seconds)"; ] (fun a -> ()) "Usage:" in Helm_registry.load_from !configuration_file; -- 2.39.2