Interface with SMT solvers
This module provides basic functions to solve SMT formulas, either by providing the file name or directly by interacting with the SMT solver via theirs incremental mode.
module Command : sig ... endtype solver_session = private {id : int;solver : Prover.t;pid : Subprocess.t;stdin : Stdlib.out_channel;stdout : Stdlib.in_channel;stderr : Stdlib.in_channel;dump : Stdlib.out_channel option;combined : Stdlib.Format.formatter;incremental : bool;}channels when interacting with solvers
val start_interactive :
?file:string ->
?timeout:int ->
Prover.t ->
solver_sessionstart_interactive ~file ~timeout solver starts an interactive session with the solver solver and the given ~timeout (default is none). ~file provides a debug output file where every command sent to the solver are also copied.
val stop_interactive : solver_session -> unitstop the interactive session by closing the process
val solve : ?timeout:int -> string -> Prover.t -> Formula.statussolve ~timeout file solver solve the formula in file with the given ~timeout and the given solver. Only, the SMT status is returned
val solve_incremental :
?term:Formula.bl_term ->
solver_session ->
Formula.statussolve_incremental ~expr ~debug session solver solve the current formula fed to the solver. An optional smt_expr ~expr can be provided which would be added first.
val solve_model :
?timeout:int ->
string ->
Prover.t ->
Formula.status * Smt_model.tsame as solve but also returns the model generated
val solve_model_time :
?timeout:int ->
?get_model:bool ->
file:string ->
Prover.t ->
Formula.status * Smt_model.t * floatsame as solve_model but also returns the computation time
val solve_incremental_model :
?term:Formula.bl_term ->
solver_session ->
Formula.status * Smt_model.tsame as solve_incremental_model but also returns the model generated
val solve_incremental_model_time :
?term:Formula.bl_term ->
?get_model:bool ->
solver_session ->
Formula.status * Smt_model.t * floatsame as solve_incremental_model but also returns the computation time
val solve_incremental_value :
?term:Formula.bl_term ->
Formula.bv_term ->
solver_session ->
Formula.status * Smtlib.term optionsame as solve_incremental_model but uses the smtlib2 get-value rather than get-model
val push : solver_session -> unitsend the push command to the solver
val pop : solver_session -> unitsend the pop command to the solver
returns a formatter st everything printed to the formatter will be sent to * the solver *
val get_formatter_of_session : solver_session -> Stdlib.Format.formattermodule Session : sig ... end