From cb1b4380e7133a0a7a0f22c667afbb6abd0de410 Mon Sep 17 00:00:00 2001
From: denes <??>
Date: Mon, 22 Jun 2009 17:12:49 +0000
Subject: [PATCH] Added more precise time information

---
 helm/software/components/ng_paramodulation/paramod.ml    | 9 ++++++---
 .../components/ng_paramodulation/superposition.ml        | 4 ++--
 2 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 8530be3e8..4968d3290 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -1,7 +1,7 @@
 (* LOOPING : COL057-1.ma *)
 
 let debug s =
-  prerr_endline s
+  () (* prerr_endline s *)
 ;;
 
 let nparamod rdb metasenv subst context t table =
@@ -182,12 +182,15 @@ let nparamod rdb metasenv subst context t table =
 	let gsteps,esteps = traverse true ([],[]) i in
 	  (List.rev esteps)@gsteps
       in
-	prerr_endline (Printf.sprintf "Found proof in %d iterations" !nb_iter);
+	prerr_endline (Printf.sprintf "Found proof in %d iterations, %fs"
+			 !nb_iter
+			 (Unix.gettimeofday() -. timeout +. amount_of_time));
       (* prerr_endline "Proof:"; 
       List.iter (fun x -> prerr_endline (string_of_int x);
               prerr_endline (Pp.pp_unit_clause (Terms.M.find x bag))) l;*)
       let proofterm = B.mk_proof bag i l in
-	prerr_endline "Got proof term";
+	prerr_endline (Printf.sprintf "Got proof term, %fs"
+			 (Unix.gettimeofday() -. timeout +. amount_of_time));
       let metasenv, proofterm = 
         let rec aux k metasenv = function
           | NCic.Meta _ as t -> metasenv, t
diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 0fc1f750a..554028fa7 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -450,7 +450,7 @@ module Superposition (B : Terms.Blob) =
       let bag, maxvar, new_goals =	
         superposition_with_table bag maxvar goal atable 
       in
-	prerr_endline "Superposed goal with active clauses";
+	debug "Superposed goal with active clauses";
 	(* We demodulate the goal with active clauses *)
       let bag, new_goals = 
         List.fold_left
@@ -459,7 +459,7 @@ module Superposition (B : Terms.Blob) =
             bag, g :: acc) 
          (bag, []) new_goals
       in
-	prerr_endline "Demodulated goal with active clauses";
+	debug "Demodulated goal with active clauses";
       bag, maxvar, List.rev new_goals
     ;;
 
-- 
2.39.2