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§
- z3
- This module contains glue code that implements
liblisa::smt::SmtSolver. To use this module, the featurez3needs to be enabled.
Structs§
- Assertion
Hash - A hash for a set of assertions executed on a solver. Used as the key for the solver cache.
- CacheBV
- Cacheable SMT BV type.
- CacheBV
Array - Cacheable SMT Array type.
- Cache
Bool - Cacheable SMT Bool type.
- Cache
HitCounter - A wrapper around a
SolverCachethat counts the number of cache hits and misses. - Cache
Int - Cacheable SMT Int type.
- Cache
Model - Cacheable SMT model that is returned when the assertions are satisfiable.
- Cache
Model Ref - A reference to a
CacheModel. - Cached
Solver - A solver that uses caching.
- Cached
Solver Provider - A solver provider that returns
CachedSolvers. - File
Cache - A
SolverCachethat persists its cache to disk. - Memory
Cache - A solver cache backed by a
HashMap. - Shared
Cache - A solver cache wrapped in a
Mutex.
Enums§
- Cache
Result - A cached SAT solver result
- Dynamic
- An expression that is dynamically typed.
- SatResult
- The result of running a SAT solver on a set of assertions.
- Sort
- The sort of an expression.
- Sort
Kind - The sort kind of an expression.
Traits§
- SmtBV
- BitVector expressions in the SMT solver.
- SmtBV
Array - Array expressions in the SMT solver.
- SmtBool
- Boolean expressions in the SMT solver.
- SmtInt
- Integer expressions in the SMT solver.
- SmtModel
- Model for satisfied assertions.
- SmtModel
Ref - Reference to
SmtModel. - SmtSolver
- An SMT solver.
- Solver
Cache - Methods that allow the type to be used as a cache for SMT solver assertions.
- Solver
Provider - Provides
SmtSolvers without having to know all of the configuration details of the individual solvers.