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