An interface that captures the functionality of an SMT solver. More...

#include <SmtSolver.h>

Inheritance diagram for storm::solver::SmtSolver:

[legend]

Classes
class	ModelReference
	The base class for all model references. More...

Public Types
enum class	CheckResult { Sat , Unsat , Unknown }
	possible check results More...

Public Member Functions
	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

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

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

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

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

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

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 CheckResult	check ()=0
	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)=0
	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)=0
	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 ()
	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< ModelReference >	getModel ()
	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)
	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)
	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)
	Performs AllSat over the (provided) important atoms.

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 std::vector< storm::expressions::Expression >	getUnsatAssumptions ()
	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 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.

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

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

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

Detailed Description

An interface that captures the functionality of an SMT solver.

Definition at line 22 of file SmtSolver.h.

Member Enumeration Documentation

◆ CheckResult

enum class storm::solver::SmtSolver::CheckResult

strong

possible check results

Enumerator
Sat
Unsat
Unknown

Definition at line 25 of file SmtSolver.h.

Constructor & Destructor Documentation

◆ SmtSolver() [1/3]

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

Constructs a new Smt solver with the given options.

Parameters

manager The expression manager responsible for all expressions that in some way or another interact with this solver.

Exceptions

storm::exceptions::IllegalArgumentValueException if an option is unsupported for the solver.

Definition at line 17 of file SmtSolver.cpp.

◆ ~SmtSolver()

storm::solver::SmtSolver::~SmtSolver ( )

virtual

Destructs the solver instance.

Definition at line 21 of file SmtSolver.cpp.

◆ SmtSolver() [2/3]

storm::solver::SmtSolver::SmtSolver ( SmtSolver const & other )

default

◆ SmtSolver() [3/3]

storm::solver::SmtSolver::SmtSolver ( SmtSolver && other )

default

Member Function Documentation

◆ add() [1/3]

void storm::solver::SmtSolver::add ( std::initializer_list< storm::expressions::Expression > const & assertions )

Adds the given list of assertions to the solver's stack.

Parameters

assertions The assertions to add.

Definition at line 31 of file SmtSolver.cpp.

◆ add() [2/3]

void storm::solver::SmtSolver::add ( std::set< storm::expressions::Expression > const & assertions )

Adds the given set of assertions to the solver's stack.

Parameters

assertions The assertions to add.

Definition at line 25 of file SmtSolver.cpp.

◆ add() [3/3]

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

pure virtual

Adds an assertion to the solver's stack.

Parameters

assertion The assertion to add.

Implemented in storm::solver::MathsatSmtSolver, storm::solver::SmtlibSmtSolver, and storm::solver::Z3SmtSolver.

◆ allSat() [1/3]

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

virtual

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 in storm::solver::MathsatSmtSolver, and storm::solver::Z3SmtSolver.

Definition at line 51 of file SmtSolver.cpp.

◆ allSat() [2/3]

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

virtual

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 in storm::solver::MathsatSmtSolver, and storm::solver::Z3SmtSolver.

Definition at line 59 of file SmtSolver.cpp.

◆ allSat() [3/3]

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

virtual

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 in storm::solver::MathsatSmtSolver, and storm::solver::Z3SmtSolver.

Definition at line 55 of file SmtSolver.cpp.

◆ check()

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

pure virtual

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.

Implemented in storm::solver::MathsatSmtSolver, storm::solver::SmtlibSmtSolver, and storm::solver::Z3SmtSolver.

◆ checkWithAssumptions() [1/2]

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

pure virtual

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.

Implemented in storm::solver::MathsatSmtSolver, storm::solver::SmtlibSmtSolver, and storm::solver::Z3SmtSolver.

◆ checkWithAssumptions() [2/2]

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

pure virtual

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.

Implemented in storm::solver::MathsatSmtSolver, storm::solver::SmtlibSmtSolver, and storm::solver::Z3SmtSolver.

◆ getInterpolant()

storm::expressions::Expression storm::solver::SmtSolver::getInterpolant ( std::vector< uint_fast64_t > const & groupsA )

virtual

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.

To obtain meaningful results, the conjunction of the formulas within one group should be satisfiable.

Parameters

groupsA The indices of all interpolation groups whose conjunctions form the formula A.

Returns: The interpolant for the formulas (A, B), i.e. an expression I that is implied by A but the conjunction of I and B is inconsistent.

Reimplemented in storm::solver::MathsatSmtSolver.

Definition at line 75 of file SmtSolver.cpp.

◆ getManager() [1/2]

storm::expressions::ExpressionManager & storm::solver::SmtSolver::getManager ( )

Retrieves the expression manager associated with the solver.

Returns: The expression manager associated with the solver.

Definition at line 83 of file SmtSolver.cpp.

