Module Formula.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.

type 'a command =
  1. | PutEntry : Formula.entry -> unit command
  2. | CheckSat : float -> Formula.status command
  3. | GetModel : Binsec_smtlib__.Formula_model.t command
  4. | GetBvValue : Formula.bv_term list -> Binsec_base.Bitvector.t list command
  5. | GetAxValue : Formula.ax_term -> (Binsec_base.Bitvector.t * Binsec_base.Bitvector.t) array command
module Command : sig ... end
module Make (S : sig ... end) : sig ... end