![]() |
P4C
The P4 Compiler
|
A Z3-based implementation of AbstractSolver. Encapsulates a z3::solver and a z3::context. More...
#include <z3_solver.h>
Public Member Functions | |
Z3Solver (bool isIncremental=true, std::optional< std::istream * > inOpt=std::nullopt) | |
void | asrt (const Constraint *assertion) |
Inserts an assertion into the topmost solver context. | |
void | asrt (const z3::expr &assert) |
Adds a Z3 assertion to the solver context. | |
std::optional< bool > | checkSat () |
std::optional< bool > | checkSat (const std::vector< const Constraint * > &asserts) override |
std::optional< bool > | checkSat (const z3::expr_vector &asserts) |
void | clearMemory () |
void | comment (cstring comment) override |
safe_vector< const Constraint * > | getAssertions () const |
const SymbolicMapping & | getSymbolicMapping () const override |
const z3::context & | getZ3Ctx () const |
Get the actual Z3 context that this class uses. | |
const z3::solver & | getZ3Solver () const |
Get the actual Z3 solver backing this class. | |
bool | isInIncrementalMode () const override |
void | pop () |
Removes the last solver context. | |
void | push () |
Pushes new (empty) solver context. | |
void | reset () |
void | seed (unsigned seed) override |
void | timeout (unsigned tm) override |
Sets timeout for solver in milliseconds. | |
void | toJSON (JSONGenerator &) const override |
Saves solver state to the given JSON generator. | |
![]() | |
DECLARE_TYPEINFO (AbstractSolver) | |
![]() | |
template<typename T> | |
T & | as () |
Tries to convert the class to type T. A BUG occurs if the cast fails. | |
template<typename T> | |
const T & | as () const |
Tries to convert the class to type T. A BUG occurs if the cast fails. | |
template<typename T> | |
T * | checkedTo () |
Performs a checked cast. A BUG occurs if the cast fails. | |
template<typename T> | |
const T * | checkedTo () const |
Performs a checked cast. A BUG occurs if the cast fails. | |
![]() | |
template<typename T> | |
bool | is () const noexcept |
virtual bool | isA (TypeId typeId) const noexcept=0 |
template<typename T> | |
const T * | to () const noexcept |
Same as to , but returns const pointer to T. | |
template<typename T> | |
T * | to () noexcept |
virtual TypeId | typeId () const noexcept=0 |
Friends | |
class | Z3JSON |
class | Z3SolverAccessor |
class | Z3Translator |
Additional Inherited Members | |
![]() | |
virtual const void * | toImpl (TypeId typeId) const noexcept=0 |
A Z3-based implementation of AbstractSolver. Encapsulates a z3::solver and a z3::context.
std::optional< bool > P4::P4Tools::Z3Solver::checkSat | ( | ) |
Z3Solver specific checkSat function. Calls check on the solver. Only useful in incremental mode.
|
overridevirtual |
Determines whether the set of assertions given to the solver are consistent.
Implements P4::AbstractSolver.
std::optional< bool > P4::P4Tools::Z3Solver::checkSat | ( | const z3::expr_vector & | asserts | ) |
Z3Solver specific checkSat function. Calls check on the input z3::expr_vector. Only relies on the incrementality mode of the Z3 solver.
void P4::P4Tools::Z3Solver::clearMemory | ( | ) |
Reset the internal Z3 solver state (memory and active assertions). In incremental state, all active assertions are reapplied after resetting.
|
overridevirtual |
Adds a comment to any log file that might be produced. Useful for understanding the sequence of calls made to the solver when debugging.
Implements P4::AbstractSolver.
|
nodiscard |
|
nodiscardoverridevirtual |
Obtains the first solution found by the solver in the last call to @checkSat.
A BUG occurs if the solver has no available solution. This can happen if the last call to @checkSat returned anything other than true, if there was no such previous call, or if the state in the solver has changed since the last such call (e.g., more assertions have been made).
Implements P4::AbstractSolver.
|
nodiscardoverridevirtual |
Implements P4::AbstractSolver.
void P4::P4Tools::Z3Solver::reset | ( | ) |
Resets the internal state: pops all assertions from previous solver invocation, removes variable declarations.
|
overridevirtual |
Seeds the pseudo-random number generator in the solver. The solver's PRNG is used to randomize the models produced by @getModel.
Implements P4::AbstractSolver.
|
overridevirtual |
Sets timeout for solver in milliseconds.
Implements P4::AbstractSolver.
|
overridevirtual |
Saves solver state to the given JSON generator.
Implements P4::AbstractSolver.