Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
Z3SmtSolver.cpp
Go to the documentation of this file.
6
7namespace storm {
8namespace solver {
9#ifdef STORM_HAVE_Z3
10Z3SmtSolver::Z3ModelReference::Z3ModelReference(storm::expressions::ExpressionManager const& manager, z3::model const& model,
11 storm::adapters::Z3ExpressionAdapter& expressionAdapter)
12 : ModelReference(manager), model(model), expressionAdapter(expressionAdapter) {
13 // Intentionally left empty.
14}
15#endif
16
17bool Z3SmtSolver::Z3ModelReference::getBooleanValue(storm::expressions::Variable const& variable) const {
18#ifdef STORM_HAVE_Z3
19 STORM_LOG_ASSERT(variable.getManager() == this->getManager(), "Requested variable is managed by a different manager.");
20 z3::expr z3Expr = this->expressionAdapter.translateExpression(variable);
21 z3::expr z3ExprValuation = model.eval(z3Expr, true);
22 return this->expressionAdapter.translateExpression(z3ExprValuation).isTrue();
23#else
24 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
25#endif
26}
27
28int_fast64_t Z3SmtSolver::Z3ModelReference::getIntegerValue(storm::expressions::Variable const& variable) const {
29#ifdef STORM_HAVE_Z3
30 STORM_LOG_ASSERT(variable.getManager() == this->getManager(), "Requested variable is managed by a different manager.");
31 z3::expr z3Expr = this->expressionAdapter.translateExpression(variable);
32 z3::expr z3ExprValuation = model.eval(z3Expr, true);
33 return this->expressionAdapter.translateExpression(z3ExprValuation).evaluateAsInt();
34#else
35 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
36#endif
37}
38
39double Z3SmtSolver::Z3ModelReference::getRationalValue(storm::expressions::Variable const& variable) const {
40#ifdef STORM_HAVE_Z3
41 STORM_LOG_ASSERT(variable.getManager() == this->getManager(), "Requested variable is managed by a different manager.");
42 z3::expr z3Expr = this->expressionAdapter.translateExpression(variable);
43 z3::expr z3ExprValuation = model.eval(z3Expr, true);
44 return this->expressionAdapter.translateExpression(z3ExprValuation).evaluateAsDouble();
45#else
46 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
47#endif
48}
49
50std::string Z3SmtSolver::Z3ModelReference::toString() const {
51#ifdef STORM_HAVE_Z3
52 std::stringstream sstr;
53 sstr << model;
54 return sstr.str();
55#else
56 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
57#endif
58}
59
60Z3SmtSolver::Z3SmtSolver(storm::expressions::ExpressionManager& manager)
61 : SmtSolver(manager)
62#ifdef STORM_HAVE_Z3
63 ,
64 context(nullptr),
65 solver(nullptr),
66 expressionAdapter(nullptr),
67 lastCheckAssumptions(false),
68 lastResult(CheckResult::Unknown)
69#endif
70{
71#ifdef STORM_HAVE_Z3
72 z3::config config;
73 config.set("model", true);
74 context = std::unique_ptr<z3::context>(new z3::context(config));
75 solver = std::unique_ptr<z3::solver>(new z3::solver(*context));
76 expressionAdapter = std::unique_ptr<storm::adapters::Z3ExpressionAdapter>(new storm::adapters::Z3ExpressionAdapter(this->getManager(), *context));
77#endif
78}
79
81 // Intentionally left empty.
82}
83
85#ifdef STORM_HAVE_Z3
86 this->solver->push();
87#else
88 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
89#endif
90}
91
93#ifdef STORM_HAVE_Z3
94 this->solver->pop();
95#else
96 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
97#endif
98}
99
100void Z3SmtSolver::pop(uint_fast64_t n) {
101#ifdef STORM_HAVE_Z3
102 this->solver->pop(static_cast<unsigned int>(n));
103#else
104 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
105#endif
106}
107
109#ifdef STORM_HAVE_Z3
110 this->solver->reset();
111#else
112 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
113#endif
114}
115
117#ifdef STORM_HAVE_Z3
118 this->solver->add(expressionAdapter->translateExpression(assertion));
119#else
120 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
121#endif
122}
123
125#ifdef STORM_HAVE_Z3
126 lastCheckAssumptions = false;
127 switch (this->solver->check()) {
128 case z3::sat:
129 this->lastResult = SmtSolver::CheckResult::Sat;
130 break;
131 case z3::unsat:
132 this->lastResult = SmtSolver::CheckResult::Unsat;
133 break;
134 default:
135 this->lastResult = SmtSolver::CheckResult::Unknown;
136 break;
137 }
138 return this->lastResult;
139#else
140 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
141#endif
142}
143
144SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) {
145#ifdef STORM_HAVE_Z3
146 lastCheckAssumptions = true;
147 z3::expr_vector z3Assumptions(*this->context);
148
149 for (storm::expressions::Expression assumption : assumptions) {
150 z3Assumptions.push_back(this->expressionAdapter->translateExpression(assumption));
151 }
152
153 switch (this->solver->check(z3Assumptions)) {
154 case z3::sat:
155 this->lastResult = SmtSolver::CheckResult::Sat;
156 break;
157 case z3::unsat:
158 this->lastResult = SmtSolver::CheckResult::Unsat;
159 break;
160 default:
161 this->lastResult = SmtSolver::CheckResult::Unknown;
162 break;
163 }
164 return this->lastResult;
165#else
166 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
167#endif
168}
169
170#ifndef WINDOWS
171SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) {
172#ifdef STORM_HAVE_Z3
173 lastCheckAssumptions = true;
174 z3::expr_vector z3Assumptions(*this->context);
175
176 for (storm::expressions::Expression assumption : assumptions) {
177 z3Assumptions.push_back(this->expressionAdapter->translateExpression(assumption));
178 }
179
180 switch (this->solver->check(z3Assumptions)) {
181 case z3::sat:
182 this->lastResult = SmtSolver::CheckResult::Sat;
183 break;
184 case z3::unsat:
185 this->lastResult = SmtSolver::CheckResult::Unsat;
186 break;
187 default:
188 this->lastResult = SmtSolver::CheckResult::Unknown;
189 break;
190 }
191 return this->lastResult;
192#else
193 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
194#endif
195}
196#endif
198#ifdef STORM_HAVE_Z3
199 STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException,
200 "Unable to create model for formula that was not determined to be satisfiable.");
201 return this->convertZ3ModelToValuation(this->solver->get_model());
202#else
203 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
204#endif
205}
206
207std::shared_ptr<SmtSolver::ModelReference> Z3SmtSolver::getModel() {
208#ifdef STORM_HAVE_Z3
209 STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException,
210 "Unable to create model for formula that was not determined to be satisfiable.");
211 return std::shared_ptr<SmtSolver::ModelReference>(new Z3ModelReference(this->getManager(), this->solver->get_model(), *this->expressionAdapter));
212#else
213 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
214#endif
215}
216
217#ifdef STORM_HAVE_Z3
218storm::expressions::SimpleValuation Z3SmtSolver::convertZ3ModelToValuation(z3::model const& model) {
219 storm::expressions::SimpleValuation stormModel(this->getManager().getSharedPointer());
220
221 for (unsigned i = 0; i < model.num_consts(); ++i) {
222 z3::func_decl variableI = model.get_const_decl(i);
223 storm::expressions::Variable stormVariable = this->expressionAdapter->getVariable(variableI);
224 storm::expressions::Expression variableInterpretation = this->expressionAdapter->translateExpression(model.get_const_interp(variableI));
225
226 if (variableInterpretation.getType().isBooleanType()) {
227 stormModel.setBooleanValue(this->getManager().getVariable(variableI.name().str()), variableInterpretation.isTrue());
228 } else if (variableInterpretation.getType().isIntegerType()) {
229 stormModel.setIntegerValue(this->getManager().getVariable(variableI.name().str()), variableInterpretation.evaluateAsInt());
230 } else if (variableInterpretation.getType().isRationalType()) {
231 stormModel.setRationalValue(this->getManager().getVariable(variableI.name().str()), variableInterpretation.evaluateAsDouble());
232 } else {
233 STORM_LOG_ASSERT(false, "Variable interpretation in model is not of type bool, int or rational.");
234 }
235 }
236
237 return stormModel;
238}
239#endif
240
241std::vector<storm::expressions::SimpleValuation> Z3SmtSolver::allSat(std::vector<storm::expressions::Variable> const& important) {
242#ifdef STORM_HAVE_Z3
243 std::vector<storm::expressions::SimpleValuation> valuations;
244 this->allSat(important, static_cast<std::function<bool(storm::expressions::SimpleValuation&)>>(
245 [&valuations](storm::expressions::SimpleValuation const& valuation) -> bool {
246 valuations.push_back(valuation);
247 return true;
248 }));
249 return valuations;
250#else
251 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
252#endif
253}
254
255uint_fast64_t Z3SmtSolver::allSat(std::vector<storm::expressions::Variable> const& important,
256 std::function<bool(storm::expressions::SimpleValuation&)> const& callback) {
257#ifdef STORM_HAVE_Z3
258 for (storm::expressions::Variable const& variable : important) {
259 STORM_LOG_THROW(variable.hasBooleanType(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be boolean variables.");
260 }
261
262 uint_fast64_t numberOfModels = 0;
263 bool proceed = true;
264
265 // Save the current assertion stack, to be able to backtrack after the procedure.
266 this->push();
267
268 // Enumerate models as long as the conjunction is satisfiable and the callback has not aborted the enumeration.
269 while (proceed && this->check() == CheckResult::Sat) {
270 ++numberOfModels;
271 z3::model model = this->solver->get_model();
272
273 z3::expr modelExpr = this->context->bool_val(true);
274 storm::expressions::SimpleValuation valuation(this->getManager().getSharedPointer());
275
276 for (storm::expressions::Variable const& importantAtom : important) {
277 z3::expr z3ImportantAtom = this->expressionAdapter->translateExpression(importantAtom.getExpression());
278 z3::expr z3ImportantAtomValuation = model.eval(z3ImportantAtom, true);
279 modelExpr = modelExpr && (z3ImportantAtom == z3ImportantAtomValuation);
280 valuation.setBooleanValue(importantAtom, this->expressionAdapter->translateExpression(z3ImportantAtomValuation).isTrue());
281 }
282
283 // Check if we are required to proceed, and if so rule out the current model.
284 proceed = callback(valuation);
285 if (proceed) {
286 this->solver->add(!modelExpr);
287 }
288 }
289
290 // Restore the old assertion stack and return.
291 this->pop();
292 return numberOfModels;
293#else
294 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
295#endif
296}
297
298uint_fast64_t Z3SmtSolver::allSat(std::vector<storm::expressions::Variable> const& important, std::function<bool(SmtSolver::ModelReference&)> const& callback) {
299#ifdef STORM_HAVE_Z3
300 for (storm::expressions::Variable const& variable : important) {
301 STORM_LOG_THROW(variable.hasBooleanType(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be boolean variables.");
302 }
303
304 uint_fast64_t numberOfModels = 0;
305 bool proceed = true;
306
307 // Save the current assertion stack, to be able to backtrack after the procedure.
308 this->push();
309
310 // Enumerate models as long as the conjunction is satisfiable and the callback has not aborted the enumeration.
311 while (proceed && this->check() == CheckResult::Sat) {
312 ++numberOfModels;
313 z3::model model = this->solver->get_model();
314
315 z3::expr modelExpr = this->context->bool_val(true);
316 storm::expressions::SimpleValuation valuation(this->getManager().getSharedPointer());
317
318 for (storm::expressions::Variable const& importantAtom : important) {
319 z3::expr z3ImportantAtom = this->expressionAdapter->translateExpression(importantAtom.getExpression());
320 z3::expr z3ImportantAtomValuation = model.eval(z3ImportantAtom, true);
321 modelExpr = modelExpr && (z3ImportantAtom == z3ImportantAtomValuation);
322 }
323 Z3ModelReference modelRef(this->getManager(), model, *expressionAdapter);
324
325 // Check if we are required to proceed, and if so rule out the current model.
326 proceed = callback(modelRef);
327 if (proceed) {
328 this->solver->add(!modelExpr);
329 }
330 }
331
332 this->pop();
333 return numberOfModels;
334#else
335 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
336#endif
337}
338
339std::vector<storm::expressions::Expression> Z3SmtSolver::getUnsatAssumptions() {
340#ifdef STORM_HAVE_Z3
341 STORM_LOG_THROW(lastResult == SmtSolver::CheckResult::Unsat, storm::exceptions::InvalidStateException,
342 "Unable to generate unsatisfiable core of assumptions, because the last check did not determine the formulas to be unsatisfiable.");
343 STORM_LOG_THROW(lastCheckAssumptions, storm::exceptions::InvalidStateException,
344 "Unable to generate unsatisfiable core of assumptions, because the last check did not involve assumptions.");
345
346 z3::expr_vector z3UnsatAssumptions = this->solver->unsat_core();
347 std::vector<storm::expressions::Expression> unsatAssumptions;
348
349 for (unsigned int i = 0; i < z3UnsatAssumptions.size(); ++i) {
350 unsatAssumptions.push_back(this->expressionAdapter->translateExpression(z3UnsatAssumptions[i]));
351 }
352
353 return unsatAssumptions;
354#else
355 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
356#endif
357}
358
359bool Z3SmtSolver::setTimeout(uint_fast64_t milliseconds) {
360#ifdef STORM_HAVE_Z3
361 z3::params paramObject(*context);
362 paramObject.set(":timeout", static_cast<unsigned>(milliseconds));
363 solver->set(paramObject);
364 return true;
365#else
366 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
367#endif
368}
369
371#ifdef STORM_HAVE_Z3
372 z3::params paramObject(*context);
373 paramObject.set(":timeout", 0u);
374 solver->set(paramObject);
375 return true;
376#else
377 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
378#endif
379}
380
381std::string Z3SmtSolver::getSmtLibString() const {
382#ifdef STORM_HAVE_Z3
383 return solver->to_smt2();
384#else
385 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
386#endif
387}
388
389} // namespace solver
390} // namespace storm
int_fast64_t evaluateAsInt(Valuation const *valuation=nullptr) const
Evaluates the expression under the valuation of variables given by the valuation and returns the resu...
double evaluateAsDouble(Valuation const *valuation=nullptr) const
Evaluates the expression under the valuation of variables given by the valuation and returns the resu...
Type const & getType() const
Retrieves the type of the expression.
bool isTrue() const
Checks if the expression is equal to the boolean literal true.
This class is responsible for managing a set of typed variables and all expressions using these varia...
A simple implementation of the valuation interface.
virtual void setBooleanValue(Variable const &booleanVariable, bool value) override
Sets the value of the given boolean variable to the provided value.
bool isBooleanType() const
Checks whether this type is a boolean type.
Definition Type.cpp:178
bool isIntegerType() const
Checks whether this type is an integral type.
Definition Type.cpp:182
bool isRationalType() const
Checks whether this type is a rational type.
Definition Type.cpp:214
ExpressionManager const & getManager() const
Retrieves the manager responsible for this variable.
Definition Variable.cpp:54
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
storm::expressions::ExpressionManager const & getManager() const
Retrieves the expression manager associated with the solver.
Definition SmtSolver.cpp:79
CheckResult
possible check results
Definition SmtSolver.h:25
virtual void add(storm::expressions::Expression const &assertion) override
Adds an assertion to the solver's stack.
virtual bool unsetTimeout() override
If supported by the solver, this unsets a previous timeout.
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 storm::expressions::SimpleValuation getModelAsValuation() override
If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model tha...
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 std::string getSmtLibString() const override
If supported by the solver, this function returns the current assertions in the SMT-LIB format.
virtual std::vector< storm::expressions::SimpleValuation > allSat(std::vector< storm::expressions::Variable > const &important) override
Performs AllSat over the (provided) important atoms.
virtual void reset() override
Removes all assertions from the solver's stack.
virtual void push() override
Pushes a backtracking point on the solver's stack.
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 bool setTimeout(uint_fast64_t milliseconds) override
If supported by the solver, this will limit all subsequent satisfiability queries to the given number...
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.
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
SettingsManager const & manager()
Retrieves the settings manager.
LabParser.cpp.
Definition cli.cpp:18