X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=a1414de795bb1311145c22cf3bedbcd71aff9d72;hb=ab0954eab207a70e6ad5f2991cc117608deff55b;hp=372127b48d9b234c97b8d009aeccf10fe0655dca;hpb=44b3d34ddcc81a5e008cc8be7db102139af1d907;p=helm.git

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 372127b48..a1414de79 100644
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -1,6 +1,35 @@
 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_weight = ref None;;
+(* 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;;
+let symbols_counter = ref 0;;
+
+(* statistics... *)
+let derived_clauses = ref 0;;
+let kept_clauses = 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 +62,13 @@ let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) =
 ;;
 
 
-module OrderedEquality =
-struct
+let weight_of_equality (_, (ty, left, right, _), _, _) =
+  let weight_of t = fst (weight_of_term ~consider_metas:false t) in
+  (weight_of ty) + (weight_of left) + (weight_of right)
+;;
+
+
+module OrderedEquality = struct
   type t = Inference.equality
 
   let compare eq1 eq2 =
@@ -46,6 +80,8 @@ struct
         let weight_of t = fst (weight_of_term ~consider_metas:false t) in
         let w1 = (weight_of ty) + (weight_of left) + (weight_of right)
         and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in
+(*         let w1 = weight_of_equality eq1 *)
+(*         and w2 = weight_of_equality eq2 in *)
         match Pervasives.compare w1 w2 with
         | 0 -> Pervasives.compare eq1 eq2
         | res -> res
@@ -54,14 +90,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
@@ -77,7 +108,11 @@ let select env passive (active, _) =
           (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
@@ -91,21 +126,19 @@ 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
-(*             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)
@@ -113,33 +146,33 @@ 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
           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 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
     )
@@ -152,6 +185,8 @@ let select env passive (active, _) =
           (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
@@ -169,15 +204,23 @@ 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 =
+      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 make_active () =
-  [], Hashtbl.create 1
+  [], Indexing.empty_table () 
 ;;
 
 
@@ -186,12 +229,19 @@ let add_to_passive passive (new_neg, new_pos) =
   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
 ;;
 
 
@@ -201,33 +251,151 @@ 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 size_of_active (active_list, _) =
+  List.length active_list
+;;
+
+
+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 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
+      EqualitySet.empty, EqualitySet.empty
+  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
+      | [] -> 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, l
+  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_weight := Some (weight_of_equality (EqualitySet.max_elt ps));
+(*     maximal_retained_equality := Some (EqualitySet.max_elt ps); *)
+  let tbl =
+    EqualitySet.fold
+      (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  
+;;
+
 
 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
+  derived_clauses := !derived_clauses + (List.length new_neg) +
+    (List.length new_pos);
+  match !maximal_weight(* !maximal_retained_equality *) with
+  | None -> new_neg, new_pos
+  | Some w (* eq *) ->
+      let new_pos =
+        List.filter (fun e -> (weight_of_equality e) <= w (* OrderedEquality.compare e eq <= 0 *)) new_pos in
+      new_neg, new_pos
 ;;
 
 
@@ -255,14 +423,15 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
         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
@@ -283,20 +452,59 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
   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
-        let pred (sign, eq) =
-          if sign <> s then false
-          else subsumption env c eq
-        in
-        if List.exists pred all 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 *)
+(*           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 = {
+  mutable build_all: float;
+  mutable demodulate: float;
+  mutable subsumption: float;
+};;
+
+let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };;
+
 
 let forward_simplify_new env (new_neg, new_pos) ?passive active =
+  let t1 = Unix.gettimeofday () in
+
   let active_list, active_table = active in
   let pl, passive_table =
     match passive with
@@ -307,11 +515,22 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
         pn @ pp, Some pt
   in
   let all = active_list @ pl in
+  
+  let t2 = Unix.gettimeofday () in
+  fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1);
+  
   let demodulate table target =
     let newmeta, newtarget = Indexing.demodulation !maxmeta env table target in
     maxmeta := newmeta;
     newtarget
   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 =
     let new_neg = List.map (demodulate active_table) new_neg
     and new_pos = List.map (demodulate active_table) new_pos in
