From: denes Date: Fri, 24 Jul 2009 13:26:36 +0000 (+0000) Subject: Fixed pretty printer and debug printings X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4693f3b9de6d867921b51f61e9a7dc36c3da1b77;p=helm.git Fixed pretty printer and debug printings --- diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml index aa77e0c5a..3736c024d 100644 --- a/helm/software/components/binaries/matitaprover/matitaprover.ml +++ b/helm/software/components/binaries/matitaprover/matitaprover.ml @@ -289,7 +289,7 @@ usage: matitaprover [options] problemfile"; ; (fun () -> worker `KBO ~useage:true ~printmsg:false goal hypotheses) ; - (fun () -> worker `LPO ~useage:true ~printmsg:true goal hypotheses) + (fun () -> worker `LPO ~useage:true ~printmsg:false goal hypotheses) ; (fun () -> worker `NRKBO ~useage:false ~printmsg:false goal hypotheses) ]; diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml index 6f36d5939..7b192579d 100644 --- a/helm/software/components/ng_paramodulation/foUtils.ml +++ b/helm/software/components/ng_paramodulation/foUtils.ml @@ -109,8 +109,8 @@ module Utils (B : Orderings.Blob) = struct match ty with | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq -> let o = Order.compare_terms l r in - (vars,(Terms.Equation (l, r, ty, o),false)::literals) - | _ -> (vars,(Terms.Predicate ty,false)::literals) + (vars,(Terms.Equation (l, r, ty, o),true)::literals) + | _ -> (vars,(Terms.Predicate ty,true)::literals) in let varlist = Terms.vars_of_term proofterm in let (varlist,nlit) = List.fold_left foterm_to_lit (varlist,[]) nlit in diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index d65fce1b2..48811239b 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -11,7 +11,7 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) -let debug s = prerr_endline s ;; +let debug s = prerr_endline (Lazy.force s) ;; let debug _ = ();; let monster = 100;; @@ -162,11 +162,11 @@ module Paramod (B : Orderings.Blob) = struct let backward_infer_step bag maxvar actives passives g_actives g_passives g_current iterno = (* superposition left, simplifications on goals *) - debug "infer_left step..."; + debug (lazy "infer_left step..."); let bag, maxvar, new_goals = Sup.infer_left bag maxvar g_current actives in - debug "Performed infer_left step"; + debug (lazy "Performed infer_left step"); let bag = Terms.replace_in_bag (g_current,false,iterno) bag in bag, maxvar, actives, passives, g_current::g_actives, (add_passive_goals g_passives new_goals) @@ -184,12 +184,12 @@ module Paramod (B : Orderings.Blob) = struct * new = supright e'' A'' * * new'= demod A'' new * * P' = P + new' *) - debug "Forward infer step..."; + debug (lazy "Forward infer step..."); debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives))))); let bag, maxvar, actives, new_clauses = Sup.infer_right bag maxvar current actives in - debug "Demodulating goals with actives..."; + debug (lazy "Demodulating goals with actives..."); (* keep goals demodulated w.r.t. actives and check if solved *) let bag, g_actives = List.fold_left @@ -294,7 +294,7 @@ module Paramod (B : Orderings.Blob) = struct if weight > monster then bag,None else bag, Some (current,actives) else if Sup.orphan_murder bag (fst actives) current then - let _ = debug "Orphan murdered" in + let _ = debug (lazy "Orphan murdered") in let bag = Terms.replace_in_bag (current,true,iterno) bag in bag, None else Sup.keep_simplified current actives bag maxvar @@ -328,7 +328,6 @@ module Paramod (B : Orderings.Blob) = struct (*prerr_endline "Active table :"; (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x)) (fst actives)); *) - let bag,maxvar,actives,passives,g_actives,g_passives = aux_select bag passives g_passives in diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml index 061dae2b1..d93fade27 100644 --- a/helm/software/components/ng_paramodulation/pp.ml +++ b/helm/software/components/ng_paramodulation/pp.ml @@ -87,20 +87,12 @@ let string_of_comparison = function | Terms.Incomparable -> "=?=" | Terms.Invertible -> "=<->=" -(*let pp_literal ~formatter:f l = - match l with +let pp_literal ~formatter:f l = + match fst l with | Terms.Predicate t -> Format.fprintf f "@[{"; pp_foterm f t; - Format.fprintf f "@;[%s] by " - (String.concat ", " (List.map string_of_int vars)); - (match proof with - | Terms.Exact t -> pp_foterm f t - | Terms.Step (rule, id1, id2, _, p, _) -> - Format.fprintf f "%s %d with %d at %s" - (string_of_rule rule) id1 id2 (String.concat - "," (List.map string_of_int p))); - Format.fprintf f "@]" + Format.fprintf f "}@;" | Terms.Equation (lhs, rhs, ty, comp) -> Format.fprintf f "@[{"; pp_foterm f ty; @@ -108,16 +100,8 @@ let string_of_comparison = function pp_foterm f lhs; Format.fprintf f "@;%s@;" (string_of_comparison comp); pp_foterm f rhs; - Format.fprintf f "@]@;[%s] by " - (String.concat ", " (List.map string_of_int vars)); - (match proof with - | Terms.Exact t -> pp_foterm f t - | Terms.Step (rule, id1, id2, _, p, _) -> - Format.fprintf f "%s %d with %d at %s" - (string_of_rule rule) id1 id2 (String.concat - "," (List.map string_of_int p))); - Format.fprintf f "@]" -*) + Format.fprintf f "@]@;" +;; let pp_unit_clause ~formatter:f c = let (id, l, vars, proof) = c in @@ -150,11 +134,28 @@ let pp_unit_clause ~formatter:f c = Format.fprintf f "%s %d with %d at %s" (string_of_rule rule) id1 id2 (String.concat "," (List.map string_of_int p))); - Format.fprintf f "@]" + Format.fprintf f "@]" ;; let pp_clause ~formatter:f c = - assert false + let (id, nlit, plit, vars, proof) = c in + Format.fprintf f "Id : %3d, " id ; + let pr_literals l = + if l <> [] then begin + pp_literal f (List.hd l); + List.iter (fun lit -> Format.fprintf f "\\/"; pp_literal f lit) (List.tl l); + end + in + pr_literals nlit; + Format.fprintf f " -> "; + pr_literals plit; + Format.fprintf f "[%s] by " (String.concat ", " (List.map string_of_int vars)); + match proof with + | Terms.Exact t -> pp_foterm f t + | Terms.Step (rule, id1, id2, _, p, _) -> + Format.fprintf f "%s %d with %d at %s" + (string_of_rule rule) id1 id2 (String.concat + "," (List.map string_of_int p)) ;; let pp_bag ~formatter:f (_,bag) = diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 0dbac61c3..67df0654e 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -22,7 +22,7 @@ module Superposition (B : Orderings.Blob) = exception Success of B.t Terms.bag * int * B.t Terms.clause - let debug s = prerr_endline s;; + let debug s = prerr_endline (Lazy.force s);; let debug _ = ();; let enable = true;; @@ -410,7 +410,7 @@ module Superposition (B : Orderings.Blob) = let (id,_,_,_,_) = cl in let actives = List.map (fun (i,_,_,_,_) -> i) actives in let (res,_) = orphan_murder bag actives id in - if res then debug "Orphan murdered"; res + if res then debug (lazy "Orphan murdered"); res ;; let prof_orphan_murder = HExtlib.profile ~enable "orphan_murder";; let orphan_murder bag actives x = @@ -588,6 +588,7 @@ module Superposition (B : Orderings.Blob) = (* this is OK for both the sup_left and sup_right inference steps *) let superposition table varlist subterm pos context = let cands = IDX.DT.retrieve_unifiables table subterm in + debug (lazy (string_of_int (IDX.ClauseSet.cardinal cands) ^ " candidates found")); HExtlib.filter_map (fun (dir, _, _, (id,nlit,plit,vl,_ (*as uc*))) -> match nlit,plit with @@ -669,7 +670,7 @@ module Superposition (B : Orderings.Blob) = in bag, (alist, List.fold_left IDX.index_clause IDX.DT.empty alist) in*) - debug "Simplified active clauses with fact"; + debug (lazy "Simplified active clauses with fact"); (* We superpose active clauses with current *) let bag, maxvar, new_clauses = List.fold_left @@ -680,13 +681,13 @@ module Superposition (B : Orderings.Blob) = bag, maxvar, newc @ acc) (bag, maxvar, []) alist in - debug "First superpositions"; + debug (lazy "First superpositions"); (* We add current to active clauses so that it can be * * superposed with itself *) let alist, atable = current :: alist, IDX.index_clause atable current in - debug "Indexed"; + debug (lazy "Indexed"); let fresh_current, maxvar = Utils.fresh_clause maxvar current in (* We need to put fresh_current into the bag so that all * * variables clauses refer to are known. *) @@ -695,14 +696,14 @@ module Superposition (B : Orderings.Blob) = let bag, maxvar, additional_new_clauses = superposition_with_table bag maxvar fresh_current atable in - debug "Another superposition"; + debug (lazy "Another superposition"); let new_clauses = new_clauses @ additional_new_clauses in debug (lazy (Printf.sprintf "Demodulating %d clauses" (List.length new_clauses))); let bag, new_clauses = HExtlib.filter_map_monad (simplify atable maxvar) bag new_clauses in - debug "Demodulated new clauses"; + debug (lazy "Demodulated new clauses"); bag, maxvar, (alist, atable), new_clauses ;; @@ -718,7 +719,7 @@ module Superposition (B : Orderings.Blob) = let bag, maxvar, new_goals = superposition_with_table bag maxvar goal atable in - debug "Superposed goal with active clauses"; + debug (lazy "Superposed goal with active clauses"); (* We simplify the new goals with active clauses *) let bag, new_goals = List.fold_left @@ -728,7 +729,7 @@ module Superposition (B : Orderings.Blob) = | Some (bag,g) -> bag,g::acc) (bag, []) new_goals in - debug "Simplified new goals with active clauses"; + debug (lazy "Simplified new goals with active clauses"); bag, maxvar, List.rev new_goals ;;