X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=c933aec0b48c3c11115d8d8346302f1144c93892;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=634df11ffb4a766f6ca18080f55197dcd815b3dd;hpb=bdc855b1b6c9552a49a01769cb906a438ca60cc4;p=helm.git

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 634df11ff..c933aec0b 100644
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -5,13 +5,16 @@ open Utils;;
 (* profiling statistics... *)
 let infer_time = ref 0.;;
 let forward_simpl_time = ref 0.;;
+let forward_simpl_new_time = ref 0.;;
 let backward_simpl_time = ref 0.;;
+let passive_maintainance_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 *)
@@ -21,13 +24,17 @@ 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
+  | Success of Inference.equality option * environment
 ;;
 
 
@@ -37,7 +44,7 @@ let symbols_of_equality (_, (_, left, right), _, _) =
 ;;
 *)
 
-let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) =
+let symbols_of_equality ((_, _, (_, left, right, _), _, _) as equality) =
   let m1 = symbols_of_term left in
   let m = 
     TermMap.fold
@@ -64,13 +71,25 @@ module OrderedEquality = struct
     match meta_convertibility_eq eq1 eq2 with
     | true -> 0
     | false ->
-        let _, (ty, left, right, _), _, _ = eq1
-        and _, (ty', left', right', _), _, _ = eq2 in
-        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, _, (ty, left, right, _), _, a = eq1
+        and w2, _, (ty', left', right', _), _, a' = eq2 in
+(*         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 *)
         match Pervasives.compare w1 w2 with
-        | 0 -> Pervasives.compare eq1 eq2
+        | 0 ->
+            let res = (List.length a) - (List.length a') in
+            if res <> 0 then res else (
+              try
+                let res = Pervasives.compare (List.hd a) (List.hd a') in
+                if res <> 0 then res else Pervasives.compare eq1 eq2
+              with _ -> Pervasives.compare eq1 eq2
+(*               match a, a' with *)
+(*               | (Cic.Meta (i, _)::_), (Cic.Meta (j, _)::_) -> *)
+(*                   let res = Pervasives.compare i j in *)
+(*                   if res <> 0 then res else Pervasives.compare eq1 eq2 *)
+(*               | _, _ -> Pervasives.compare eq1 eq2 *)
+            )
         | res -> res
 end
 
@@ -128,6 +147,10 @@ let select env passive (active, _) =
             in
             let c = others + (abs (common - card)) in
             if c < i then (c, equality)
+(*             else if c = i then *)
+(*               match OrderedEquality.compare equality e with *)
+(*               | -1 -> (c, equality) *)
+(*               | res -> (i, e) *)
             else (i, e)
           in
           let e1 = EqualitySet.min_elt pos_set in
@@ -243,6 +266,11 @@ let size_of_passive ((_, ns), (_, 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
@@ -324,11 +352,12 @@ let prune_passive howmany (active, _) passive =
           let w, s, l = picka w s tl in
           w, s, hd::l
     else
-      0, s, []
+      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
@@ -369,11 +398,13 @@ let infer env sign current (active_list, active_table) =
         let neg, pos = infer_positive curr_table active_list in
         neg, res @ pos
   in
-  match !maximal_retained_equality with
+  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 eq ->
+  | Some (* w *) eq ->
       let new_pos =
-        List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos in
+        List.filter (fun e -> (* (weight_of_equality e) <= w *) OrderedEquality.compare e eq <= 0) new_pos in
       new_neg, new_pos
 ;;
 
@@ -381,13 +412,13 @@ let infer env sign current (active_list, active_table) =
 let contains_empty env (negative, positive) =
   let metasenv, context, ugraph = env in
   try
-    let (proof, _, _, _) =
+    let found =
       List.find
-        (fun (proof, (ty, left, right, ordering), m, a) ->
+        (fun (w, proof, (ty, left, right, ordering), m, a) ->
            fst (CicReduction.are_convertible context left right ugraph))
         negative
     in
-    true, Some proof
+    true, Some found
   with Not_found ->
     false, None
 ;;
@@ -411,12 +442,24 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
 (*         else find_duplicate sign current tl *)
 (*     | _::tl -> find_duplicate sign current tl *)
 (*   in *)
+
+(*   let res =  *)
+(*     if sign = Positive then *)
+(*       Indexing.subsumption env active_table current *)
+(*     else *)
+(*       false *)
+(*   in *)
+(*   if res then *)
+(*     None *)
+(*   else *)
+  
   let demodulate table current = 
     let newmeta, newcurrent =
       Indexing.demodulation !maxmeta env table current in
     maxmeta := newmeta;
     if is_identity env newcurrent then
-      if sign = Negative then Some (sign, newcurrent) else None
+      if sign = Negative then Some (sign, newcurrent)
+      else None
     else
       Some (sign, newcurrent)
   in
@@ -445,7 +488,8 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
         match passive_table with
         | None -> res
         | Some passive_table ->
-            if Indexing.in_index passive_table c then None else res
+            if Indexing.in_index passive_table c then None
+            else res
 
 (*   | Some (s, c) -> if find_duplicate s c all then None else res *)
 
@@ -526,19 +570,22 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
   let new_pos_set =
     List.fold_left
       (fun s e ->
-         if not (Inference.is_identity env e) then EqualitySet.add e s else s)
+         if not (Inference.is_identity env e) then
+           if EqualitySet.mem e s then s
+           else EqualitySet.add e s
+         else s)
       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 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
 
@@ -557,10 +604,12 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
 
   let is_duplicate =
     match passive_table with
-    | None -> (fun e -> not (Indexing.in_index active_table e))
+    | 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)))
+        (fun e ->
+           not ((Indexing.in_index active_table e) ||
+                  (Indexing.in_index passive_table e)))
   in
   new_neg, List.filter is_duplicate new_pos
 
@@ -574,13 +623,8 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
 ;;
 
 
-let backward_simplify_active env (new_neg, new_pos) active =
+let backward_simplify_active env new_pos new_table active =
   let active_list, active_table = active in
-  let new_pos, new_table =
-    List.fold_left
-      (fun (l, t) e -> (Positive, e)::l, Indexing.index t e)
-      ([], Indexing.empty_table ()) new_pos
-  in
   let active_list, newa = 
     List.fold_right
       (fun (s, equality) (res, newn) ->
@@ -599,16 +643,20 @@ let backward_simplify_active env (new_neg, new_pos) active =
   let active, newa =
     List.fold_right
       (fun (s, eq) (res, tbl) ->
-         if (is_identity env eq) || (find eq res) then
+         if List.mem (s, eq) res then
+           res, tbl
+         else if (is_identity env eq) || (find eq res) then (
            res, tbl
+         ) (* else if (find eq res) then *)
+(*            res, tbl *)
          else
            (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
       active_list ([], Indexing.empty_table ()),
     List.fold_right
       (fun (s, eq) (n, p) ->
-         if (s <> Negative) && (is_identity env eq) then
+         if (s <> Negative) && (is_identity env eq) then (
            (n, p)
-         else
+         ) else
            if s = Negative then eq::n, p
            else n, eq::p)
       newa ([], [])
@@ -619,12 +667,7 @@ let backward_simplify_active env (new_neg, new_pos) active =
 ;;
 
 
-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)
-      ([], Indexing.empty_table ()) new_pos
-  in
+let backward_simplify_passive env new_pos new_table passive =
   let (nl, ns), (pl, ps), passive_table = passive in
   let f sign equality (resl, ress, newn) =
     match forward_simplify env (sign, equality) (new_pos, new_table) with
@@ -649,26 +692,34 @@ let backward_simplify_passive env (new_neg, new_pos) passive =
 
 
 let backward_simplify env new' ?passive active =
-  let active, newa = backward_simplify_active env new' active in
+  let new_pos, new_table =
+    List.fold_left
+      (fun (l, t) e -> (Positive, e)::l, Indexing.index t e)
+      ([], Indexing.empty_table ()) (snd new')
+  in    
+  let active, newa = backward_simplify_active env new_pos new_table active in
   match passive with
   | None ->
       active, (make_passive [] []), newa, None
   | Some passive ->
       let passive, newp =
-        backward_simplify_passive env new' passive in
+        backward_simplify_passive env new_pos new_table passive in
       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 /. !elapsed_time -. 1.)))
+            ((!time_limit (* *. 2. *)) /. !elapsed_time -. 1.)))
 ;;
 
   
 let rec given_clause env passive active =
+  let time1 = Unix.gettimeofday () in
+
   let selection_estimate = get_selection_estimate () in
   let kept = size_of_passive passive in
   let passive =
@@ -685,12 +736,21 @@ let rec given_clause env passive active =
     ) else
       passive
   in
+
+  let time2 = Unix.gettimeofday () in
+  passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
+
+  kept_clauses := (size_of_passive passive) + (size_of_active active);
     
   match passive_is_empty passive with
   | true -> Failure
   | false ->
       let (sign, current), passive = select env passive active in
-      match forward_simplify env (sign, current) ~passive active with
+      let time1 = Unix.gettimeofday () in
+      let res = forward_simplify env (sign, current) ~passive active in
+      let time2 = Unix.gettimeofday () in
+      forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
+      match res with
       | None ->
           given_clause env passive active
       | Some (sign, current) ->
@@ -698,8 +758,7 @@ let rec given_clause env passive active =
             Printf.printf "OK!!! %s %s" (string_of_sign sign)
               (string_of_equality ~env current);
             print_newline ();
-            let proof, _, _, _ = current in
-            Success (Some proof, env)
+            Success (Some current, env)
           ) else (            
             print_endline "\n================================================";
             Printf.printf "selected: %s %s"
@@ -711,15 +770,15 @@ let rec given_clause env passive active =
             let t2 = Unix.gettimeofday () in
             infer_time := !infer_time +. (t2 -. t1);
             
-            let res, proof = contains_empty env new' in
+            let res, goal = contains_empty env new' in
             if res then
-              Success (proof, env)
+              Success (goal, env)
             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)