@@ -321,6 +540,10 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
         List.map (demodulate passive_table) new_neg,
         List.map (demodulate passive_table) new_pos
   in
+
+  let t2 = Unix.gettimeofday () in
+  fs_time_info.demodulate <- fs_time_info.demodulate +. (t2 -. t1);
+
   let new_pos_set =
     List.fold_left
       (fun s e ->
@@ -328,12 +551,47 @@ 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 f sign' target (sign, eq) =
-    if sign <> sign' then false
-    else subsumption env target eq 
+
+(*   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);
+
+  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
-  (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)
+  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) *)
+(*   in *)
+(*   res *)
 ;;
 
 
@@ -342,7 +600,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
@@ -366,7 +624,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
@@ -386,7 +644,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) =
@@ -403,7 +661,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
@@ -422,8 +680,36 @@ let backward_simplify env new' ?passive active =
       active, passive, newa, newp
 ;;
 
+
+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 *. 2.) /. !elapsed_time -. 1.)))
+;;
+
   
 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. || !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
+
+  kept_clauses := (size_of_passive passive) + (size_of_active active);
+    
   match passive_is_empty passive with
   | true -> Failure
   | false ->
@@ -444,19 +730,31 @@ let rec given_clause env passive active =
               (string_of_sign sign) (string_of_equality ~env current);
             print_newline ();
 
+            let t1 = Unix.gettimeofday () in
             let new' = infer env sign current active in
+            let t2 = Unix.gettimeofday () in
+            infer_time := !infer_time +. (t2 -. t1);
+            
             let res, proof = contains_empty env new' in
             if res then
               Success (proof, env)
-            else
-              let new' = forward_simplify_new env new' active in
+            else 
+              let t1 = Unix.gettimeofday () 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)
+              in
               let active =
                 match sign with
                 | Negative -> active
                 | Positive ->
+                    let t1 = Unix.gettimeofday () in
                     let active, _, newa, _ =
                       backward_simplify env ([], [current]) active
                     in
+                    let t2 = Unix.gettimeofday () in
+                    backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
                     match newa with
                     | None -> active
                     | Some (n, p) ->
@@ -471,27 +769,27 @@ let rec given_clause env passive active =
                         in
                         nn @ al @ pp, tbl
               in
