Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
SmtSolver.h
Go to the documentation of this file.
1#ifndef STORM_SOLVER_SMTSOLVER
2#define STORM_SOLVER_SMTSOLVER
3
4#include <cstdint>
5
9
10#include <functional>
11#include <initializer_list>
12#include <set>
13#include <unordered_set>
14#include <vector>
15
16namespace storm {
17namespace solver {
18
22class SmtSolver {
23 public:
25 enum class CheckResult { Sat, Unsat, Unknown };
26
32 public:
39 virtual ~ModelReference() = default;
40
41 virtual bool getBooleanValue(storm::expressions::Variable const& variable) const = 0;
42 virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const = 0;
43 virtual double getRationalValue(storm::expressions::Variable const& variable) const = 0;
44
51
52 virtual std::string toString() const = 0;
53
54 private:
55 // The expression manager responsible for the variables whose value can be requested via this model
56 // reference.
58 };
59
60 public:
69
73 virtual ~SmtSolver();
74
75 SmtSolver(SmtSolver const& other) = default;
76
77 SmtSolver(SmtSolver&& other) = default;
78 SmtSolver& operator=(SmtSolver const& other) = delete;
79 SmtSolver& operator=(SmtSolver&& other) = delete;
80
85 virtual void push() = 0;
86
91 virtual void pop() = 0;
92
98 virtual void pop(uint_fast64_t n);
99
103 virtual void reset() = 0;
104
110 virtual void add(storm::expressions::Expression const& assertion) = 0;
111
117 void add(std::set<storm::expressions::Expression> const& assertions);
118
124 void add(std::initializer_list<storm::expressions::Expression> const& assertions);
125
132 virtual CheckResult check() = 0;
133
143 virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) = 0;
144
154 virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) = 0;
155
166
176 virtual std::shared_ptr<ModelReference> getModel();
177
188 virtual std::vector<storm::expressions::SimpleValuation> allSat(std::vector<storm::expressions::Variable> const& important);
189
201 virtual uint_fast64_t allSat(std::vector<storm::expressions::Variable> const& important,
202 std::function<bool(storm::expressions::SimpleValuation&)> const& callback);
203
215 virtual uint_fast64_t allSat(std::vector<storm::expressions::Variable> const& important, std::function<bool(ModelReference&)> const& callback);
216
224 virtual std::vector<storm::expressions::Expression> getUnsatCore();
225
235 virtual std::vector<storm::expressions::Expression> getUnsatAssumptions();
236
246 virtual void setInterpolationGroup(uint_fast64_t group);
247
260 virtual storm::expressions::Expression getInterpolant(std::vector<uint_fast64_t> const& groupsA);
261
268
275
283 virtual bool setTimeout(uint_fast64_t milliseconds);
284
290 virtual bool unsetTimeout();
291
297 virtual std::string getSmtLibString() const;
298
299 private:
300 // The manager responsible for the expressions that interact with this solver.
302};
303} // namespace solver
304} // namespace storm
305
306#endif // STORM_SOLVER_SMTSOLVER
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.
Definition SmtSolver.h:31
virtual int_fast64_t getIntegerValue(storm::expressions::Variable const &variable) const =0
virtual std::string toString() const =0
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.
Definition SmtSolver.cpp:13
virtual double getRationalValue(storm::expressions::Variable const &variable) const =0
An interface that captures the functionality of an SMT solver.
Definition SmtSolver.h:22
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...
Definition SmtSolver.cpp:75
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...
Definition SmtSolver.cpp:87
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...
Definition SmtSolver.cpp:67
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.
Definition SmtSolver.cpp:91
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...
Definition SmtSolver.cpp:43
storm::expressions::ExpressionManager const & getManager() const
Retrieves the expression manager associated with the solver.
Definition SmtSolver.cpp:79
virtual std::vector< storm::expressions::SimpleValuation > allSat(std::vector< storm::expressions::Variable > const &important)
Performs AllSat over the (provided) important atoms.
Definition SmtSolver.cpp:51
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.
Definition SmtSolver.cpp:21
SmtSolver(SmtSolver const &other)=default
virtual void setInterpolationGroup(uint_fast64_t group)
Sets the current interpolation group.
Definition SmtSolver.cpp:71
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.
Definition SmtSolver.cpp:95
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...
Definition SmtSolver.cpp:63
virtual std::shared_ptr< ModelReference > getModel()
If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model tha...
Definition SmtSolver.cpp:47
CheckResult
possible check results
Definition SmtSolver.h:25
LabParser.cpp.
Definition cli.cpp:18