Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
MathsatSmtSolver.h
Go to the documentation of this file.
1#ifndef STORM_SOLVER_MATHSATSMTSOLVER
2#define STORM_SOLVER_MATHSATSMTSOLVER
3
4#include <boost/container/flat_map.hpp>
5#include "storm-config.h"
8
9#ifdef STORM_HAVE_MATHSAT
10#include "mathsat.h"
11#endif
12
13namespace storm {
14namespace solver {
16 public:
35
36#ifdef STORM_HAVE_MATHSAT
37 class MathsatAllsatModelReference : public SmtSolver::ModelReference {
38 public:
39 MathsatAllsatModelReference(storm::expressions::ExpressionManager const& manager, msat_env const& env, msat_term* model,
40 std::unordered_map<storm::expressions::Variable, uint_fast64_t> const& variableNameToSlotMapping);
41
42 virtual bool getBooleanValue(storm::expressions::Variable const& variable) const override;
43 virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const override;
44 virtual double getRationalValue(storm::expressions::Variable const& variable) const override;
45 virtual std::string toString() const override;
46
47 private:
48 msat_env const& env;
49 msat_term* model;
50 std::unordered_map<storm::expressions::Variable, uint_fast64_t> const& variableToSlotMapping;
51 };
52#endif
53
54#ifdef STORM_HAVE_MATHSAT
55 class MathsatModelReference : public SmtSolver::ModelReference {
56 public:
57 MathsatModelReference(storm::expressions::ExpressionManager const& manager, msat_env const& env,
58 storm::adapters::MathsatExpressionAdapter& expressionAdapter);
59
60 virtual bool getBooleanValue(storm::expressions::Variable const& variable) const override;
61 virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const override;
62 virtual double getRationalValue(storm::expressions::Variable const& variable) const override;
63 virtual std::string toString() const override;
64
65 private:
66 msat_env const& env;
67 storm::adapters::MathsatExpressionAdapter& expressionAdapter;
68 };
69#endif
70
71 MathsatSmtSolver(storm::expressions::ExpressionManager& manager, Options const& options = Options());
72
73 virtual ~MathsatSmtSolver();
74
75 virtual void push() override;
76
77 virtual void pop() override;
78
79 virtual void pop(uint_fast64_t n) override;
80
81 virtual void reset() override;
82
83 virtual void add(storm::expressions::Expression const& assertion) override;
84
85 virtual CheckResult check() override;
86
87 virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) override;
88
89 virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) override;
90
92
93 virtual std::shared_ptr<SmtSolver::ModelReference> getModel() override;
94
95 virtual std::vector<storm::expressions::SimpleValuation> allSat(std::vector<storm::expressions::Variable> const& important) override;
96
97 virtual uint_fast64_t allSat(std::vector<storm::expressions::Variable> const& important,
98 std::function<bool(storm::expressions::SimpleValuation&)> const& callback) override;
99
100 virtual uint_fast64_t allSat(std::vector<storm::expressions::Variable> const& important, std::function<bool(ModelReference&)> const& callback) override;
101
102 virtual std::vector<storm::expressions::Expression> getUnsatAssumptions() override;
103
104 virtual void setInterpolationGroup(uint_fast64_t group) override;
105
106 virtual storm::expressions::Expression getInterpolant(std::vector<uint_fast64_t> const& groupsA) override;
107
108 private:
109 storm::expressions::SimpleValuation convertMathsatModelToValuation();
110
111#ifdef STORM_HAVE_MATHSAT
112 // The MathSAT environment.
113 msat_env env;
114
115 // The expression adapter used to translate expressions to MathSAT's format. This has to be a pointer, since
116 // it must be initialized after creating the environment, but the adapter class has no default constructor.
117 std::unique_ptr<storm::adapters::MathsatExpressionAdapter> expressionAdapter;
118#endif
119
120 // A flag storing whether the last call was a check involving assumptions.
121 bool lastCheckAssumptions;
122
123 // The result of the last call to any of the check methods.
124 CheckResult lastResult;
125
126 // A mapping of interpolation group indices to their MathSAT identifier.
127 typedef boost::container::flat_map<uint_fast64_t, int> InterpolationGroupMapType;
128 InterpolationGroupMapType interpolationGroups;
129};
130} // namespace solver
131} // namespace storm
132#endif // STORM_SOLVER_MATHSATSMTSOLVER
This class is responsible for managing a set of typed variables and all expressions using these varia...
A simple implementation of the valuation interface.
A class that captures options that may be passed to the Mathsat solver.
Options(bool enableModelGeneration=true, bool enableUnsatCoreGeneration=false, bool enableInterpolantGeneration=false)
virtual std::vector< storm::expressions::Expression > getUnsatAssumptions() override
If the last call to checkWithAssumptions() returned Unsat, this function can be used to retrieve a su...
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 interpo...
virtual std::shared_ptr< SmtSolver::ModelReference > getModel() override
If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model tha...
virtual void add(storm::expressions::Expression const &assertion) override
Adds an assertion to the solver's stack.
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 void pop() override
Pops a backtracking point from 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 void reset() override
Removes all assertions from the solver's stack.
virtual std::vector< storm::expressions::SimpleValuation > allSat(std::vector< storm::expressions::Variable > const &important) override
Performs AllSat over the (provided) important atoms.
virtual void push() override
Pushes a backtracking point on the solver's stack.
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 t...
virtual storm::expressions::SimpleValuation getModelAsValuation() override
If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model tha...
virtual void setInterpolationGroup(uint_fast64_t group) override
Sets the current interpolation group.
The base class for all model references.
Definition SmtSolver.h:31
An interface that captures the functionality of an SMT solver.
Definition SmtSolver.h:22
CheckResult
possible check results
Definition SmtSolver.h:25
LabParser.cpp.