-              let _ =
-                Printf.printf "active:\n%s\n"
-                  (String.concat "\n"
-                     ((List.map
-                         (fun (s, e) -> (string_of_sign s) ^ " " ^
-                            (string_of_equality ~env e)) (fst active))));
-                print_newline ();
-              in
-              let _ =
-                match new' with
-                | neg, pos ->
-                    Printf.printf "new':\n%s\n"
-                      (String.concat "\n"
-                         ((List.map
-                             (fun e -> "Negative " ^
-                                (string_of_equality ~env e)) neg) @
-                            (List.map
-                               (fun e -> "Positive " ^
-                                  (string_of_equality ~env e)) pos)));
-                    print_newline ();
-              in
+(*               let _ = *)
+(*                 Printf.printf "active:\n%s\n" *)
+(*                   (String.concat "\n" *)
+(*                      ((List.map *)
+(*                          (fun (s, e) -> (string_of_sign s) ^ " " ^ *)
+(*                             (string_of_equality ~env e)) (fst active)))); *)
+(*                 print_newline (); *)
+(*               in *)
+(*               let _ = *)
+(*                 match new' with *)
+(*                 | neg, pos -> *)
+(*                     Printf.printf "new':\n%s\n" *)
+(*                       (String.concat "\n" *)
+(*                          ((List.map *)
+(*                              (fun e -> "Negative " ^ *)
+(*                                 (string_of_equality ~env e)) neg) @ *)
+(*                             (List.map *)
+(*                                (fun e -> "Positive " ^ *)
+(*                                   (string_of_equality ~env e)) pos))); *)
+(*                     print_newline (); *)
+(*               in *)
               match contains_empty env new' with
               | false, _ -> 
                   let active =
@@ -502,16 +800,16 @@ let rec given_clause env passive active =
                         al @ [(sign, current)], Indexing.index tbl current
                   in
                   let passive = add_to_passive passive new' in
-                  let (_, ns), (_, ps), _ = passive in
-                  Printf.printf "passive:\n%s\n"
-                    (String.concat "\n"
-                       ((List.map (fun e -> "Negative " ^
-                                     (string_of_equality ~env e))
-                           (EqualitySet.elements ns)) @
-                          (List.map (fun e -> "Positive " ^
-                                       (string_of_equality ~env e))
-                             (EqualitySet.elements ps))));
-                  print_newline ();
+(*                   let (_, ns), (_, ps), _ = passive in *)
+(*                   Printf.printf "passive:\n%s\n" *)
+(*                     (String.concat "\n" *)
+(*                        ((List.map (fun e -> "Negative " ^ *)
+(*                                      (string_of_equality ~env e)) *)
+(*                            (EqualitySet.elements ns)) @ *)
+(*                           (List.map (fun e -> "Positive " ^ *)
+(*                                        (string_of_equality ~env e)) *)
+(*                              (EqualitySet.elements ps)))); *)
+(*                   print_newline (); *)
                   given_clause env passive active
               | true, proof ->
                   Success (proof, env)
@@ -520,6 +818,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 ->
@@ -540,7 +855,10 @@ let rec given_clause_fullred env passive active =
               (string_of_sign sign) (string_of_equality ~env current);
             print_newline ();
 
+            let t1 = Unix.gettimeofday () in
             let new' = infer env sign current active in
+            let t2 = Unix.gettimeofday () in
+            infer_time := !infer_time +. (t2 -. t1);
 
             let active =
               if is_identity env current then active
@@ -551,10 +869,15 @@ let rec given_clause_fullred env passive active =
                 | Positive -> al @ [(sign, current)], Indexing.index tbl current
             in
             let rec simplify new' active passive =
+              let t1 = Unix.gettimeofday () in
               let new' = forward_simplify_new env new' ~passive active in
+              let t2 = Unix.gettimeofday () in
+              forward_simpl_time := !forward_simpl_time +. (t2 -. t1);
+              let t1 = Unix.gettimeofday () in
               let active, passive, newa, retained =
-                backward_simplify env new' ~passive active
-              in
+                backward_simplify env new' ~passive active in
+              let t2 = Unix.gettimeofday () in
+              backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
               match newa, retained with
               | None, None -> active, passive, new'
               | Some (n, p), None
@@ -566,6 +889,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"
@@ -648,19 +976,41 @@ let main () =
     print_endline "--------------------------------------------------";
     let start = Unix.gettimeofday () in
     print_endline "GO!";
-    let res = !given_clause_ref env passive active in
+    start_time := Unix.gettimeofday ();
+    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 "NO proof found! :-(\n\n"
-    | Success (Some proof, env) ->
-        Printf.printf "OK, found a proof!:\n%s\n%.9f\n"
-          (PP.pp proof (names_of_context context))
-          (finish -. start);
-    | Success (None, env) ->
-        Printf.printf "Success, but no proof?!?\n\n"
+    let _ =
+      match res with
+      | Failure ->
+          Printf.printf "NO proof found! :-(\n\n"
+      | Success (Some proof, env) ->
+          Printf.printf "OK, found a proof!:\n%s\n%.9f\n"
+            (PP.pp proof (names_of_context context))
+            (finish -. start);
+(*         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"
+    in
+    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 "successful unification/matching time: %.9f\n"
+      !Indexing.match_unif_time_ok;
+    Printf.printf "failed unification/matching time: %.9f\n"
+      !Indexing.match_unif_time_no;
+    Printf.printf "indexing retrieval time: %.9f\n"
+      !Indexing.indexing_retrieval_time;
+    Printf.printf "derived %d clauses, kept %d clauses.\n"
+      !derived_clauses !kept_clauses;
   with exc ->
     print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
+    raise exc
 ;;
 
 
@@ -672,7 +1022,8 @@ let _ =
   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 [
     "-f", Arg.Unit set_fullred, "Use full-reduction strategy";
@@ -687,6 +1038,8 @@ let _ =
     "-lpo", Arg.Unit set_lpo, "Use lpo term ordering";
 
     "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)";
+
+    "-l", Arg.Int set_time_limit, "Time limit (in seconds)";
   ] (fun a -> ()) "Usage:"
 in
 Helm_registry.load_from !configuration_file;