;;
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))
else
let _ =
(* print_status iterno goals active passive *)
- Printf.printf ".%!";
+ Printf.eprintf ".%!";
in
(* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *)
let passive =
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
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"; *)
(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
;;
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 =
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)) *)