X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=83588d24d5a7987da65242326adeda5a9bf07567;hb=dd1c4eeef3d38eb9e01d50d06de6892a048c05a5;hp=021afb5abdf0ed36f61450e6119d7fdc2230173c;hpb=894b08ca7d14aa7e31c35f3acb3903a1c3472a27;p=helm.git

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index 021afb5ab..83588d24d 100644
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -976,7 +976,7 @@ let pp_goals label goals context =
 ;;
 
 let print_status iterno goals active passive =
-  print_endline 
+  prerr_endline 
     (Printf.sprintf "\n%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)"
       iterno (size_of_active active) (size_of_passive passive)
       (size_of_goal_set_a goals) (size_of_goal_set_p goals)) 
@@ -1006,7 +1006,7 @@ let given_clause
     else
       let _ = 
 (*         print_status iterno goals active passive  *)
-        Printf.printf ".%!";
+        Printf.eprintf ".%!";
       in
       (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *) 
       let passive =
@@ -1025,7 +1025,7 @@ let given_clause
       in
       match check_if_goals_set_is_solved env active goals with
       | Some p -> 
-          print_endline 
+          prerr_endline 
             (Printf.sprintf "\nFound a proof in: %f\n" 
               (Unix.gettimeofday() -. initial_time));
           ParamodulationSuccess p
@@ -1211,7 +1211,8 @@ let eq_and_ty_of_goal = function
 
 let saturate 
     caso_strano 
-    dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = 
+    dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) 
+    ?(timeout=600.) status = 
   let module C = Cic in
   reset_refs ();
   Indexing.init_index ();
@@ -1282,7 +1283,7 @@ let saturate
 *)
       let goals = make_goal_set goal in
       let max_iterations = 10000 in
-      let max_time = Unix.gettimeofday () +.  600. (* minutes *) in
+      let max_time = Unix.gettimeofday () +.  timeout (* minutes *) in
       given_clause 
         eq_uri env goals theorems passive active max_iterations max_time 
     in
@@ -1294,8 +1295,8 @@ let saturate
       raise (ProofEngineTypes.Fail (lazy ("NO proof found: " ^ s)))
   | ParamodulationSuccess 
     (goalproof,newproof,subsumption_id,subsumption_subst, proof_menv) ->
-      print_endline "Proof:";
-      print_endline 
+      prerr_endline "Proof:";
+      prerr_endline 
         (Equality.pp_proof names goalproof newproof subsumption_subst
           subsumption_id type_of_goal);
 (*       prerr_endline "ENDOFPROOFS"; *)
@@ -1413,7 +1414,7 @@ let saturate
           (CicMetaSubst.ppmetasenv [] metasenv)
           (CicMetaSubst.ppmetasenv [] real_metasenv);
 *)
-      print_endline (Printf.sprintf "\nTIME NEEDED: %8.2f" time);
+      prerr_endline (Printf.sprintf "\nTIME NEEDED: %8.2f" time);
       proof, open_goals
 ;;
 
@@ -1537,14 +1538,14 @@ let main_demod_equalities dbd term metasenv ugraph =
     in
     let active = make_active () in
     let passive = make_passive equalities in
-    Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
-    Printf.printf "\nmetasenv:\n%s\n" (Utils.print_metasenv metasenv);
-    Printf.printf "\nequalities:\n%s\n"
+    Printf.eprintf "\ncontext:\n%s\n" (PP.ppcontext context);
+    Printf.eprintf "\nmetasenv:\n%s\n" (Utils.print_metasenv metasenv);
+    Printf.eprintf "\nequalities:\n%s\n"
       (String.concat "\n"
          (List.map
             (Equality.string_of_equality ~env) equalities));
-    print_endline "--------------------------------------------------";
-    print_endline "GO!";
+    prerr_endline "--------------------------------------------------";
+    prerr_endline "GO!";
     start_time := Unix.gettimeofday ();
     if !time_limit < 1. then time_limit := 60.;    
     let ra, rp =
@@ -1568,7 +1569,7 @@ let main_demod_equalities dbd term metasenv ugraph =
       let l = fst ra in
       EqualitySet.elements (List.fold_left addfun EqualitySet.empty l)
     in
-    Printf.printf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n"
+    Printf.eprintf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n"
        (String.concat "\n" (List.map (Equality.string_of_equality ~env) active)) 
      (*  (String.concat "\n"
          (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active)) *)