Module Flags.Smt

SMT solver flags

type logic = [
  1. | `None
  2. | `detect
  3. | `Logic of string
]

Logic sendable to the SMT solver.

val logic : unit -> logic

Logic to send to the SMT solver

type solver = [
  1. | `Bitwuzla_SMTLIB
  2. | `cvc5_SMTLIB
  3. | `MathSAT_SMTLIB
  4. | `OpenSMT_SMTLIB
  5. | `SMTInterpol_SMTLIB
  6. | `Yices2_SMTLIB
  7. | `Yices_native
  8. | `Z3_SMTLIB
  9. | `detect
]

Legal SMT solvers.

val set_solver : solver -> unit

Set SMT solver and executable

val solver : unit -> solver

Which SMT solver to use.

type qe_solver = [
  1. | `cvc5_SMTLIB
  2. | `Z3_SMTLIB
  3. | `detect
]
val set_qe_solver : qe_solver -> unit

Set SMT solver for QE

val qe_solver : unit -> qe_solver

Which SMT solver for QE to use.

type itp_solver = [
  1. | `cvc5_QE
  2. | `Bitwuzla_SMTLIB
  3. | `MathSAT_SMTLIB
  4. | `OpenSMT_SMTLIB
  5. | `SMTInterpol_SMTLIB
  6. | `Z3_QE
  7. | `detect
]
val set_itp_solver : itp_solver -> unit

Set SMT solver for interpolation

val itp_solver : unit -> itp_solver

Which SMT solver for interpolation to use.

val get_itp_solver : unit -> solver
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 bitwuzla_bin : unit -> string

Executable of Bitwuzla solver

val cvc5_bin : unit -> string

Executable of cvc5 solver

val mathsat_bin : unit -> string

Executable of MathSAT solver

val opensmt_bin : unit -> string

Executable of OpenSMT solver

val smtinterpol_jar : unit -> string

JAR of SMTInterpol 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 yices_bin : unit -> string

Executable of Yices solver

val z3_bin : unit -> string

Executable of Z3 solver

val z3_qe_light : unit -> bool

Whether Z3 qe-light strategy is used in addition to qe

val set_z3_qe_light : bool -> unit

Specify if Z3 qe-light strategy should be used in addition to qe

val set_trace : bool -> unit

Forces SMT traces.

val trace : unit -> bool

Write all SMT commands to files

val trace_dir : unit -> string

Path to the smt trace directory.

val trace_subdir : unit -> string

Name of subdirectory within the smt trace directory.

val set_trace_subdir : string -> unit