package why3

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

type prover_answer =

| Valid
| Invalid
| Timeout
| OutOfMemory
| StepLimitExceeded
| Unknown of string
| Failure of string
| HighFailure

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 -> unit

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

val debug : Debug.flag

type timeregexp

type stepregexp

val timeregexp : string -> timeregexp

val stepregexp : string -> int -> stepregexp

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;

}

type prover_call

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

type prover_update =

| NoUpdates
| ProverInterrupted
| InternalFailure of exn
| ProverStarted
| ProverFinished of prover_result

val get_new_results : blocking:bool -> (prover_call * prover_update) list

val query_call : prover_call -> prover_update

val interrupt_call : prover_call -> unit

val wait_on_call : prover_call -> prover_result