From 49094e65a1b9d794d2bef9d2b69173c7af07ab36 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 9 Dec 2009 15:56:01 +0000 Subject: [PATCH] Clean up of debgging info --- .../ng_paramodulation/nCicParamod.ml | 13 +++--- .../components/ng_paramodulation/paramod.ml | 44 +++++++++++++------ 2 files changed, 39 insertions(+), 18 deletions(-) diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml index a96d3cc0a..78a57faa2 100644 --- a/helm/software/components/ng_paramodulation/nCicParamod.ml +++ b/helm/software/components/ng_paramodulation/nCicParamod.ml @@ -16,6 +16,9 @@ NCicBlob.set_default_eqP() NCicProof.set_default_sig() ;; +let debug _ = ();; +(* let debug s = prerr_endline (Lazy.force s);; *) + module B(C : NCicBlob.NCicContext): Orderings.Blob with type t = NCic.term and type input = NCic.term = Orderings.LPO(NCicBlob.NCicBlob(C)) @@ -30,8 +33,8 @@ let readback rdb metasenv subst context (bag,i,l) = *) let stamp = Unix.gettimeofday () in let proofterm = NCicProof.mk_proof bag i l in - prerr_endline (Printf.sprintf "Got proof term in %fs" - (Unix.gettimeofday() -. stamp)); + debug (lazy (Printf.sprintf "Got proof term in %fs" + (Unix.gettimeofday() -. stamp))); let metasenv, proofterm = let rec aux k metasenv = function | NCic.Meta _ as t -> metasenv, t @@ -45,13 +48,13 @@ let readback rdb metasenv subst context (bag,i,l) = in aux 0 metasenv proofterm in - prerr_endline "so far 1"; - prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context proofterm); + debug (lazy (NCicPp.ppterm ~metasenv ~subst ~context proofterm)); let metasenv, subst, proofterm, _prooftype = NCicRefiner.typeof (rdb#set_coerc_db NCicCoercion.empty_db) metasenv subst context proofterm None in + debug (lazy "refined!"); proofterm, metasenv, subst let nparamod rdb metasenv subst context t table = @@ -98,7 +101,7 @@ let forward_infer_step s t ty = let bag,clause = P.mk_passive bag (t,ty) in if Terms.is_eq_clause clause then P.forward_infer_step (P.replace_bag s bag) clause 0 - else (prerr_endline "not and equality"; s) + else s ;; let index_obj s uri = diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 3af1a38e4..b15503de4 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -204,7 +204,12 @@ module Paramod (B : Orderings.Blob) = struct let initialize_goal (bag,maxvar,actives,passives,_,_) t = let (bag,maxvar), g = mk_goal (bag,maxvar) t in let g_passives = g_passive_empty_set in - let g_passives = add_passive_goal g_passives g in + (* if the goal is not an equation we returns an empty + passive set *) + let g_passives = + if Terms.is_eq_clause g then add_passive_goal g_passives g + else g_passives + in (bag,maxvar,actives,passives,[],g_passives) @@ -318,7 +323,18 @@ module Paramod (B : Orderings.Blob) = struct debug (lazy("Last chance " ^ string_of_float (Unix.gettimeofday()))); let active_t = snd actives in - let passive_t,_,_ = passives in + let passive_t,wset,_ = passives in + let _ = debug + (lazy + ("Passive set :" ^ (String.concat ";\n" + (List.map (fun _,cl -> Pp.pp_unit_clause cl) + (WeightPassiveSet.elements wset))))) in + let wset = IDX.elems passive_t in + let _ = debug + (lazy + ("Passive table :" ^(String.concat ";\n" + (List.map (fun _,cl -> Pp.pp_unit_clause cl) + (IDX.ClauseSet.elements wset))))) in let g_passives = WeightPassiveSet.fold (fun (_,x) acc -> @@ -462,14 +478,13 @@ module Paramod (B : Orderings.Blob) = struct let gsteps,esteps = traverse true ([],[]) i in (List.rev esteps)@gsteps in - prerr_endline ("steps: " ^ (string_of_int (List.length l))); + debug (lazy ("steps: " ^ (string_of_int (List.length l)))); let max_w = List.fold_left (fun acc i -> let (cl,_,_) = Terms.get_from_bag i bag in max acc (Order.compute_unit_clause_weight cl)) 0 l in - prerr_endline "Statistics :"; - prerr_endline ("Max weight : " ^ (string_of_int max_w)); + debug (lazy ("Max weight : " ^ (string_of_int max_w))); (* List.iter (fun id -> let ((_,lit,_,proof as cl),d,it) = Terms.get_from_bag id bag in if d then @@ -482,11 +497,12 @@ module Paramod (B : Orderings.Blob) = struct (Printf.sprintf "Id : %d, selected at %d, weight %d by %s" id it (Order.compute_unit_clause_weight cl) (Pp.pp_proof_step proof))) l;*) - prerr_endline "Proof:"; - List.iter - (fun x -> - let cl,_,_ = Terms.get_from_bag x bag in - prerr_endline (Pp.pp_unit_clause cl)) l; + debug (lazy ("Proof:" ^ + (String.concat "\n" + (List.map + (fun x -> + let cl,_,_ = Terms.get_from_bag x bag in + Pp.pp_unit_clause cl) l)))); Unsatisfiable [ bag, i, l ] let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives = @@ -505,18 +521,20 @@ module Paramod (B : Orderings.Blob) = struct with | Sup.Success (bag, _, (i,_,_,_)) -> compute_result bag i - | Stop (Unsatisfiable _) -> Error "stop bug solution found!" + | Stop (Unsatisfiable _) -> Error "solution found!" | Stop o -> o ;; let fast_eq_check s goal = - let s = initialize_goal s goal in + let (_,_,_,_,_,g_passives) as s = initialize_goal s goal in + if is_passive_g_set_empty g_passives then Error "not an equation" + else try goal_narrowing 0 2 None s with | Sup.Success (bag, _, (i,_,_,_)) -> compute_result bag i - | Stop (Unsatisfiable _) -> Error "stop bug solution found!" + | Stop (Unsatisfiable _) -> Error "solution found!" | Stop o -> o ;; -- 2.39.2