1#ifndef STORM_SOLVER_SMTSOLVER
2#define STORM_SOLVER_SMTSOLVER
11#include <initializer_list>
13#include <unordered_set>
91 virtual void pop() = 0;
98 virtual void pop(uint_fast64_t n);
117 void add(std::set<storm::expressions::Expression>
const& assertions);
124 void add(std::initializer_list<storm::expressions::Expression>
const& assertions);
176 virtual std::shared_ptr<ModelReference>
getModel();
188 virtual std::vector<storm::expressions::SimpleValuation>
allSat(std::vector<storm::expressions::Variable>
const& important);
201 virtual uint_fast64_t
allSat(std::vector<storm::expressions::Variable>
const& important,
215 virtual uint_fast64_t
allSat(std::vector<storm::expressions::Variable>
const& important, std::function<
bool(
ModelReference&)>
const& callback);
224 virtual std::vector<storm::expressions::Expression>
getUnsatCore();
283 virtual bool setTimeout(uint_fast64_t milliseconds);
This class is responsible for managing a set of typed variables and all expressions using these varia...
A simple implementation of the valuation interface.
The base class for all model references.
virtual int_fast64_t getIntegerValue(storm::expressions::Variable const &variable) const =0
virtual std::string toString() const =0
virtual ~ModelReference()=default
virtual bool getBooleanValue(storm::expressions::Variable const &variable) const =0
storm::expressions::ExpressionManager const & getManager() const
Retrieves the expression manager associated with this model reference.
virtual double getRationalValue(storm::expressions::Variable const &variable) const =0
An interface that captures the functionality of an SMT solver.
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 interpo...
virtual void pop()=0
Pops a backtracking point from the solver's stack.
virtual void reset()=0
Removes all assertions from the solver's stack.
virtual bool setTimeout(uint_fast64_t milliseconds)
If supported by the solver, this will limit all subsequent satisfiability queries to the given number...
SmtSolver & operator=(SmtSolver const &other)=delete
virtual std::vector< storm::expressions::Expression > getUnsatAssumptions()
If the last call to checkWithAssumptions() returned Unsat, this function can be used to retrieve a su...
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 t...
virtual void add(storm::expressions::Expression const &assertion)=0
Adds an assertion to the solver's stack.
virtual bool unsetTimeout()
If supported by the solver, this unsets a previous timeout.
SmtSolver & operator=(SmtSolver &&other)=delete
virtual storm::expressions::SimpleValuation getModelAsValuation()
If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model tha...
storm::expressions::ExpressionManager const & getManager() const
Retrieves the expression manager associated with the solver.
virtual std::vector< storm::expressions::SimpleValuation > allSat(std::vector< storm::expressions::Variable > const &important)
Performs AllSat over the (provided) important atoms.
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 t...
virtual ~SmtSolver()
Destructs the solver instance.
SmtSolver(SmtSolver const &other)=default
virtual void setInterpolationGroup(uint_fast64_t group)
Sets the current interpolation group.
virtual void push()=0
Pushes a backtracking point on the solver's stack.
SmtSolver(SmtSolver &&other)=default
virtual std::string getSmtLibString() const
If supported by the solver, this function returns the current assertions in the SMT-LIB format.
virtual std::vector< storm::expressions::Expression > getUnsatCore()
If the last call to check() returned Unsat, this function can be used to retrieve the unsatisfiable c...
virtual std::shared_ptr< ModelReference > getModel()
If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model tha...
CheckResult
possible check results