Module Call_provers

module Call_provers: sig .. end

Call provers and parse their outputs

data types for prover answers

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`	`(*`	The prover can't determine if the task is valid	`*)`
`\|`	`Failure of string`	`(*`	The prover reports a failure	`*)`
`\|`	`HighFailure of string`	`(*`	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_models : (prover_answer * Model_parser.model) list;`	`(*`	The models produced by a the solver	`*)`

}

val print_prover_answer : Stdlib.Format.formatter -> prover_answer -> unit

Pretty-print a Call_provers.prover_answer

val print_prover_result : ?json:bool -> Stdlib.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 json_prover_result : prover_result -> Json_base.json

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_limits = {

	`limit_time : float;`
	`limit_mem : int;`
	`limit_steps : int;`

}

val empty_limits : resource_limits

val limit_max : resource_limits ->
       resource_limits -> resource_limits

val call_editor : config:Whyconf.main -> command:string -> string -> prover_call

val call_on_buffer : command:string ->
       config:Whyconf.main ->
       limits:resource_limits ->
       res_parser:prover_result_parser ->
       filename:string ->
       get_model:Printer.printing_info option ->
       gen_new_file:bool ->
       ?inplace:bool -> Stdlib.Buffer.t -> prover_call

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

config : the main configuration data for Why3 (see Whyconf).

res_parser : prover result parser

filename : the suffix of the proof task's file, if the prover doesn't accept stdin.

gen_new_file : When set, this generates a new temp file to run the prover on. Otherwise it reuses the filename already given.

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 interrupt_call : config:Whyconf.main -> prover_call -> unit

non-blocking function that asks for prover interruption

val wait_on_call : prover_call -> prover_result

blocking function that waits until the prover finishes.

val debug_attrs : Debug.flag

Print attributes in model