print_endline => prerr_endline

[helm.git] / helm / software / components / tactics / paramodulation / saturation.ml

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 021afb5abdf0ed36f61450e6119d7fdc2230173c..90cc852474da915ce94c7645783a39a7d1d8a5a2 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/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)) 
@@ -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
 ;;
 
@@ -1543,8 +1544,8 @@ let main_demod_equalities dbd term metasenv ugraph =
       (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 =