◆ getManager() [2/2]

storm::expressions::ExpressionManager const & storm::solver::SmtSolver::getManager ( ) const

Retrieves the expression manager associated with the solver.

Returns: The expression manager associated with the solver.

Definition at line 79 of file SmtSolver.cpp.

◆ getModel()

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

virtual

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 in storm::solver::MathsatSmtSolver, and storm::solver::Z3SmtSolver.

Definition at line 47 of file SmtSolver.cpp.

◆ getModelAsValuation()

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

virtual

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 in storm::solver::MathsatSmtSolver, and storm::solver::Z3SmtSolver.

Definition at line 43 of file SmtSolver.cpp.

◆ getSmtLibString()

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

virtual

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 in storm::solver::Z3SmtSolver.

Definition at line 95 of file SmtSolver.cpp.

◆ getUnsatAssumptions()

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

virtual

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 in storm::solver::MathsatSmtSolver, and storm::solver::Z3SmtSolver.

Definition at line 67 of file SmtSolver.cpp.

◆ getUnsatCore()

std::vector< storm::expressions::Expression > storm::solver::SmtSolver::getUnsatCore ( )

virtual

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.

Returns: A subset of the asserted formulas whose conjunction is unsatisfiable.

Definition at line 63 of file SmtSolver.cpp.

◆ operator=() [1/2]

SmtSolver & storm::solver::SmtSolver::operator= ( SmtSolver && other )

delete

◆ operator=() [2/2]

SmtSolver & storm::solver::SmtSolver::operator= ( SmtSolver const & other )

delete

◆ pop() [1/2]

virtual void storm::solver::SmtSolver::pop ( )

pure virtual

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().

Implemented in storm::solver::MathsatSmtSolver, storm::solver::SmtlibSmtSolver, and storm::solver::Z3SmtSolver.

◆ pop() [2/2]

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

virtual

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 in storm::solver::MathsatSmtSolver, storm::solver::SmtlibSmtSolver, and storm::solver::Z3SmtSolver.

Definition at line 37 of file SmtSolver.cpp.

◆ push()

virtual void storm::solver::SmtSolver::push ( )

pure virtual

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.

Implemented in storm::solver::MathsatSmtSolver, storm::solver::SmtlibSmtSolver, and storm::solver::Z3SmtSolver.

◆ reset()

virtual void storm::solver::SmtSolver::reset ( )

pure virtual

Removes all assertions from the solver's stack.

Implemented in storm::solver::MathsatSmtSolver, storm::solver::SmtlibSmtSolver, and storm::solver::Z3SmtSolver.

◆ setInterpolationGroup()

void storm::solver::SmtSolver::setInterpolationGroup ( uint_fast64_t group )

virtual

Sets the current interpolation group.

All terms added to the assertion stack after this call will belong to the set group until the next call to this function. Note that, depending on the solver, it might not be possible to "re-open" groups, so this should be used with care. Also, this functionality is only available if the solver has been instantiated with support for interpolant generation.

Parameters

group The index of the interpolation group with which all assertions added after this call will be associated.

Reimplemented in storm::solver::MathsatSmtSolver.

Definition at line 71 of file SmtSolver.cpp.

◆ setTimeout()

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

virtual

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 in storm::solver::Z3SmtSolver.

Definition at line 87 of file SmtSolver.cpp.

◆ unsetTimeout()

bool storm::solver::SmtSolver::unsetTimeout ( )

virtual

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

Returns: True iff the solver supports timeouts.

Reimplemented in storm::solver::Z3SmtSolver.

Definition at line 91 of file SmtSolver.cpp.

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

src/storm/solver/SmtSolver.h
src/storm/solver/SmtSolver.cpp

Classes

Public Types

Public Member Functions

Detailed Description

Member Enumeration Documentation

◆ CheckResult

Constructor & Destructor Documentation

◆ SmtSolver() [1/3]

◆ ~SmtSolver()

◆ SmtSolver() [2/3]

◆ SmtSolver() [3/3]

Member Function Documentation

◆ add() [1/3]

◆ add() [2/3]

◆ add() [3/3]

◆ allSat() [1/3]

◆ allSat() [2/3]

◆ allSat() [3/3]

◆ check()

◆ checkWithAssumptions() [1/2]

◆ checkWithAssumptions() [2/2]

◆ getInterpolant()

◆ getManager() [1/2]

◆ getManager() [2/2]

◆ getModel()

◆ getModelAsValuation()

◆ getSmtLibString()

◆ getUnsatAssumptions()

◆ getUnsatCore()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ pop() [1/2]

◆ pop() [2/2]

◆ push()

◆ reset()

◆ setInterpolationGroup()

◆ setTimeout()

◆ unsetTimeout()