Module Flags.Smt

module Smt: sig .. end

SMT solver flags



type logic = [ `Logic of string | `None | `detect ] 
Logic sendable to the SMT solver.
val logic : unit -> logic
Logic to send to the SMT solver
type solver = [ `CVC4_SMTLIB | `Yices_SMTLIB | `Yices_native | `Z3_SMTLIB | `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 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 set_trace : bool -> unit
Forces SMT traces.

Write all SMT commands to files

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