From: Alberto Griggio <griggio@fbk.eu>
Date: Sun, 19 Jun 2005 10:09:42 +0000 (+0000)
Subject: path indexing integration, limited-resource-strategy implementation (not yet working)
X-Git-Tag: INDEXING_NO_PROOFS~113
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eb29eb8e516abf6791aadc91d1ba7ea2e403614f;p=helm.git

path indexing integration, limited-resource-strategy implementation (not yet working)
---

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;