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