23#ifdef STORM_HAVE_Z3_OPTIMIZE
25template<
typename ValueType,
bool RawMode>
27 : LpSolver<
ValueType, RawMode>(optDir), isIncremental(false) {
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));
35template<
typename ValueType,
bool RawMode>
40template<
typename ValueType,
bool RawMode>
41Z3LpSolver<ValueType, RawMode>::Z3LpSolver(OptimizationDirection
const& optDir) : Z3LpSolver(
"", optDir) {
45template<
typename ValueType,
bool RawMode>
50template<
typename ValueType,
bool RawMode>
51Z3LpSolver<ValueType, RawMode>::~Z3LpSolver() {
55template<
typename ValueType,
bool RawMode>
56void Z3LpSolver<ValueType, RawMode>::update()
const {
58 lastCheckObjectiveValue.reset(
nullptr);
59 lastCheckModel.reset(
nullptr);
60 this->currentModelHasBeenOptimized =
false;
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.");
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)));
75 solver->add(expressionAdapter->translateExpression(newVariable.
getExpression() >= this->manager->rational(*lowerBound)));
78 solver->add(expressionAdapter->translateExpression(newVariable.
getExpression() <= this->manager->rational(*upperBound)));
81 optimizationSummands.push_back(this->
manager->rational(objectiveFunctionCoefficient) * newVariable);
84 if constexpr (RawMode) {
85 rawIndexToVariableMap.push_back(newVariable);
86 return rawIndexToVariableMap.size() - 1;
92template<
typename ValueType,
bool RawMode>
93void Z3LpSolver<ValueType, RawMode>::addConstraint(std::string
const& name, Constraint
const& constraint) {
94 if constexpr (RawMode) {
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));
105 if (lhsSummands.empty()) {
106 lhsSummands.push_back(this->
manager->rational(storm::utility::zero<ValueType>()));
110 solver->add(expressionAdapter->translateExpression(constraintExpr));
112 STORM_LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException,
"Illegal constraint is not a relational expression.");
114 "Illegal constraint uses inequality operator.");
115 solver->add(expressionAdapter->translateExpression(constraint));
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");
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.");
130 "Illegal constraint uses inequality operator.");
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));
139template<
typename ValueType,
bool RawMode>
140void Z3LpSolver<ValueType, RawMode>::optimize()
const {
149 if (!optimizationSummands.empty()) {
152 z3::optimize::handle optFuncHandle = this->getOptimizationDirection() == OptimizationDirection::Minimize
153 ? solver->minimize(expressionAdapter->translateExpression(optimizationFunction))
154 : solver->maximize(expressionAdapter->translateExpression(optimizationFunction));
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.");
162 lastCheckInfeasible = (chkRes == z3::unsat);
163 if (lastCheckInfeasible) {
164 lastCheckUnbounded =
false;
167 lastCheckObjectiveValue = std::make_unique<z3::expr>(solver->upper(optFuncHandle));
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);
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());
183 this->currentModelHasBeenOptimized =
true;
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;
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;
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;
207template<
typename ValueType,
bool RawMode>
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.");
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));
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));
227template<
typename ValueType,
bool RawMode>
228ValueType Z3LpSolver<ValueType, RawMode>::getContinuousValue(Variable
const& variable)
const {
234 "Expected a rational literal while obtaining the value of a continuous variable. Got " << value <<
"instead.");
238template<
typename ValueType,
bool RawMode>
239int_fast64_t Z3LpSolver<ValueType, RawMode>::getIntegerValue(Variable
const& variable)
const {
242 "Expected an integer literal while obtaining the value of an integer variable. Got " << value <<
"instead.");
246template<
typename ValueType,
bool RawMode>
247bool Z3LpSolver<ValueType, RawMode>::getBinaryValue(Variable
const& variable)
const {
251 "Expected an integer literal while obtaining the value of a binary variable. Got " << value <<
"instead.");
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.");
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.");
265 STORM_LOG_ASSERT(lastCheckObjectiveValue,
"Objective value has not been stored.");
272 "Expected a rational literal while obtaining the objective result. Got " << result <<
"instead.");
276template<
typename ValueType,
bool RawMode>
277void Z3LpSolver<ValueType, RawMode>::writeModelToFile(std::string
const& filename)
const {
278 std::ofstream stream;
280 stream << Z3_optimize_to_string(*context, *solver);
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());
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.");
297 optimizationSummands.resize(incrementaOptimizationSummandIndicators.back());
298 incrementaOptimizationSummandIndicators.pop_back();
299 isIncremental =
true;
302template<
typename ValueType,
bool RawMode>
303void Z3LpSolver<ValueType, RawMode>::setMaximalMILPGap(ValueType
const&,
bool) {
308template<
typename ValueType,
bool RawMode>
309ValueType Z3LpSolver<ValueType, RawMode>::getMILPGap(
bool relative)
const {
311 return storm::utility::zero<ValueType>();
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.";
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.";
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.";
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.";
338template<
typename ValueType,
bool RawMode>
341template<
typename ValueType,
bool RawMode>
343 std::optional<ValueType>
const&, std::optional<ValueType>
const&,
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.";
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.";
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.";
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.";
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.";
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.";
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.";
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.";
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.";
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.";
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.";
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.";
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.";
421template<
typename ValueType,
bool RawMode>
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.";
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.";
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.";
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.";
445template<
typename ValueType,
bool RawMode>
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.";
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.
A class that implements the LpSolver interface using Z3.
typename LpSolver< ValueType, RawMode >::Variable Variable
typename LpSolver< ValueType, RawMode >::Constraint Constraint
Z3LpSolver()
Constructs a solver without a name.
typename LpSolver< ValueType, RawMode >::VariableType VariableType
#define STORM_LOG_ASSERT(cond, message)
#define STORM_LOG_THROW(cond, exception, message)
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.
void openFile(std::string const &filepath, std::ofstream &filestream, bool append=false, bool silent=false)
Open the given file for writing.
SettingsManager const & manager()
Retrieves the settings manager.
bool isZero(ValueType const &a)