Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
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
124void Z3SmtSolver::addNotCurrentModel(bool performSolverReset) {
125#ifdef STORM_HAVE_Z3
126 STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException,
127 "Unable to create model for formula that was not determined to be satisfiable.");
128
129 auto currentModel = this->solver->get_model();
130 z3::expr notThisModel = currentModel.ctx().bool_val(true);
131 for (auto const& variable : this->getManager().getVariables()) {
132 z3::expr var = this->expressionAdapter->translateExpression(variable);
133 auto value = currentModel.eval(var);
134 if (notThisModel.is_const()) {
135 notThisModel = var == value;
136 } else {
137 notThisModel = notThisModel && (var == value);
138 }
139 }
140 // https://stackoverflow.com/questions/78261966/z3-non-incremental-search-for-multiple-models-works-incremental-search-does-no
141 if (performSolverReset) {
142 auto const allAssertions = this->solver->assertions();
143 solver->reset();
144 for (auto const& assertion : allAssertions) {
145 solver->add(assertion);
146 }
147 }
148 this->solver->add(!notThisModel);
149#else
150 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
151#endif
152}
153
155#ifdef STORM_HAVE_Z3
156 lastCheckAssumptions = false;
157 switch (this->solver->check()) {
158 case z3::sat:
159 this->lastResult = SmtSolver::CheckResult::Sat;
160 break;
161 case z3::unsat:
162 this->lastResult = SmtSolver::CheckResult::Unsat;
163 break;
164 default:
165 this->lastResult = SmtSolver::CheckResult::Unknown;
166 break;
167 }
168 return this->lastResult;
169#else
170 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
171#endif
172}
173
174SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) {
175#ifdef STORM_HAVE_Z3
176 lastCheckAssumptions = true;
177 z3::expr_vector z3Assumptions(*this->context);
178
179 for (storm::expressions::Expression assumption : assumptions) {
180 z3Assumptions.push_back(this->expressionAdapter->translateExpression(assumption));
181 }
182
183 switch (this->solver->check(z3Assumptions)) {
184 case z3::sat:
185 this->lastResult = SmtSolver::CheckResult::Sat;
186 break;
187 case z3::unsat:
188 this->lastResult = SmtSolver::CheckResult::Unsat;
189 break;
190 default:
191 this->lastResult = SmtSolver::CheckResult::Unknown;
192 break;
193 }
194 return this->lastResult;
195#else
196 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
197#endif
198}
199
200SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) {
201#ifdef STORM_HAVE_Z3
202 lastCheckAssumptions = true;
203 z3::expr_vector z3Assumptions(*this->context);
204
205 for (storm::expressions::Expression assumption : assumptions) {
206 z3Assumptions.push_back(this->expressionAdapter->translateExpression(assumption));
207 }
208
209 switch (this->solver->check(z3Assumptions)) {
210 case z3::sat:
211 this->lastResult = SmtSolver::CheckResult::Sat;
212 break;
213 case z3::unsat:
214 this->lastResult = SmtSolver::CheckResult::Unsat;
215 break;
216 default:
217 this->lastResult = SmtSolver::CheckResult::Unknown;
218 break;
219 }
220 return this->lastResult;
221#else
222 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
223#endif
224}
225
227#ifdef STORM_HAVE_Z3
228 STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException,
229 "Unable to create model for formula that was not determined to be satisfiable.");
230 return this->convertZ3ModelToValuation(this->solver->get_model());
231#else
232 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
233#endif
234}
235
236std::shared_ptr<SmtSolver::ModelReference> Z3SmtSolver::getModel() {
237#ifdef STORM_HAVE_Z3
238 STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException,
239 "Unable to create model for formula that was not determined to be satisfiable.");
240 return std::shared_ptr<SmtSolver::ModelReference>(new Z3ModelReference(this->getManager(), this->solver->get_model(), *this->expressionAdapter));
241#else
242 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
243#endif
244}
245
246#ifdef STORM_HAVE_Z3
247storm::expressions::SimpleValuation Z3SmtSolver::convertZ3ModelToValuation(z3::model const& model) {
248 storm::expressions::SimpleValuation stormModel(this->getManager().getSharedPointer());
249
250 for (unsigned i = 0; i < model.num_consts(); ++i) {
251 z3::func_decl variableI = model.get_const_decl(i);
252 storm::expressions::Variable stormVariable = this->expressionAdapter->getVariable(variableI);
253 storm::expressions::Expression variableInterpretation = this->expressionAdapter->translateExpression(model.get_const_interp(variableI));
254
255 if (variableInterpretation.getType().isBooleanType()) {
256 stormModel.setBooleanValue(this->getManager().getVariable(variableI.name().str()), variableInterpretation.isTrue());
257 } else if (variableInterpretation.getType().isIntegerType()) {
258 stormModel.setIntegerValue(this->getManager().getVariable(variableI.name().str()), variableInterpretation.evaluateAsInt());
259 } else if (variableInterpretation.getType().isRationalType()) {
260 stormModel.setRationalValue(this->getManager().getVariable(variableI.name().str()), variableInterpretation.evaluateAsDouble());
261 } else {
262 STORM_LOG_ASSERT(false, "Variable interpretation in model is not of type bool, int or rational.");
263 }
264 }
265
266 return stormModel;
267}
268#endif
269
270std::vector<storm::expressions::SimpleValuation> Z3SmtSolver::allSat(std::vector<storm::expressions::Variable> const& important) {
271#ifdef STORM_HAVE_Z3
272 std::vector<storm::expressions::SimpleValuation> valuations;
273 this->allSat(important, static_cast<std::function<bool(storm::expressions::SimpleValuation&)>>(
274 [&valuations](storm::expressions::SimpleValuation const& valuation) -> bool {
275 valuations.push_back(valuation);
276 return true;
277 }));
278 return valuations;
279#else
280 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
281#endif
282}
283
284uint_fast64_t Z3SmtSolver::allSat(std::vector<storm::expressions::Variable> const& important,
285 std::function<bool(storm::expressions::SimpleValuation&)> const& callback) {
286#ifdef STORM_HAVE_Z3
287 for (storm::expressions::Variable const& variable : important) {
288 STORM_LOG_THROW(variable.hasBooleanType(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be boolean variables.");
289 }
290
291 uint_fast64_t numberOfModels = 0;
292 bool proceed = true;
293
294 // Save the current assertion stack, to be able to backtrack after the procedure.
295 this->push();
296
297 // Enumerate models as long as the conjunction is satisfiable and the callback has not aborted the enumeration.
298 while (proceed && this->check() == CheckResult::Sat) {
299 ++numberOfModels;
300 z3::model model = this->solver->get_model();
301
302 z3::expr modelExpr = this->context->bool_val(true);
303 storm::expressions::SimpleValuation valuation(this->getManager().getSharedPointer());
304
305 for (storm::expressions::Variable const& importantAtom : important) {
306 z3::expr z3ImportantAtom = this->expressionAdapter->translateExpression(importantAtom.getExpression());
307 z3::expr z3ImportantAtomValuation = model.eval(z3ImportantAtom, true);
308 modelExpr = modelExpr && (z3ImportantAtom == z3ImportantAtomValuation);
309 valuation.setBooleanValue(importantAtom, this->expressionAdapter->translateExpression(z3ImportantAtomValuation).isTrue());
310 }
311
312 // Check if we are required to proceed, and if so rule out the current model.
313 proceed = callback(valuation);
314 if (proceed) {
315 this->solver->add(!modelExpr);
316 }
317 }
318
319 // Restore the old assertion stack and return.
320 this->pop();
321 return numberOfModels;
322#else
323 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
324#endif
325}
326
327uint_fast64_t Z3SmtSolver::allSat(std::vector<storm::expressions::Variable> const& important, std::function<bool(SmtSolver::ModelReference&)> const& callback) {
328#ifdef STORM_HAVE_Z3
329 for (storm::expressions::Variable const& variable : important) {
330 STORM_LOG_THROW(variable.hasBooleanType(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be boolean variables.");
331 }
332
333 uint_fast64_t numberOfModels = 0;
334 bool proceed = true;
335
336 // Save the current assertion stack, to be able to backtrack after the procedure.
337 this->push();
338
339 // Enumerate models as long as the conjunction is satisfiable and the callback has not aborted the enumeration.
340 while (proceed && this->check() == CheckResult::Sat) {
341 ++numberOfModels;
342 z3::model model = this->solver->get_model();
343
344 z3::expr modelExpr = this->context->bool_val(true);
345 storm::expressions::SimpleValuation valuation(this->getManager().getSharedPointer());
346
347 for (storm::expressions::Variable const& importantAtom : important) {
348 z3::expr z3ImportantAtom = this->expressionAdapter->translateExpression(importantAtom.getExpression());
349 z3::expr z3ImportantAtomValuation = model.eval(z3ImportantAtom, true);
350 modelExpr = modelExpr && (z3ImportantAtom == z3ImportantAtomValuation);
351 }
352 Z3ModelReference modelRef(this->getManager(), model, *expressionAdapter);
353
354 // Check if we are required to proceed, and if so rule out the current model.
355 proceed = callback(modelRef);
356 if (proceed) {
357 this->solver->add(!modelExpr);
358 }
359 }
360
361 this->pop();
362 return numberOfModels;
363#else
364 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
365#endif
366}
367
368std::vector<storm::expressions::Expression> Z3SmtSolver::getUnsatAssumptions() {
369#ifdef STORM_HAVE_Z3
370 STORM_LOG_THROW(lastResult == SmtSolver::CheckResult::Unsat, storm::exceptions::InvalidStateException,
371 "Unable to generate unsatisfiable core of assumptions, because the last check did not determine the formulas to be unsatisfiable.");
372 STORM_LOG_THROW(lastCheckAssumptions, storm::exceptions::InvalidStateException,
373 "Unable to generate unsatisfiable core of assumptions, because the last check did not involve assumptions.");
374
375 z3::expr_vector z3UnsatAssumptions = this->solver->unsat_core();
376 std::vector<storm::expressions::Expression> unsatAssumptions;
377
378 for (unsigned int i = 0; i < z3UnsatAssumptions.size(); ++i) {
379 unsatAssumptions.push_back(this->expressionAdapter->translateExpression(z3UnsatAssumptions[i]));
380 }
381
382 return unsatAssumptions;
383#else
384 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
385#endif
386}
387
388bool Z3SmtSolver::setTimeout(uint_fast64_t milliseconds) {
389#ifdef STORM_HAVE_Z3
390 z3::params paramObject(*context);
391 paramObject.set(":timeout", static_cast<unsigned>(milliseconds));
392 solver->set(paramObject);
393 return true;
394#else
395 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
396#endif
397}
398
400#ifdef STORM_HAVE_Z3
401 z3::params paramObject(*context);
402 paramObject.set(":timeout", 0u);
403 solver->set(paramObject);
404 return true;
405#else
406 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
407#endif
408}
409
410std::string Z3SmtSolver::getSmtLibString() const {
411#ifdef STORM_HAVE_Z3
412 return solver->to_smt2();
413#else
414 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support.");
415#endif
416}
417
418} // namespace solver
419} // 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...
std::set< Variable > const & getVariables() const
Retrieves the set of all variables known to this manager.
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 addNotCurrentModel(bool performSolverReset=true) override
If supported by the solver, this function tells the SMT solver to produce a model different from the ...
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.