+                forward_simpl_new_time := !forward_simpl_new_time +. (t2 -. t1)
               in
               let active =
                 match sign with
@@ -745,27 +804,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 =
@@ -776,24 +835,26 @@ 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)
+              | true, goal ->
+                  Success (goal, env)
           )
 ;;
 
 
 let rec given_clause_fullred env passive active =
+  let time1 = Unix.gettimeofday () in
+  
   let selection_estimate = get_selection_estimate () in
   let kept = size_of_passive passive in
   let passive =
@@ -810,12 +871,21 @@ let rec given_clause_fullred env passive active =
     ) else
       passive
   in
+
+  let time2 = Unix.gettimeofday () in
+  passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
     
+  kept_clauses := (size_of_passive passive) + (size_of_active active);
+
   match passive_is_empty passive with
   | true -> Failure
   | false ->
       let (sign, current), passive = select env passive active in
-      match forward_simplify env (sign, current) ~passive active with
+      let time1 = Unix.gettimeofday () in
+      let res = forward_simplify env (sign, current) ~passive active in
+      let time2 = Unix.gettimeofday () in
+      forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
+      match res with
       | None ->
           given_clause_fullred env passive active
       | Some (sign, current) ->
@@ -823,8 +893,7 @@ let rec given_clause_fullred env passive active =
             Printf.printf "OK!!! %s %s" (string_of_sign sign)
               (string_of_equality ~env current);
             print_newline ();
