#include <Cvc5SmtSolver.h>

Inheritance diagram for storm::solver::Cvc5SmtSolver:

Collaboration diagram for storm::solver::Cvc5SmtSolver:

Classes
class	Cvc5ModelReference

Public Member Functions
	Cvc5SmtSolver (storm::expressions::ExpressionManager &manager)
virtual	~Cvc5SmtSolver ()
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 void	addNotCurrentModel (bool performSolverReset=true) override
	If supported by the solver, this function tells the SMT solver to produce a model different from the current model.
virtual CheckResult	check () override
	Checks whether the conjunction of assertions that are currently on the solver's stack is satisfiable.
virtual CheckResult	checkWithAssumptions (storm::expressions::ExpressionSet 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.
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 (storm::expressions::ExpressionSet 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.
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 12 of file Cvc5SmtSolver.h.

Constructor & Destructor Documentation

◆ Cvc5SmtSolver()

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

Definition at line 55 of file Cvc5SmtSolver.cpp.

◆ ~Cvc5SmtSolver()

storm::solver::Cvc5SmtSolver::~Cvc5SmtSolver ( )

virtual

Definition at line 76 of file Cvc5SmtSolver.cpp.

Member Function Documentation

◆ add()

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

◆ addNotCurrentModel()

void storm::solver::Cvc5SmtSolver::addNotCurrentModel ( bool performSolverReset = true )

overridevirtual

If supported by the solver, this function tells the SMT solver to produce a model different from the current model.

Reimplemented from storm::solver::SmtSolver.

Definition at line 120 of file Cvc5SmtSolver.cpp.

◆ allSat() [1/3]

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

◆ allSat() [2/3]

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

◆ check()

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

◆ checkWithAssumptions() [1/2]

SmtSolver::CheckResult storm::solver::Cvc5SmtSolver::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 Cvc5SmtSolver.cpp.

◆ checkWithAssumptions() [2/2]

SmtSolver::CheckResult storm::solver::Cvc5SmtSolver::checkWithAssumptions ( storm::expressions::ExpressionSet 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 154 of file Cvc5SmtSolver.cpp.

◆ getModel()

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

◆ getModelAsValuation()

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

◆ getUnsatAssumptions()

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

◆ pop() [1/2]

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

◆ pop() [2/2]

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

◆ push()

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

◆ reset()

void storm::solver::Cvc5SmtSolver::reset ( )

overridevirtual

Removes all assertions from the solver's stack.

Implements storm::solver::SmtSolver.

Definition at line 104 of file Cvc5SmtSolver.cpp.

◆ setTimeout()

bool storm::solver::Cvc5SmtSolver::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 345 of file Cvc5SmtSolver.cpp.

◆ unsetTimeout()

bool storm::solver::Cvc5SmtSolver::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 354 of file Cvc5SmtSolver.cpp.

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

src/storm/solver/Cvc5SmtSolver.h
src/storm/solver/Cvc5SmtSolver.cpp

Classes

Public Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ Cvc5SmtSolver()

◆ ~Cvc5SmtSolver()

Member Function Documentation

◆ add()

◆ addNotCurrentModel()

◆ allSat() [1/3]

◆ allSat() [2/3]

◆ allSat() [3/3]

◆ check()

◆ checkWithAssumptions() [1/2]

◆ checkWithAssumptions() [2/2]

◆ getModel()

◆ getModelAsValuation()

◆ getUnsatAssumptions()

◆ pop() [1/2]

◆ pop() [2/2]

◆ push()

◆ reset()

◆ setTimeout()

◆ unsetTimeout()