Module smtlib_lowlevel::backend

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
• [Z3Static]: A Z3 backend using the z3-sys crate.
  • Enabled by feature: z3-static
• Cvc5Binary: A cvc5 backend using the binary CLI interface.
  • Enabled by feature: cvc5

Structs

• Cvc5Binary
• Z3Binary

Traits

• AsyncBackend
  The AsyncBackend trait is used to interact with SMT solver using the SMT-LIB language.
• Backend
  The Backend trait is used to interact with SMT solver using the SMT-LIB language.