-            let proof, _, _, _ = current in
-            Success (Some proof, env)
+            Success (Some current, env)
           ) else (
             print_endline "\n================================================";
             Printf.printf "selected: %s %s"
@@ -848,7 +917,7 @@ let rec given_clause_fullred env passive active =
               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);
+              forward_simpl_new_time := !forward_simpl_new_time +. (t2 -. t1);
               let t1 = Unix.gettimeofday () in
               let active, passive, newa, retained =
                 backward_simplify env new' ~passive active in
@@ -870,33 +939,33 @@ let rec given_clause_fullred env passive active =
             if k < (kept - 1) then
               processed_clauses := !processed_clauses + (kept - 1 - k);
             
-            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 passive = add_to_passive passive new' in
                 given_clause_fullred env passive active
-            | true, proof ->
-                Success (proof, env)
+            | true, goal ->
+                Success (goal, env)
           )
 ;;
 
@@ -937,7 +1006,7 @@ let main () =
   let env = (metasenv, context, ugraph) in
   try
     let term_equality = equality_of_term meta_proof goal in
-    let meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
+    let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
     let active = make_active () in
     let passive = make_passive [term_equality] equalities in
     Printf.printf "\ncurrent goal: %s\n"
@@ -958,22 +1027,35 @@ let main () =
         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);
-        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; *)
-    | 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 goal, env) ->
+          Printf.printf "OK, found a proof!\n";
+          let proof = Inference.build_term_proof goal in
+          print_endline (PP.pp proof (names_of_context context));
+          print_endline (string_of_float (finish -. start));
+      | Success (None, env) ->
+          Printf.printf "Success, but no proof?!?\n\n"
+    in
+    Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
+                     "forward_simpl_new_time: %.9f\n" ^^
+                     "backward_simpl_time: %.9f\n")
+      !infer_time !forward_simpl_time !forward_simpl_new_time
+      !backward_simpl_time;
+    Printf.printf "passive_maintainance_time: %.9f\n"
+      !passive_maintainance_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 "    demodulate_term.build_newtarget_time: %.9f\n"
+      !Indexing.build_newtarget_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