Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
Z3LpSolver.cpp
Go to the documentation of this file.
2
3#include <numeric>
4
7
8#include "storm/io/file.h"
13
19
20namespace storm {
21namespace solver {
22
23#ifdef STORM_HAVE_Z3_OPTIMIZE
24
25template<typename ValueType, bool RawMode>
26Z3LpSolver<ValueType, RawMode>::Z3LpSolver(std::string const& name, OptimizationDirection const& optDir)
27 : LpSolver<ValueType, RawMode>(optDir), isIncremental(false) {
28 z3::config config;
29 config.set("model", true);
30 context = std::unique_ptr<z3::context>(new z3::context(config));
31 solver = std::unique_ptr<z3::optimize>(new z3::optimize(*context));
32 expressionAdapter = std::unique_ptr<storm::adapters::Z3ExpressionAdapter>(new storm::adapters::Z3ExpressionAdapter(*this->manager, *context));
33}
34
35template<typename ValueType, bool RawMode>
36Z3LpSolver<ValueType, RawMode>::Z3LpSolver(std::string const& name) : Z3LpSolver(name, OptimizationDirection::Minimize) {
37 // Intentionally left empty.
38}
39
40template<typename ValueType, bool RawMode>
41Z3LpSolver<ValueType, RawMode>::Z3LpSolver(OptimizationDirection const& optDir) : Z3LpSolver("", optDir) {
42 // Intentionally left empty.
43}
44
45template<typename ValueType, bool RawMode>
46Z3LpSolver<ValueType, RawMode>::Z3LpSolver() : Z3LpSolver("", OptimizationDirection::Minimize) {
47 // Intentionally left empty.
48}
49
50template<typename ValueType, bool RawMode>
51Z3LpSolver<ValueType, RawMode>::~Z3LpSolver() {
52 // Intentionally left empty.
53}
54
55template<typename ValueType, bool RawMode>
56void Z3LpSolver<ValueType, RawMode>::update() const {
57 // Since the model changed, we erase the optimality flag.
58 lastCheckObjectiveValue.reset(nullptr);
59 lastCheckModel.reset(nullptr);
60 this->currentModelHasBeenOptimized = false;
61}
62
63template<typename ValueType, bool RawMode>
64typename Z3LpSolver<ValueType, RawMode>::Variable Z3LpSolver<ValueType, RawMode>::addVariable(std::string const& name, VariableType const& type,
65 std::optional<ValueType> const& lowerBound,
66 std::optional<ValueType> const& upperBound,
67 ValueType objectiveFunctionCoefficient) {
68 STORM_LOG_ASSERT(isIncremental || !this->manager->hasVariable(name), "Variable with name " << name << " already exists.");
69 storm::expressions::Variable newVariable = this->declareOrGetExpressionVariable(name, type);
70 if (type == VariableType::Binary) {
71 solver->add(expressionAdapter->translateExpression(newVariable.getExpression() >= this->manager->integer(0)));
72 solver->add(expressionAdapter->translateExpression(newVariable.getExpression() <= this->manager->integer(1)));
73 }
74 if (lowerBound) {
75 solver->add(expressionAdapter->translateExpression(newVariable.getExpression() >= this->manager->rational(*lowerBound)));
76 }
77 if (upperBound) {
78 solver->add(expressionAdapter->translateExpression(newVariable.getExpression() <= this->manager->rational(*upperBound)));
79 }
80 if (!storm::utility::isZero(objectiveFunctionCoefficient)) {
81 optimizationSummands.push_back(this->manager->rational(objectiveFunctionCoefficient) * newVariable);
82 }
83
84 if constexpr (RawMode) {
85 rawIndexToVariableMap.push_back(newVariable);
86 return rawIndexToVariableMap.size() - 1;
87 } else {
88 return newVariable;
89 }
90}
91
92template<typename ValueType, bool RawMode>
93void Z3LpSolver<ValueType, RawMode>::addConstraint(std::string const& name, Constraint const& constraint) {
94 if constexpr (RawMode) {
95 // Generate expression from raw constraint
96 STORM_LOG_ASSERT(constraint.lhsVariableIndices.size() == constraint.lhsCoefficients.size(), "number of variables and coefficients do not match.");
97 std::vector<storm::expressions::Expression> lhsSummands;
98 lhsSummands.reserve(constraint.lhsVariableIndices.size());
99 auto varIt = constraint.lhsVariableIndices.cbegin();
100 auto varItEnd = constraint.lhsVariableIndices.cend();
101 auto coefIt = constraint.lhsCoefficients.cbegin();
102 for (; varIt != varItEnd; ++varIt, ++coefIt) {
103 lhsSummands.push_back(rawIndexToVariableMap[*varIt] * this->manager->rational(*coefIt));
104 }
105 if (lhsSummands.empty()) {
106 lhsSummands.push_back(this->manager->rational(storm::utility::zero<ValueType>()));
107 }
109 storm::expressions::sum(lhsSummands), this->manager->rational(constraint.rhs), constraint.relationType);
110 solver->add(expressionAdapter->translateExpression(constraintExpr));
111 } else {
112 STORM_LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException, "Illegal constraint is not a relational expression.");
113 STORM_LOG_THROW(constraint.getOperator() != storm::expressions::OperatorType::NotEqual, storm::exceptions::InvalidArgumentException,
114 "Illegal constraint uses inequality operator.");
115 solver->add(expressionAdapter->translateExpression(constraint));
116 }
117}
118
119template<typename ValueType, bool RawMode>
120void Z3LpSolver<ValueType, RawMode>::addIndicatorConstraint(std::string const& name, Variable indicatorVariable, bool indicatorValue,
121 Constraint const& constraint) {
122 if constexpr (RawMode) {
123 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Indicator constraints not implemented in RawMode");
124 } else {
125 // binary variables are encoded as integer variables with domain {0,1}.
126 STORM_LOG_THROW(indicatorVariable.hasIntegerType(), storm::exceptions::InvalidArgumentException,
127 "Variable " << indicatorVariable.getName() << " is not binary.");
128 STORM_LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException, "Illegal constraint is not a relational expression.");
129 STORM_LOG_THROW(constraint.getOperator() != storm::expressions::OperatorType::NotEqual, storm::exceptions::InvalidArgumentException,
130 "Illegal constraint uses inequality operator.");
131
132 storm::expressions::Expression invertedIndicatorVal =
133 this->getConstant(indicatorValue ? storm::utility::zero<ValueType>() : storm::utility::one<ValueType>());
134 auto indicatorConstraint = (indicatorVariable.getExpression() == invertedIndicatorVal) || constraint;
135 solver->add(expressionAdapter->translateExpression(indicatorConstraint));
136 }
137}
138
139template<typename ValueType, bool RawMode>
140void Z3LpSolver<ValueType, RawMode>::optimize() const {
141 // First incorporate all recent changes.
142 this->update();
143
144 // Invoke push() as we want to be able to erase the current optimization function after checking
145 solver->push();
146
147 storm::expressions::Expression optimizationFunction = this->manager->integer(0);
148 // Solve the optimization problem depending on the optimization direction
149 if (!optimizationSummands.empty()) {
150 optimizationFunction = storm::expressions::sum(optimizationSummands);
151 }
152 z3::optimize::handle optFuncHandle = this->getOptimizationDirection() == OptimizationDirection::Minimize
153 ? solver->minimize(expressionAdapter->translateExpression(optimizationFunction))
154 : solver->maximize(expressionAdapter->translateExpression(optimizationFunction));
155
156 z3::check_result chkRes = solver->check();
157 STORM_LOG_THROW(chkRes != z3::unknown, storm::exceptions::InvalidStateException, "Unable to solve LP problem with Z3: Check result is unknown.");
158
159 // We need to store the resulting information at this point. Otherwise, the information would be lost after calling pop() ...
160
161 // Check feasibility
162 lastCheckInfeasible = (chkRes == z3::unsat);
163 if (lastCheckInfeasible) {
164 lastCheckUnbounded = false;
165 } else {
166 // Get objective result
167 lastCheckObjectiveValue = std::make_unique<z3::expr>(solver->upper(optFuncHandle));
168 // Check boundedness
169 STORM_LOG_ASSERT(lastCheckObjectiveValue->is_app(), "Failed to convert Z3 expression. Encountered unknown expression type.");
170 lastCheckUnbounded = (lastCheckObjectiveValue->decl().decl_kind() != Z3_OP_ANUM);
171 if (lastCheckUnbounded) {
172 lastCheckObjectiveValue.reset(nullptr);
173 } else {
174 // Assert that the upper approximation equals the lower one
175 STORM_LOG_ASSERT(std::string(Z3_get_numeral_string(*context, *lastCheckObjectiveValue)) ==
176 std::string(Z3_get_numeral_string(*context, solver->lower(optFuncHandle))),
177 "Lower and Upper Approximation of z3LPSolver result do not match.");
178 lastCheckModel = std::make_unique<z3::model>(solver->get_model());
179 }
180 }
181
182 solver->pop(); // removes current optimization function
183 this->currentModelHasBeenOptimized = true;
184}
185
186template<typename ValueType, bool RawMode>
187bool Z3LpSolver<ValueType, RawMode>::isInfeasible() const {
188 STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException,
189 "Illegal call to Z3LpSolver<ValueType, RawMode>::isInfeasible: model has not been optimized.");
190 return lastCheckInfeasible;
191}
192
193template<typename ValueType, bool RawMode>
194bool Z3LpSolver<ValueType, RawMode>::isUnbounded() const {
195 STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException,
196 "Illegal call to Z3LpSolver<ValueType, RawMode>::isUnbounded: model has not been optimized.");
197 return lastCheckUnbounded;
198}
199
200template<typename ValueType, bool RawMode>
201bool Z3LpSolver<ValueType, RawMode>::isOptimal() const {
202 STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException,
203 "Illegal call to Z3LpSolver<ValueType, RawMode>::isOptimal: model has not been optimized.");
204 return !lastCheckInfeasible && !lastCheckUnbounded;
205}
206
207template<typename ValueType, bool RawMode>
208storm::expressions::Expression Z3LpSolver<ValueType, RawMode>::getValue(Variable const& variable) const {
209 if (!this->isOptimal()) {
210 STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from infeasible model.");
211 STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from unbounded model.");
212 STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from unoptimized model.");
213 }
214 STORM_LOG_ASSERT(lastCheckModel, "Model has not been stored.");
215
216 if constexpr (RawMode) {
217 STORM_LOG_ASSERT(variable < rawIndexToVariableMap.size(), "Requested variable out of range.");
218 z3::expr z3Var = this->expressionAdapter->translateExpression(rawIndexToVariableMap[variable]);
219 return this->expressionAdapter->translateExpression(lastCheckModel->eval(z3Var, true));
220 } else {
221 STORM_LOG_ASSERT(variable.getManager() == this->getManager(), "Requested variable is managed by a different manager.");
222 z3::expr z3Var = this->expressionAdapter->translateExpression(variable);
223 return this->expressionAdapter->translateExpression(lastCheckModel->eval(z3Var, true));
224 }
225}
226
227template<typename ValueType, bool RawMode>
228ValueType Z3LpSolver<ValueType, RawMode>::getContinuousValue(Variable const& variable) const {
229 storm::expressions::Expression value = getValue(variable);
231 return storm::utility::convertNumber<ValueType>(value.getBaseExpression().asIntegerLiteralExpression().getValue());
232 }
233 STORM_LOG_THROW(value.getBaseExpression().isRationalLiteralExpression(), storm::exceptions::ExpressionEvaluationException,
234 "Expected a rational literal while obtaining the value of a continuous variable. Got " << value << "instead.");
235 return storm::utility::convertNumber<ValueType>(value.getBaseExpression().asRationalLiteralExpression().getValue());
236}
237
238template<typename ValueType, bool RawMode>
239int_fast64_t Z3LpSolver<ValueType, RawMode>::getIntegerValue(Variable const& variable) const {
240 storm::expressions::Expression value = getValue(variable);
241 STORM_LOG_THROW(value.getBaseExpression().isIntegerLiteralExpression(), storm::exceptions::ExpressionEvaluationException,
242 "Expected an integer literal while obtaining the value of an integer variable. Got " << value << "instead.");
244}
245
246template<typename ValueType, bool RawMode>
247bool Z3LpSolver<ValueType, RawMode>::getBinaryValue(Variable const& variable) const {
248 storm::expressions::Expression value = getValue(variable);
249 // Binary variables are in fact represented as integer variables!
250 STORM_LOG_THROW(value.getBaseExpression().isIntegerLiteralExpression(), storm::exceptions::ExpressionEvaluationException,
251 "Expected an integer literal while obtaining the value of a binary variable. Got " << value << "instead.");
252 int_fast64_t val = value.getBaseExpression().asIntegerLiteralExpression().getValue();
253 STORM_LOG_THROW((val == 0 || val == 1), storm::exceptions::ExpressionEvaluationException,
254 "Tried to get a binary value for a variable that is neither 0 nor 1.");
255 return val == 1;
256}
257
258template<typename ValueType, bool RawMode>
259ValueType Z3LpSolver<ValueType, RawMode>::getObjectiveValue() const {
260 if (!this->isOptimal()) {
261 STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from infeasible model.");
262 STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from unbounded model.");
263 STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from unoptimized model.");
264 }
265 STORM_LOG_ASSERT(lastCheckObjectiveValue, "Objective value has not been stored.");
266
267 storm::expressions::Expression result = this->expressionAdapter->translateExpression(*lastCheckObjectiveValue);
269 return storm::utility::convertNumber<ValueType>(result.getBaseExpression().asIntegerLiteralExpression().getValue());
270 }
271 STORM_LOG_THROW(result.getBaseExpression().isRationalLiteralExpression(), storm::exceptions::ExpressionEvaluationException,
272 "Expected a rational literal while obtaining the objective result. Got " << result << "instead.");
273 return storm::utility::convertNumber<ValueType>(result.getBaseExpression().asRationalLiteralExpression().getValue());
274}
275
276template<typename ValueType, bool RawMode>
277void Z3LpSolver<ValueType, RawMode>::writeModelToFile(std::string const& filename) const {
278 std::ofstream stream;
279 storm::io::openFile(filename, stream);
280 stream << Z3_optimize_to_string(*context, *solver);
281 storm::io::closeFile(stream);
282}
283
284template<typename ValueType, bool RawMode>
285void Z3LpSolver<ValueType, RawMode>::push() {
286 STORM_LOG_THROW(!RawMode, storm::exceptions::NotImplementedException, "Incremental solving is not supported in Raw mode.");
287 incrementaOptimizationSummandIndicators.push_back(optimizationSummands.size());
288 solver->push();
289}
290
291template<typename ValueType, bool RawMode>
292void Z3LpSolver<ValueType, RawMode>::pop() {
293 STORM_LOG_THROW(!RawMode, storm::exceptions::NotImplementedException, "Incremental solving is not supported in Raw mode.");
294 STORM_LOG_ASSERT(!incrementaOptimizationSummandIndicators.empty(), "Tried to pop() without push()ing first.");
295 solver->pop();
296 // Delete summands of the optimization function that have been added since the last call to push()
297 optimizationSummands.resize(incrementaOptimizationSummandIndicators.back());
298 incrementaOptimizationSummandIndicators.pop_back();
299 isIncremental = true;
300}
301
302template<typename ValueType, bool RawMode>
303void Z3LpSolver<ValueType, RawMode>::setMaximalMILPGap(ValueType const&, bool) {
304 // Since the solver is always exact, setting a gap has no effect.
305 // Intentionally left empty.
306}
307
308template<typename ValueType, bool RawMode>
309ValueType Z3LpSolver<ValueType, RawMode>::getMILPGap(bool relative) const {
310 // Since the solver is precise, the milp gap is always zero.
311 return storm::utility::zero<ValueType>();
312}
313#else
314template<typename ValueType, bool RawMode>
316 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. "
317 "Yet, a method was called that requires this support.";
318}
319
320template<typename ValueType, bool RawMode>
322 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. "
323 "Yet, a method was called that requires this support.";
324}
325
326template<typename ValueType, bool RawMode>
328 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. "
329 "Yet, a method was called that requires this support.";
330}
331
332template<typename ValueType, bool RawMode>
334 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. "
335 "Yet, a method was called that requires this support.";
336}
337
338template<typename ValueType, bool RawMode>
340
341template<typename ValueType, bool RawMode>
343 std::optional<ValueType> const&, std::optional<ValueType> const&,
344 ValueType) {
345 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. "
346 "Yet, a method was called that requires this support.";
347}
348
349template<typename ValueType, bool RawMode>
351 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. "
352 "Yet, a method was called that requires this support.";
353}
354
355template<typename ValueType, bool RawMode>
357 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. "
358 "Yet, a method was called that requires this support.";
359}
360
361template<typename ValueType, bool RawMode>
363 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. "
364 "Yet, a method was called that requires this support.";
365}
366
367template<typename ValueType, bool RawMode>
369 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. "
370 "Yet, a method was called that requires this support.";
371}
372
373template<typename ValueType, bool RawMode>
375 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. "
376 "Yet, a method was called that requires this support.";
377}
378
379template<typename ValueType, bool RawMode>
381 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. "
382 "Yet, a method was called that requires this support.";
383}
384
385template<typename ValueType, bool RawMode>
387 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. "
388 "Yet, a method was called that requires this support.";
389}
390
391template<typename ValueType, bool RawMode>
393 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. "
394 "Yet, a method was called that requires this support.";
395}
396
397template<typename ValueType, bool RawMode>
399 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. "
400 "Yet, a method was called that requires this support.";
401}
402
403template<typename ValueType, bool RawMode>
405 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. "
406 "Yet, a method was called that requires this support.";
407}
408
409template<typename ValueType, bool RawMode>
411 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. "
412 "Yet, a method was called that requires this support.";
413}
414
415template<typename ValueType, bool RawMode>
417 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. "
418 "Yet, a method was called that requires this support.";
419}
420
421template<typename ValueType, bool RawMode>
422void Z3LpSolver<ValueType, RawMode>::writeModelToFile(std::string const& filename) const {
423 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. "
424 "Yet, a method was called that requires this support.";
425}
426
427template<typename ValueType, bool RawMode>
429 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. "
430 "Yet, a method was called that requires this support.";
431}
432
433template<typename ValueType, bool RawMode>
435 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. "
436 "Yet, a method was called that requires this support.";
437}
438
439template<typename ValueType, bool RawMode>
441 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. "
442 "Yet, a method was called that requires this support.";
443}
444
445template<typename ValueType, bool RawMode>
446ValueType Z3LpSolver<ValueType, RawMode>::getMILPGap(bool relative) const {
447 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. "
448 "Yet, a method was called that requires this support.";
449}
450#endif
451
452template class Z3LpSolver<double, false>;
454template class Z3LpSolver<double, true>;
456} // namespace solver
457} // namespace storm
IntegerLiteralExpression const & asIntegerLiteralExpression() const
RationalLiteralExpression const & asRationalLiteralExpression() const
virtual bool isRationalLiteralExpression() const
virtual bool isIntegerLiteralExpression() const
BaseExpression const & getBaseExpression() const
Retrieves the base expression underlying this expression object.
int_fast64_t getValue() const
Retrieves the value of the integer literal.
storm::RationalNumber getValue() const
Retrieves the value of the double literal.
storm::expressions::Expression getExpression() const
Retrieves an expression that represents the variable.
Definition Variable.cpp:34
A class that implements the LpSolver interface using Z3.
Definition Z3LpSolver.h:24
typename LpSolver< ValueType, RawMode >::Variable Variable
Definition Z3LpSolver.h:27
typename LpSolver< ValueType, RawMode >::Constraint Constraint
Definition Z3LpSolver.h:29
Z3LpSolver()
Constructs a solver without a name.
typename LpSolver< ValueType, RawMode >::VariableType VariableType
Definition Z3LpSolver.h:26
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
SFTBDDChecker::ValueType ValueType
Expression makeBinaryRelationExpression(Expression const &first, Expression const &second, RelationType const &reltype)
Expression sum(std::vector< storm::expressions::Expression > const &expressions)
void closeFile(std::ofstream &stream)
Close the given file after writing.
Definition file.h:47
void openFile(std::string const &filepath, std::ofstream &filestream, bool append=false, bool silent=false)
Open the given file for writing.
Definition file.h:18
SettingsManager const & manager()
Retrieves the settings manager.
bool isZero(ValueType const &a)
Definition constants.cpp:41
ValueType one()
Definition constants.cpp:21
LabParser.cpp.
Definition cli.cpp:18