type prover_result = {pr_answer : prover_answer;pr_status : Unix.process_status;pr_output : string;pr_time : float;pr_steps : int;pr_model : Model_parser.model;}val print_prover_answer : Format.formatter -> prover_answer -> unitval print_prover_result : Format.formatter -> prover_result -> unitval debug : Debug.flagval timeregexp : string -> timeregexpval stepregexp : string -> int -> stepregexptype prover_result_parser = {prp_regexps : (string * prover_answer) list;prp_timeregexps : timeregexp list;prp_stepregexps : stepregexp list;prp_exitcodes : (int * prover_answer) list;prp_model_parser : Model_parser.model_parser;}val empty_limit : resource_limitval limit_max : resource_limit -> resource_limit -> resource_limitval call_editor : command:string -> string -> prover_callval call_on_buffer :
command:string ->
limit:resource_limit ->
res_parser:prover_result_parser ->
filename:string ->
printer_mapping:Printer.printer_mapping ->
gen_new_file:bool ->
?inplace:bool ->
Buffer.t ->
prover_calltype prover_update = | NoUpdates| ProverInterrupted| InternalFailure of exn| ProverStarted| ProverFinished of prover_resultval get_new_results : blocking:bool -> (prover_call * prover_update) listval query_call : prover_call -> prover_updateval interrupt_call : prover_call -> unitval wait_on_call : prover_call -> prover_result