Module Call_provers

module Call_provers: sig .. end

Call provers and parse their outputs

data types for prover answers

type reason_unknown = 
| Resourceout (*

Out of resources

*)
| Other (*

Other reason

*)

The reason why unknown was reported

type prover_answer = 
| Valid (*

The task is valid according to the prover

*)
| Invalid (*

The task is invalid

*)
| Timeout (*

the task timeouts, ie it takes more time than specified

*)
| OutOfMemory (*

the task runs out of memory

*)
| StepLimitExceeded (*

the task required more steps than the limit provided

*)
| Unknown of (string * reason_unknown option) (*

The prover can't determine if the task is valid

*)
| Failure of string (*

The prover reports a failure

*)
| HighFailure (*

An error occured during the call to the prover or none of the given regexps match the output of the prover

*)
type prover_result = {
   pr_answer : prover_answer; (*

The answer of the prover on the given task

*)
   pr_status : Unix.process_status; (*

The process exit status

*)
   pr_output : string; (*

The output of the prover currently stderr and stdout

*)
   pr_time : float; (*

The time taken by the prover

*)
   pr_steps : int; (*

The number of steps taken by the prover (-1 if not available)

*)
   pr_model : Model_parser.model; (*

The model produced by a the solver

*)
}
val print_prover_answer : Format.formatter -> prover_answer -> unit

Pretty-print a Call_provers.prover_answer

val print_prover_result : Format.formatter -> prover_result -> unit

Pretty-print a prover_result. The answer and the time are output. The output of the prover is printed if and only if the answer is a HighFailure

val debug : Debug.flag

debug flag for the calling procedure (option "--debug call_prover") If set call_on_buffer prints on stderr the commandline called and the output of the prover.

type timeregexp 

The type of precompiled regular expressions for time parsing

type stepregexp 

The type of precompiled regular expressions for parsing of steps

val timeregexp : string -> timeregexp

Converts a regular expression with special markers '%h','%m', '%s','%i' (for milliseconds) into a value of type timeregexp

val stepregexp : string -> int -> stepregexp

stepregexp s n creates a regular expression to match the number of steps. s is a regular expression, n is the group number with steps number.

type 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;
}

Functions for calling external provers

type prover_call 

Type that represents a single prover run

type resource_limit = {
   limit_time : int;
   limit_mem : int;
   limit_steps : int;
}
val empty_limit : resource_limit
val limit_max : resource_limit ->
resource_limit -> resource_limit
val call_editor : command:string -> string -> prover_call
val 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_call

Build a prover call on the task already printed in the Buffer.t given.

limit : : set the available time limit (def. 0 : unlimited), memory limit (def. 0 : unlimited) and step limit (def. -1 : unlimited)
res_parser : : prover result parser
filename : : the suffix of the proof task's file, if the prover doesn't accept stdin.
inplace : : it is used to make a save of the file on which the prover was called. It is renamed as %f.save if inplace=true and the command actualcommand fails
type prover_update = 
| NoUpdates
| ProverInterrupted
| InternalFailure of exn
| ProverStarted
| ProverFinished of prover_result
val get_new_results : blocking:bool -> (prover_call * prover_update) list

returns new results from why3server, in an unordered fashion.

val query_call : prover_call -> prover_update

non-blocking function that reports any new updates from the server related to a given prover call.

val wait_on_call : prover_call -> prover_result

blocking function that waits until the prover finishes.