Module `Flags.Smt`

SMT solver flags

type logic = [ | `None | `detect | `Logic of string ]: Logic sendable to the SMT solver.

val logic : unit -> logic: Logic to send to the SMT solver

type solver = [ | `Z3_SMTLIB | `CVC4_SMTLIB | `Yices_SMTLIB | `Yices_native | `detect ]: Legal SMT solvers.

val set_solver : solver -> unit: Set SMT solver and executable

val solver : unit -> solver: Which SMT solver to use.

val check_sat_assume : unit -> bool: Use check-sat with assumptions, or simulate with push/pop

val set_check_sat_assume : bool -> unit
val short_names : unit -> bool: Send short names to SMT solver

val set_short_names : bool -> unit: Change sending of short names to SMT solver

val z3_bin : unit -> string: Executable of Z3 solver

val cvc4_bin : unit -> string: Executable of CVC4 solver

val yices_bin : unit -> string: Executable of Yices solver

val yices2smt2_bin : unit -> string: Executable of Yices2 SMT2 solver

val yices2_smt2models : unit -> bool: Yices 2 binary supports models in SMT2 format *

val set_yices2_smt2models : bool -> unit

val set_trace : bool -> unit

Forces SMT traces.

Write all SMT commands to files

val trace : unit -> bool: Write all SMT commands to files

val trace_dir : unit -> string: Path to the smt trace directory.