Module Binsec.Solver

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 ... end
type solver_session = private {
  1. id : int;
  2. solver : Prover.t;
  3. pid : Subprocess.t;
  4. stdin : out_channel;
  5. stdout : in_channel;
  6. stderr : in_channel;
  7. dump : out_channel option;
  8. combined : Format.formatter;
  9. incremental : bool;
}

channels when interacting with solvers

val start_interactive : ?file:string -> ?timeout:int -> Prover.t -> solver_session

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

stop the interactive session by closing the process

val solve : ?timeout:int -> string -> Prover.t -> Formula.status

solve ~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.status

solve_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.t

same 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 * float

same as solve_model but also returns the computation time

val solve_incremental_model : ?term:Formula.bl_term -> solver_session -> Formula.status * Smt_model.t

same 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 * float

same 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 option

same as solve_incremental_model but uses the smtlib2 get-value rather than get-model

val push : solver_session -> unit

send the push command to the solver

val pop : solver_session -> unit

send 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 -> Format.formatter
module Session : sig ... end