Added more precise time information

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 8530be3e8b571b14c01ef6d65e28ed1c5a172091..4968d3290030c7e1b47441bf79d2b9242006db7f 100644 (file)
--- 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 0fc1f750a6cc16d8fc99adfc75215157e06e9b13..554028fa75b857c3c10ccadf73d6d5cf825404a7 100644 (file)
--- 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
     ;;