#include <Z3SmtSolver.h>

Inheritance diagram for storm::solver::Z3SmtSolver:

Collaboration diagram for storm::solver::Z3SmtSolver:

Classes
class	Z3ModelReference

Public Member Functions
	Z3SmtSolver (storm::expressions::ExpressionManager &manager)

virtual	~Z3SmtSolver ()

virtual void	push () override
	Pushes a backtracking point on the solver's stack.

virtual void	pop () override
	Pops a backtracking point from the solver's stack.

virtual void	pop (uint_fast64_t n) override
	Pops multiple backtracking points from the solver's stack in the same way as pop() does.

virtual void	reset () override
	Removes all assertions from the solver's stack.

virtual void	add (storm::expressions::Expression const &assertion) override
	Adds an assertion to the solver's stack.

virtual CheckResult	check () override
	Checks whether the conjunction of assertions that are currently on the solver's stack is satisfiable.

virtual CheckResult	checkWithAssumptions (std::set< storm::expressions::Expression > const &assumptions) override
	Checks whether the conjunction of assertions that are currently on the solver's stack together with the provided assumptions is satisfiable.

virtual CheckResult	checkWithAssumptions (std::initializer_list< storm::expressions::Expression > const &assumptions) override
	Checks whether the conjunction of assertions that are currently on the solver's stack together with the provided assumptions is satisfiable.

virtual storm::expressions::SimpleValuation	getModelAsValuation () override
	If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model that satisfies all assertions on the solver's stack (as well as provided assumptions), provided that the solver was instantiated with support for model generation.

virtual std::shared_ptr< SmtSolver::ModelReference >	getModel () override
	If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model that satisfies all assertions on the solver's stack (as well as provided assumptions), provided that the solver was instantiated with support for model generation.

virtual std::vector< storm::expressions::SimpleValuation >	allSat (std::vector< storm::expressions::Variable > const &important) override
	Performs AllSat over the (provided) important atoms.

virtual uint_fast64_t	allSat (std::vector< storm::expressions::Variable > const &important, std::function< bool(storm::expressions::SimpleValuation &)> const &callback) override
	Performs AllSat over the (provided) important atoms.

virtual uint_fast64_t	allSat (std::vector< storm::expressions::Variable > const &important, std::function< bool(ModelReference &)> const &callback) override
	Performs AllSat over the (provided) important atoms.

virtual std::vector< storm::expressions::Expression >	getUnsatAssumptions () override
	If the last call to checkWithAssumptions() returned Unsat, this function can be used to retrieve a subset of the assumptions such that the assertion stack and these assumptions are unsatisfiable.

virtual bool	setTimeout (uint_fast64_t milliseconds) override
	If supported by the solver, this will limit all subsequent satisfiability queries to the given number of milliseconds.

virtual bool	unsetTimeout () override
	If supported by the solver, this unsets a previous timeout.

virtual std::string	getSmtLibString () const override
	If supported by the solver, this function returns the current assertions in the SMT-LIB format.

Public Member Functions inherited from storm::solver::SmtSolver
	SmtSolver (storm::expressions::ExpressionManager &manager)
	Constructs a new Smt solver with the given options.

virtual	~SmtSolver ()
	Destructs the solver instance.

	SmtSolver (SmtSolver const &other)=default

	SmtSolver (SmtSolver &&other)=default

SmtSolver &	operator= (SmtSolver const &other)=delete

SmtSolver &	operator= (SmtSolver &&other)=delete

void	add (std::set< storm::expressions::Expression > const &assertions)
	Adds the given set of assertions to the solver's stack.

void	add (std::initializer_list< storm::expressions::Expression > const &assertions)
	Adds the given list of assertions to the solver's stack.

virtual std::vector< storm::expressions::Expression >	getUnsatCore ()
	If the last call to check() returned Unsat, this function can be used to retrieve the unsatisfiable core of the assertions on the solver's stack, provided that the solver has been instantiated with support for the generation of unsatisfiable cores.

virtual void	setInterpolationGroup (uint_fast64_t group)
	Sets the current interpolation group.

virtual storm::expressions::Expression	getInterpolant (std::vector< uint_fast64_t > const &groupsA)
	If the last call to check() returned Unsat, the solver has been instantiated with support for interpolant generation and at least two non-empty interpolation groups have been added, the function can be used to retrieve an interpolant for the pair (A, B) of formulas where A is the conjunction of all the assertions in the groups provided as a parameter and B is the set of all other assertions.

storm::expressions::ExpressionManager const &	getManager () const
	Retrieves the expression manager associated with the solver.

storm::expressions::ExpressionManager &	getManager ()
	Retrieves the expression manager associated with the solver.

Additional Inherited Members
Public Types inherited from storm::solver::SmtSolver
enum class	CheckResult { Sat , Unsat , Unknown }
	possible check results More...

Detailed Description

Definition at line 15 of file Z3SmtSolver.h.

