#include <MathsatSmtSolver.h>

Inheritance diagram for storm::solver::MathsatSmtSolver:

Collaboration diagram for storm::solver::MathsatSmtSolver:

Classes
class	Options
	A class that captures options that may be passed to the Mathsat solver. More...

Public Member Functions
	MathsatSmtSolver (storm::expressions::ExpressionManager &manager, Options const &options=Options())

virtual	~MathsatSmtSolver ()

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 void	setInterpolationGroup (uint_fast64_t group) override
	Sets the current interpolation group.

virtual storm::expressions::Expression	getInterpolant (std::vector< uint_fast64_t > const &groupsA) override
	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.

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.

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.

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 MathsatSmtSolver.h.

Constructor & Destructor Documentation

◆ MathsatSmtSolver()

storm::solver::MathsatSmtSolver::MathsatSmtSolver	(	storm::expressions::ExpressionManager &	manager,
		Options const &	options = `Options()`
	)

Definition at line 116 of file MathsatSmtSolver.cpp.

◆ ~MathsatSmtSolver()

storm::solver::MathsatSmtSolver::~MathsatSmtSolver ( )

virtual

Definition at line 149 of file MathsatSmtSolver.cpp.

Member Function Documentation

◆ add()

void storm::solver::MathsatSmtSolver::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 194 of file MathsatSmtSolver.cpp.

◆ allSat() [1/3]

std::vector< storm::expressions::SimpleValuation > storm::solver::MathsatSmtSolver::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 334 of file MathsatSmtSolver.cpp.

◆ allSat() [2/3]

virtual uint_fast64_t storm::solver::MathsatSmtSolver::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::MathsatSmtSolver::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 427 of file MathsatSmtSolver.cpp.

◆ check()

SmtSolver::CheckResult storm::solver::MathsatSmtSolver::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 209 of file MathsatSmtSolver.cpp.

◆ checkWithAssumptions() [1/2]

SmtSolver::CheckResult storm::solver::MathsatSmtSolver::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 257 of file MathsatSmtSolver.cpp.

◆ checkWithAssumptions() [2/2]

SmtSolver::CheckResult storm::solver::MathsatSmtSolver::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 229 of file MathsatSmtSolver.cpp.

◆ getInterpolant()

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

overridevirtual

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 from storm::solver::SmtSolver.

Definition at line 523 of file MathsatSmtSolver.cpp.

◆ getModel()

std::shared_ptr< SmtSolver::ModelReference > storm::solver::MathsatSmtSolver::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 295 of file MathsatSmtSolver.cpp.

◆ getModelAsValuation()

storm::expressions::SimpleValuation storm::solver::MathsatSmtSolver::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 285 of file MathsatSmtSolver.cpp.

◆ getUnsatAssumptions()

std::vector< storm::expressions::Expression > storm::solver::MathsatSmtSolver::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 485 of file MathsatSmtSolver.cpp.

◆ pop() [1/2]

void storm::solver::MathsatSmtSolver::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 169 of file MathsatSmtSolver.cpp.

◆ pop() [2/2]

void storm::solver::MathsatSmtSolver::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 177 of file MathsatSmtSolver.cpp.

◆ push()

void storm::solver::MathsatSmtSolver::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 161 of file MathsatSmtSolver.cpp.

◆ reset()

void storm::solver::MathsatSmtSolver::reset ( )

overridevirtual

Removes all assertions from the solver's stack.

Implements storm::solver::SmtSolver.

Definition at line 186 of file MathsatSmtSolver.cpp.

◆ setInterpolationGroup()

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

overridevirtual

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 from storm::solver::SmtSolver.

Definition at line 508 of file MathsatSmtSolver.cpp.

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

src/storm/solver/MathsatSmtSolver.h
src/storm/solver/MathsatSmtSolver.cpp

Classes

Public Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ MathsatSmtSolver()

◆ ~MathsatSmtSolver()

Member Function Documentation

◆ add()

◆ allSat() [1/3]

◆ allSat() [2/3]

◆ allSat() [3/3]

◆ check()

◆ checkWithAssumptions() [1/2]

◆ checkWithAssumptions() [2/2]

◆ getInterpolant()

◆ getModel()

◆ getModelAsValuation()

◆ getUnsatAssumptions()

◆ pop() [1/2]

◆ pop() [2/2]

◆ push()

◆ reset()

◆ setInterpolationGroup()