module Smt:`sig`

..`end`

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.