Module 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.
• Z3BinaryTokio: An async Z3 backend using the binary CLI interface with tokio.
  • Enabled by feature: tokio
• Z3Static: A Z3 backend using the z3-sys crate.
  • Enabled by feature: z3-static
• Cvc5Binary: A cvc5 backend using the binary CLI interface.
• Cvc5BinaryTokio: An async cvc5 backend using the binary CLI interface with tokio.
  • Enabled by feature: tokio

Modules

cvc5_binary

z3_binary

Traits

Backend

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