This class represents an SMT-LIBv2 conforming solver. More...

#include <SmtlibSmtSolver.h>

Inheritance diagram for storm::solver::SmtlibSmtSolver:

Collaboration diagram for storm::solver::SmtlibSmtSolver:

Classes
class	SmtlibModelReference

Public Member Functions
	SmtlibSmtSolver (storm::expressions::ExpressionManager &manager, bool useCarlExpressions=false)
	Creates a new solver with the given manager.

virtual	~SmtlibSmtSolver ()

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.

bool	isNeedsRestart () const

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

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

Detailed Description

This class represents an SMT-LIBv2 conforming solver.

Any SMT-LIBv2 conforming solver can be called and will be opened as a child process. It is also possible to export the SMT2 script for later use.

Note: The parsing of the solver responses is a little bit crude and might cause bugs (e.g., if a variable name has the infix "error")

Definition at line 20 of file SmtlibSmtSolver.h.

Constructor & Destructor Documentation

◆ SmtlibSmtSolver()

storm::solver::SmtlibSmtSolver::SmtlibSmtSolver	(	storm::expressions::ExpressionManager &	manager,
		bool	useCarlExpressions = `false`
	)

Creates a new solver with the given manager.

In addition to storm expressions, this solver also allows carl expressions (but not both to not confuse variables). Hence, there is a flag to chose between the two

Definition at line 49 of file SmtlibSmtSolver.cpp.

◆ ~SmtlibSmtSolver()

storm::solver::SmtlibSmtSolver::~SmtlibSmtSolver ( )

virtual

Definition at line 62 of file SmtlibSmtSolver.cpp.

Member Function Documentation

◆ add()

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

◆ check()

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

◆ checkWithAssumptions() [1/2]

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

◆ checkWithAssumptions() [2/2]

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

◆ isNeedsRestart()

bool storm::solver::SmtlibSmtSolver::isNeedsRestart ( ) const

Definition at line 244 of file SmtlibSmtSolver.cpp.

◆ pop() [1/2]

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

◆ pop() [2/2]

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

◆ push()

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

◆ reset()

void storm::solver::SmtlibSmtSolver::reset ( )

overridevirtual

Removes all assertions from the solver's stack.

Implements storm::solver::SmtSolver.

Definition at line 91 of file SmtlibSmtSolver.cpp.

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

src/storm/solver/SmtlibSmtSolver.h
src/storm/solver/SmtlibSmtSolver.cpp

Classes

Public Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ SmtlibSmtSolver()

◆ ~SmtlibSmtSolver()

Member Function Documentation

◆ add()

◆ check()

◆ checkWithAssumptions() [1/2]

◆ checkWithAssumptions() [2/2]

◆ isNeedsRestart()

◆ pop() [1/2]

◆ pop() [2/2]

◆ push()

◆ reset()