P4::P4Tools::Z3Solver Class Reference

A Z3-based implementation of AbstractSolver. Encapsulates a z3::solver and a z3::context. More...

#include <z3_solver.h>

Inheritance diagram for P4::P4Tools::Z3Solver:

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.
Public Member Functions inherited from P4::AbstractSolver
	DECLARE_TYPEINFO (AbstractSolver)
Public Member Functions inherited from P4::ICastable
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.
Public Member Functions inherited from P4::RTTI::Base
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
Protected Member Functions inherited from P4::RTTI::Base
virtual const void *	toImpl (TypeId typeId) const noexcept=0

Detailed Description

A Z3-based implementation of AbstractSolver. Encapsulates a z3::solver and a z3::context.

Member Function Documentation

checkSat() [1/3]

std::optional< bool > P4::P4Tools::Z3Solver::checkSat

(

)

Z3Solver specific checkSat function. Calls check on the solver. Only useful in incremental mode.

checkSat() [2/3]

std::optional< bool > P4::P4Tools::Z3Solver::checkSat ( const std::vector< const Constraint * > & asserts )

overridevirtual

Determines whether the set of assertions given to the solver are consistent.

Returns

true if the given assertions are consistent.

false if the given assertions are inconsistent.

std::nullopt if the solver times out, or is otherwise unable to provide an answer.

Implements P4::AbstractSolver.

checkSat() [3/3]

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.

clearMemory()

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.

comment()

void P4::P4Tools::Z3Solver::comment ( cstring comment )

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.

getAssertions()

safe_vector< const Constraint * > P4::P4Tools::Z3Solver::getAssertions ( ) const

nodiscard

Returns

the list of active assertions on this solver.

getSymbolicMapping()

const SymbolicMapping & P4::P4Tools::Z3Solver::getSymbolicMapping ( ) const

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.

isInIncrementalMode()

bool P4::P4Tools::Z3Solver::isInIncrementalMode ( ) const

nodiscardoverridevirtual

Returns

whether this solver is incremental.

Implements P4::AbstractSolver.

reset()

void P4::P4Tools::Z3Solver::reset

(

)

Resets the internal state: pops all assertions from previous solver invocation, removes variable declarations.

seed()

void P4::P4Tools::Z3Solver::seed ( unsigned seed )

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.

timeout()

void P4::P4Tools::Z3Solver::timeout ( unsigned tm )

overridevirtual

Sets timeout for solver in milliseconds.

Implements P4::AbstractSolver.

toJSON()

void P4::P4Tools::Z3Solver::toJSON ( JSONGenerator & ) const

overridevirtual

Saves solver state to the given JSON generator.

Implements P4::AbstractSolver.