Clean up of debgging info

[helm.git] / helm / software / components / ng_paramodulation / paramod.ml

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
   ;;