From 754f74638de5c287c849dc72494143b1da82cd88 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 4 Mar 2010 07:55:14 +0000 Subject: [PATCH] Small changes for debugging --- helm/software/components/ng_paramodulation/paramod.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 0558e89c7..8abdaaec5 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -12,8 +12,8 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) let print s = prerr_endline (Lazy.force s) ;; -(* let debug = print *) -let debug s = ();; +let noprint s = ();; +let debug = noprint;; let monster = 100;; @@ -346,12 +346,12 @@ module Paramod (B : Orderings.Blob) = struct (Unix.gettimeofday()))); let actives_l, active_t = actives in let passive_t,wset,_ = passives in - let _ = debug + let _ = noprint (lazy ("Actives :" ^ (String.concat ";\n" (List.map Pp.pp_unit_clause actives_l)))) in let wset = IDX.elems passive_t in - let _ = debug + let _ = noprint (lazy ("Passives:" ^(String.concat ";\n" (List.map (fun _,cl -> Pp.pp_unit_clause cl) @@ -452,7 +452,7 @@ module Paramod (B : Orderings.Blob) = struct Sup.simplify_goal ~no_demod maxvar (snd actives) bag g_actives current with - | None -> status + | None -> debug (lazy "None"); status | Some (bag,g_current) -> let _ = debug (lazy("Infer on goal : " -- 2.39.2