Module z3
Expand description
This module contains glue code that implements liblisa::smt::SmtSolver.
To use this module, the feature z3 needs to be enabled.
Structsยง
- BV
- A Z3 bitvector.
- Bool
- A Z3 Bool.
- BvArray
- A Z3 Array.
- Int
- A Z3 Int.
- Model
- The Z3 model returned when assertions are satisfiable.
- Model
Ref - A reference to the Z3 model returned when assertions are satisfiable.
- Thread
Local Z3 - A
SolverProviderthat uses a thread-local Z3 instance. - Z3Solver
- The Z3
SmtSolver.