Module Driver

module Driver: sig .. end

Managing the drivers for external provers

Create a driver

type driver

val load_driver_absolute : Env.env -> string -> string list -> driver

loads a driver from a file

Use a driver

val file_of_task : driver -> string -> string -> Task.task -> string

file_of_task d f th t produces a filename for the prover of driver d, for a task t generated from a goal in theory named th of filename f

val file_of_theory : driver -> string -> Theory.theory -> string

file_of_theory d f th produces a filename for the prover of driver d, for a theory th from filename f

val call_on_buffer : command:string ->
       limit:Call_provers.resource_limit ->
       ?inplace:bool ->
       filename:string ->
       printer_mapping:Printer.printer_mapping ->
       driver -> Buffer.t -> Call_provers.prover_call

val print_task : ?old:Pervasives.in_channel ->
       ?cntexample:bool -> driver -> Format.formatter -> Task.task -> unit

val print_theory : ?old:Pervasives.in_channel ->
       driver -> Format.formatter -> Theory.theory -> unit

produce a realization of the given theory using the given driver

val prove_task : command:string ->
       limit:Call_provers.resource_limit ->
       ?cntexample:bool ->
       ?old:string ->
       ?inplace:bool -> driver -> Task.task -> Call_provers.prover_call

val prepare_task : cntexample:bool -> driver -> Task.task -> Task.task

Split the previous function in two simpler functions

val print_task_prepared : ?old:Pervasives.in_channel ->
       driver -> Format.formatter -> Task.task -> Printer.printer_mapping

val prove_task_prepared : command:string ->
       limit:Call_provers.resource_limit ->
       ?old:string ->
       ?inplace:bool -> driver -> Task.task -> Call_provers.prover_call

Traverse all metas from a driver

val syntax_map : driver -> Printer.syntax_map