Constructor & Destructor Documentation

◆ Z3SmtSolver()

storm::solver::Z3SmtSolver::Z3SmtSolver ( storm::expressions::ExpressionManager & manager )

Definition at line 60 of file Z3SmtSolver.cpp.

◆ ~Z3SmtSolver()

storm::solver::Z3SmtSolver::~Z3SmtSolver ( )

virtual

Definition at line 80 of file Z3SmtSolver.cpp.

Member Function Documentation

◆ add()

void storm::solver::Z3SmtSolver::add ( storm::expressions::Expression const & assertion )

overridevirtual

Adds an assertion to the solver's stack.

Parameters

assertion The assertion to add.

Implements storm::solver::SmtSolver.

Definition at line 116 of file Z3SmtSolver.cpp.

◆ allSat() [1/3]

std::vector< storm::expressions::SimpleValuation > storm::solver::Z3SmtSolver::allSat ( std::vector< storm::expressions::Variable > const & important )

overridevirtual

Performs AllSat over the (provided) important atoms.

That is, this function returns all models of the assertions on the solver's stack.

Warning: If infinitely many models exist, this function will never return.

Parameters

important The set of important atoms over which to perform all sat.

Returns: the set of all valuations of the important atoms, such that the currently asserted formulas are satisfiable

Reimplemented from storm::solver::SmtSolver.

Definition at line 241 of file Z3SmtSolver.cpp.

◆ allSat() [2/3]

virtual uint_fast64_t storm::solver::Z3SmtSolver::allSat	(	std::vector< storm::expressions::Variable > const &	important,
		std::function< bool(ModelReference &)> const &	callback
	)

overridevirtual

Performs AllSat over the (provided) important atoms.

That is, this function determines all models of the assertions on the solver's stack. While doing so, every time a model is found, the provided callback is called and informed about the content of the current model. The callback function can signal to abort the enumeration process by returning false.

Parameters

important	The set of important atoms over which to perform all sat.
callback	A function to call for each found model.

Returns: The number of models of the important atoms that where found.

Reimplemented from storm::solver::SmtSolver.

◆ allSat() [3/3]

uint_fast64_t storm::solver::Z3SmtSolver::allSat	(	std::vector< storm::expressions::Variable > const &	important,
		std::function< bool(storm::expressions::SimpleValuation &)> const &	callback
	)

overridevirtual

Performs AllSat over the (provided) important atoms.

That is, this function determines all models of the assertions on the solver's stack. While doing so, every time a model is found, the provided callback is called and informed about the content of the current model. The callback function can signal to abort the enumeration process by returning false.

Parameters

important	The set of important atoms over which to perform all sat.
callback	A function to call for each found model.

Returns: The number of models of the important atoms that where found.

Reimplemented from storm::solver::SmtSolver.

Definition at line 255 of file Z3SmtSolver.cpp.

◆ check()

SmtSolver::CheckResult storm::solver::Z3SmtSolver::check ( )

overridevirtual

Checks whether the conjunction of assertions that are currently on the solver's stack is satisfiable.

Returns: Sat if the conjunction of the asserted expressions is satisfiable, Unsat if it is unsatisfiable and Unknown if the solver could not determine satisfiability.

Implements storm::solver::SmtSolver.

Definition at line 124 of file Z3SmtSolver.cpp.

◆ checkWithAssumptions() [1/2]

SmtSolver::CheckResult storm::solver::Z3SmtSolver::checkWithAssumptions ( std::initializer_list< storm::expressions::Expression > const & assumptions )

overridevirtual

Checks whether the conjunction of assertions that are currently on the solver's stack together with the provided assumptions is satisfiable.

The assumptions are, however, not added to the solver's stack, but are merely considered for this one call.

Parameters

assumptions The assumptions to add to the call.

Returns: Sat if the conjunction of the asserted expressions together with the provided assumptions is satisfiable, Unsat if it is unsatisfiable and Unknown if the solver could not determine satisfiability.

Implements storm::solver::SmtSolver.

Definition at line 171 of file Z3SmtSolver.cpp.

◆ checkWithAssumptions() [2/2]

SmtSolver::CheckResult storm::solver::Z3SmtSolver::checkWithAssumptions ( std::set< storm::expressions::Expression > const & assumptions )

overridevirtual

Checks whether the conjunction of assertions that are currently on the solver's stack together with the provided assumptions is satisfiable.

The assumptions are, however, not added to the solver's stack, but are merely considered for this one call.

Parameters

assumptions The assumptions to add to the call.

Returns: Sat if the conjunction of the asserted expressions together with the provided assumptions is satisfiable, Unsat if it is unsatisfiable and Unknown if the solver could not determine satisfiability.

Implements storm::solver::SmtSolver.

Definition at line 144 of file Z3SmtSolver.cpp.

◆ getModel()

std::shared_ptr< SmtSolver::ModelReference > storm::solver::Z3SmtSolver::getModel ( )

