Module smtlib_lowlevel::backend
source · Expand description
Backends are concrete solvers which can be communicated with using the SMT-LIB language.
This module contains the solver which are supported out-of-the-box by
smtlib
. Each backend is feature gated, which means that a feature must be
enabled to use the backend.
Backends
Z3Binary
: A Z3 backend using the binary CLI interface.- Enabled by feature:
z3
- Enabled by feature:
- [
Z3Static
]: A Z3 backend using thez3-sys
crate.- Enabled by feature:
z3-static
- Enabled by feature:
Cvc5Binary
: A cvc5 backend using the binary CLI interface.- Enabled by feature:
cvc5
- Enabled by feature:
Structs
Traits
- The
AsyncBackend
trait is used to interact with SMT solver using the SMT-LIB language. - The
Backend
trait is used to interact with SMT solver using the SMT-LIB language.