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

Inheritance diagram for 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

void	toJSON (JSONGenerator &) const override

Detailed Description

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

Member Function Documentation

std::optional< bool > P4Tools::Z3Solver::checkSat ( )

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

std::optional< bool > 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 P4Tools::Z3Solver::clearMemory ( )

Reset the internal Z3 solver state (memory and active assertions). In incremental state, all active assertions are reapplied after resetting.

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

void P4Tools::Z3Solver::reset ( )

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