- match res with
- | Failure ->
- Printf.printf "NO proof found! :-(\n\n"
- | Success (Some proof, env) ->
- Printf.printf "OK, found a proof!:\n%s\n%.9f\n"
- (PP.pp proof (names_of_context context))
- (finish -. start);
- Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
- "backward_simpl_time: %.9f\n")
- !infer_time !forward_simpl_time !backward_simpl_time;
-(* Printf.printf ("forward_simpl_details:\n build_all: %.9f\n" ^^ *)
-(* " demodulate: %.9f\n subsumption: %.9f\n") *)
-(* fs_time_info.build_all fs_time_info.demodulate *)
-(* fs_time_info.subsumption; *)
- | Success (None, env) ->
- Printf.printf "Success, but no proof?!?\n\n"
+ let _ =
+ match res with
+ | Failure ->
+ Printf.printf "NO proof found! :-(\n\n"
+ | Success (Some goal, env) ->
+ Printf.printf "OK, found a proof!\n";
+ let proof = Inference.build_term_proof goal in
+ print_endline (PP.pp proof (names_of_context context));
+ print_endline (string_of_float (finish -. start));
+ | Success (None, env) ->
+ Printf.printf "Success, but no proof?!?\n\n"
+ in
+ Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
+ "forward_simpl_new_time: %.9f\n" ^^
+ "backward_simpl_time: %.9f\n")
+ !infer_time !forward_simpl_time !forward_simpl_new_time
+ !backward_simpl_time;
+ Printf.printf "passive_maintainance_time: %.9f\n"
+ !passive_maintainance_time;
+ Printf.printf " successful unification/matching time: %.9f\n"
+ !Indexing.match_unif_time_ok;
+ Printf.printf " failed unification/matching time: %.9f\n"
+ !Indexing.match_unif_time_no;
+ Printf.printf " indexing retrieval time: %.9f\n"
+ !Indexing.indexing_retrieval_time;
+ Printf.printf " demodulate_term.build_newtarget_time: %.9f\n"
+ !Indexing.build_newtarget_time;
+ Printf.printf "derived %d clauses, kept %d clauses.\n"
+ !derived_clauses !kept_clauses;