Smt (kind2dev@731decdf5fb1.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 = [

| `Bitwuzla_SMTLIB
| `cvc5_SMTLIB
| `MathSAT_SMTLIB
| `OpenSMT_SMTLIB
| `SMTInterpol_SMTLIB
| `Yices2_SMTLIB
| `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.

type qe_solver = [

| `cvc5_SMTLIB
| `Z3_SMTLIB
| `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 = [

| `cvc5_QE
| `Bitwuzla_SMTLIB
| `MathSAT_SMTLIB
| `OpenSMT_SMTLIB
| `SMTInterpol_SMTLIB
| `Z3_QE
| `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 prefer_solvers : 
  ?solver:solver ->
  ?itp:itp_solver ->
  ?qe:qe_solver ->
  unit ->
  unit

prefer_solvers ?solver ?itp ?qe () uses the given main, interpolating and quantifier-elimination solvers for the roles that were left to detection (no --smt_solver, --smt_itp_solver, --smt_qe_solver), provided their executables are found. A role whose preferred solver is not found is left to detection. To be called before the solvers are checked (see check_solvers).

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 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