Clean up of debgging info

diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml
index a96d3cc0a098ab8046c72ada33eaba6cc9d5e44c..78a57faa22da8c23d28a1815307dbf3670e588aa 100644 (file)
--- 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 3af1a38e448c459369a0bead452a7b4c84cc6363..b15503de4f1ba9497efd292f24bac9a97a15171c 100644 (file)
--- 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
   ;;