package binsec

  1. Overview
  2. Docs
package binsec
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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 type S = sig ... end
module Make (S : sig ... end) : S with type arg = S.arg
module Make_binding (_ : Binsec_smtlib_bindings.OPEN) : S with type arg = unit
val create : Binsec_smtlib__.Backend.t -> (module S with type arg = unit)