overridevirtual

If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model that satisfies all assertions on the solver's stack (as well as provided assumptions), provided that the solver was instantiated with support for model generation.

Note that this function may throw an exception if it is not called immediately after a call to check() or checkWithAssumptions() that returned Sat depending on the implementation.

Returns: A reference to a model that can be queried for the values of specific variables.

Reimplemented from storm::solver::SmtSolver.

Definition at line 207 of file Z3SmtSolver.cpp.

◆ getModelAsValuation()

storm::expressions::SimpleValuation storm::solver::Z3SmtSolver::getModelAsValuation ( )

overridevirtual

If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model that satisfies all assertions on the solver's stack (as well as provided assumptions), provided that the solver was instantiated with support for model generation.

Note that this function may throw an exception if it is not called immediately after a call to check() or checkWithAssumptions() that returned Sat depending on the implementation.

Returns: A valuation that holds the values of the variables in the current model.

Reimplemented from storm::solver::SmtSolver.

Definition at line 197 of file Z3SmtSolver.cpp.

◆ getSmtLibString()

std::string storm::solver::Z3SmtSolver::getSmtLibString ( ) const

overridevirtual

If supported by the solver, this function returns the current assertions in the SMT-LIB format.

Returns: the current assertions in the SMT-LIB format.

Reimplemented from storm::solver::SmtSolver.

Definition at line 381 of file Z3SmtSolver.cpp.

◆ getUnsatAssumptions()

std::vector< storm::expressions::Expression > storm::solver::Z3SmtSolver::getUnsatAssumptions ( )

overridevirtual

If the last call to checkWithAssumptions() returned Unsat, this function can be used to retrieve a subset of the assumptions such that the assertion stack and these assumptions are unsatisfiable.

This may only be called provided that the solver has been instantiated with support for the generation of unsatisfiable cores.

Returns: A subset of the assumptions of the last call to checkWithAssumptions whose conjunction with the solver's stack is unsatisfiable.

Reimplemented from storm::solver::SmtSolver.

Definition at line 339 of file Z3SmtSolver.cpp.

◆ pop() [1/2]

void storm::solver::Z3SmtSolver::pop ( )

overridevirtual

Pops a backtracking point from the solver's stack.

This deletes all assertions from the solver's stack that were added after the last call to push().

Implements storm::solver::SmtSolver.

Definition at line 92 of file Z3SmtSolver.cpp.

◆ pop() [2/2]

void storm::solver::Z3SmtSolver::pop ( uint_fast64_t n )

overridevirtual

Pops multiple backtracking points from the solver's stack in the same way as pop() does.

Parameters

n	The number of backtracking points to pop.

Reimplemented from storm::solver::SmtSolver.

Definition at line 100 of file Z3SmtSolver.cpp.

◆ push()

void storm::solver::Z3SmtSolver::push ( )

overridevirtual

Pushes a backtracking point on the solver's stack.

A following call to pop() deletes exactly those assertions from the solver's stack that were added after this call.

Implements storm::solver::SmtSolver.

Definition at line 84 of file Z3SmtSolver.cpp.

◆ reset()

void storm::solver::Z3SmtSolver::reset ( )

overridevirtual

Removes all assertions from the solver's stack.

Implements storm::solver::SmtSolver.

Definition at line 108 of file Z3SmtSolver.cpp.

◆ setTimeout()

bool storm::solver::Z3SmtSolver::setTimeout ( uint_fast64_t milliseconds )

overridevirtual

If supported by the solver, this will limit all subsequent satisfiability queries to the given number of milliseconds.

Parameters

milliseconds The amount of milliseconds before timing out.

Returns: True iff the solver supports setting a timeout.

Reimplemented from storm::solver::SmtSolver.

Definition at line 359 of file Z3SmtSolver.cpp.

◆ unsetTimeout()

bool storm::solver::Z3SmtSolver::unsetTimeout ( )

overridevirtual

If supported by the solver, this unsets a previous timeout.

Returns: True iff the solver supports timeouts.

Reimplemented from storm::solver::SmtSolver.

Definition at line 370 of file Z3SmtSolver.cpp.

The documentation for this class was generated from the following files:

src/storm/solver/Z3SmtSolver.h
src/storm/solver/Z3SmtSolver.cpp

Classes

Public Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ Z3SmtSolver()

◆ ~Z3SmtSolver()

Member Function Documentation

◆ add()

◆ allSat() [1/3]

◆ allSat() [2/3]

◆ allSat() [3/3]

◆ check()

◆ checkWithAssumptions() [1/2]

◆ checkWithAssumptions() [2/2]

◆ getModel()

◆ getModelAsValuation()

◆ getSmtLibString()

◆ getUnsatAssumptions()

◆ pop() [1/2]

◆ pop() [2/2]

◆ push()

◆ reset()

◆ setTimeout()

◆ unsetTimeout()