Module smt
Expand description
A generic interface for SMT solvers.
We do not want libLISA to depend on a specific SMT solver. This pulls in unwanted C dependencies that make the library less portable.
The generic SmtSolver trait abstracts over the SMT solver implementation.
This allows us to specify operations that use an SMT solver,
but leave the actual implementation up to a separate crate (liblisa-z3) that can be imported when necessary.
Modules§
- This module contains glue code that implements
liblisa::smt::SmtSolver. To use this module, the featurez3needs to be enabled.
Structs§
- A hash for a set of assertions executed on a solver. Used as the key for the solver cache.
- Cacheable SMT BV type.
- Cacheable SMT Array type.
- Cacheable SMT Bool type.
- A wrapper around a
SolverCachethat counts the number of cache hits and misses. - Cacheable SMT Int type.
- Cacheable SMT model that is returned when the assertions are satisfiable.
- A reference to a
CacheModel. - A solver that uses caching.
- A solver provider that returns
CachedSolvers. - A
SolverCachethat persists its cache to disk. - A solver cache backed by a
HashMap. - A solver cache wrapped in a
Mutex.
Enums§
- A cached SAT solver result
- An expression that is dynamically typed.
- The result of running a SAT solver on a set of assertions.
- The sort of an expression.
- The sort kind of an expression.
Traits§
- BitVector expressions in the SMT solver.
- Array expressions in the SMT solver.
- Boolean expressions in the SMT solver.
- Integer expressions in the SMT solver.
- Model for satisfied assertions.
- Reference to
SmtModel. - An SMT solver.
- Methods that allow the type to be used as a cache for SMT solver assertions.
- Provides
SmtSolvers without having to know all of the configuration details of the individual solvers.