From ed465f75bd658e7d94f04dc7d77fefb905cda579 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 10 Feb 2017 20:33:39 +0100 Subject: [PATCH] added Z3LPSolver --- src/storm/solver/Z3LPSolver.cpp | 306 +++++++++++++++++++++++++++++ src/storm/solver/Z3LPSolver.h | 134 +++++++++++++ src/test/solver/Z3LpSolverTest.cpp | 249 +++++++++++++++++++++++ 3 files changed, 689 insertions(+) create mode 100644 src/storm/solver/Z3LPSolver.cpp create mode 100644 src/storm/solver/Z3LPSolver.h create mode 100644 src/test/solver/Z3LpSolverTest.cpp diff --git a/src/storm/solver/Z3LPSolver.cpp b/src/storm/solver/Z3LPSolver.cpp new file mode 100644 index 000000000..6bc2da2c1 --- /dev/null +++ b/src/storm/solver/Z3LPSolver.cpp @@ -0,0 +1,306 @@ +#include "storm/solver/Z3LpSolver.h" + +#include + +#include "storm/storage/expressions/LinearCoefficientVisitor.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/DebugSettings.h" + +#include "storm/utility/macros.h" +#include "storm/utility/constants.h" +#include "storm/storage/expressions/Expression.h" +#include "storm/storage/expressions/ExpressionManager.h" + +#include "storm/exceptions/InvalidStateException.h" +#include "storm/exceptions/InvalidAccessException.h" +#include "storm/exceptions/InvalidArgumentException.h" +#include "storm/exceptions/NotImplementedException.h" +#include "storm/exceptions/ExpressionEvaluationException.h" + + +namespace storm { + namespace solver { + +#ifdef STORM_HAVE_Z3 + Z3LpSolver::Z3LpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver(optDir), z3CheckResult(z3::unknown), z3Handle(0) { + STORM_LOG_WARN_COND(name != "", "Z3 does not support names for solvers"); + z3::config config; + config.set("model", true); + context = std::unique_ptr(new z3::context(config)); + solver = std::unique_ptr(new z3::optimize(*context)); + expressionAdapter = std::unique_ptr(new storm::adapters::Z3ExpressionAdapter(*this->manager, *context)); + optimizationFunction = this->getManager().rational(storm::utility::zero()); + } + + Z3LpSolver::Z3LpSolver(std::string const& name) : Z3LpSolver(name, OptimizationDirection::Minimize) { + // Intentionally left empty. + } + + Z3LpSolver::Z3LpSolver(OptimizationDirection const& optDir) : Z3LpSolver("", optDir) { + // Intentionally left empty. + } + + Z3LpSolver::Z3LpSolver() : Z3LpSolver("", OptimizationDirection::Minimize) { + // Intentionally left empty. + } + + Z3LpSolver::~Z3LpSolver() { + // Intentionally left empty. + } + + void Z3LpSolver::update() const { + // Since the model changed, we erase the optimality flag and reset the current model. + this->z3Model.reset(nullptr); + this->currentModelHasBeenOptimized = false; + } + + storm::expressions::Variable Z3LpSolver::addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getRationalType()); + solver->add(expressionAdapter->translateExpression((newVariable.getExpression() >= this->manager->rational(lowerBound)) && (newVariable.getExpression() <= this->manager->rational(upperBound)))); + optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; + return newVariable; + } + + storm::expressions::Variable Z3LpSolver::addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getRationalType()); + solver->add(expressionAdapter->translateExpression(newVariable.getExpression() >= this->manager->rational(lowerBound))); + optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; + return newVariable; + } + + storm::expressions::Variable Z3LpSolver::addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getRationalType()); + solver->add(expressionAdapter->translateExpression(newVariable.getExpression() <= this->manager->rational(upperBound))); + optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; + return newVariable; + } + + storm::expressions::Variable Z3LpSolver::addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getRationalType()); + optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; + return newVariable; + } + + storm::expressions::Variable Z3LpSolver::addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType()); + solver->add(expressionAdapter->translateExpression((newVariable.getExpression() >= this->manager->rational(lowerBound)) && (newVariable.getExpression() <= this->manager->rational(upperBound)))); + optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; + return newVariable; + } + + storm::expressions::Variable Z3LpSolver::addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType()); + solver->add(expressionAdapter->translateExpression(newVariable.getExpression() >= this->manager->rational(lowerBound))); + optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; + return newVariable; + } + + storm::expressions::Variable Z3LpSolver::addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType()); + solver->add(expressionAdapter->translateExpression(newVariable.getExpression() <= this->manager->rational(upperBound))); + optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; + return newVariable; + } + + storm::expressions::Variable Z3LpSolver::addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType()); + optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; + return newVariable; + } + + storm::expressions::Variable Z3LpSolver::addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getBooleanType()); + optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; + return newVariable; + } + + void Z3LpSolver::addConstraint(std::string const& name, storm::expressions::Expression const& constraint) { + STORM_LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException, "Illegal constraint is not a relational expression."); + STORM_LOG_THROW(constraint.getOperator() != storm::expressions::OperatorType::NotEqual, storm::exceptions::InvalidArgumentException, "Illegal constraint uses inequality operator."); + STORM_LOG_WARN_COND(name != "", "Z3 does not support names for constraints"); + solver->add(expressionAdapter->translateExpression(constraint)); + } + + void Z3LpSolver::optimize() const { + // First incorporate all recent changes. + this->update(); + + // Invoke push() as we want to be able to erase the current optimization function after checking + solver->push(); + + // Solve the optimization problem depending on the optimization direction + z3Handle = this->getOptimizationDirection() == OptimizationDirection::Minimize ? solver->minimize(expressionAdapter->translateExpression(optimizationFunction)) : solver->maximize(expressionAdapter->translateExpression(optimizationFunction)); + z3CheckResult = solver->check(); + STORM_LOG_THROW(z3CheckResult != z3::unknown, storm::exceptions::InvalidStateException, "Unable to solve LP problem with Z3: Check result is unknown."); + + this->currentModelHasBeenOptimized = true; + solver->pop(); // removes current optimization function + + } + + bool Z3LpSolver::isInfeasible() const { + STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException, "Illegal call to Z3LpSolver::isInfeasible: model has not been optimized."); + return z3CheckResult == z3::unsat; + } + + bool Z3LpSolver::isUnbounded() const { + STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException, "Illegal call to Z3LpSolver::isInfeasible: model has not been optimized."); + z3::expr expr = solver->upper(z3Handle); + STORM_LOG_THROW(expr.is_app(), storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered unknown expression type."); + return expr.decl().decl_kind() != Z3_OP_ANUM; + } + + bool Z3LpSolver::isOptimal() const { + return !this->isInfeasible() && !this->isUnbounded(); + } + + + storm::expressions::Expression Z3LpSolver::getValue(storm::expressions::Variable const& variable) const { + STORM_LOG_ASSERT(variable.getManager() == this->getManager(), "Requested variable is managed by a different manager."); + if (!this->isOptimal()) { + STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from infeasible model."); + STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from unbounded model."); + STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from unoptimized model."); + } + if(!this->z3Model) { + z3Model = std::unique_ptr(new z3::model(solver->get_model())); + } + z3::expr z3Var = this->expressionAdapter->translateExpression(variable); + return this->expressionAdapter->translateExpression(z3Model->eval(z3Var, true)); + } + + double Z3LpSolver::getContinuousValue(storm::expressions::Variable const& variable) const { + return getValue(variable).evaluateAsDouble(); + } + + int_fast64_t Z3LpSolver::getIntegerValue(storm::expressions::Variable const& variable) const { + return getValue(variable).evaluateAsInt(); + } + + bool Z3LpSolver::getBinaryValue(storm::expressions::Variable const& variable) const { + return getValue(variable).evaluateAsBool(); + } + + double Z3LpSolver::getObjectiveValue() const { + if (!this->isOptimal()) { + STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from infeasible model."); + STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from unbounded model."); + STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from unoptimized model."); + } + z3::expr expr = solver->upper(z3Handle); + STORM_LOG_THROW(expr == solver->lower(z3Handle), storm::exceptions::InvalidAccessException, "Lower and Upper Approximation of z3LPSolver result do not match."); // TODO: make this an assertion + return this->expressionAdapter->translateExpression(expr).evaluateAsDouble(); + } + + void Z3LpSolver::writeModelToFile(std::string const& filename) const { + STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::NotImplementedException, "Exporting LP Problems to a file is not implemented for z3."); + } + +#else + Z3LpSolver::Z3LpSolver(std::string const&, OptimizationDirection const&) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + + Z3LpSolver::Z3LpSolver(std::string const&) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + + Z3LpSolver::Z3LpSolver(OptimizationDirection const&) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + + Z3LpSolver::Z3LpSolver() { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + + Z3LpSolver::~Z3LpSolver() { + + } + + storm::expressions::Variable Z3LpSolver::addBoundedContinuousVariable(std::string const&, double, double, double) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + + storm::expressions::Variable Z3LpSolver::addLowerBoundedContinuousVariable(std::string const&, double, double ) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; } + + storm::expressions::Variable Z3LpSolver::addUpperBoundedContinuousVariable(std::string const&, double, double ) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + + storm::expressions::Variable Z3LpSolver::addUnboundedContinuousVariable(std::string const&, double ) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + + storm::expressions::Variable Z3LpSolver::addBoundedIntegerVariable(std::string const&, double, double, double) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + + storm::expressions::Variable Z3LpSolver::addLowerBoundedIntegerVariable(std::string const&, double, double) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + + storm::expressions::Variable Z3LpSolver::addUpperBoundedIntegerVariable(std::string const&, double, double) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + + storm::expressions::Variable Z3LpSolver::addUnboundedIntegerVariable(std::string const&, double) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + + storm::expressions::Variable Z3LpSolver::addBinaryVariable(std::string const&, double) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + + void Z3LpSolver::update() const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + + void Z3LpSolver::addConstraint(std::string const&, storm::expressions::Expression const&) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + + void Z3LpSolver::optimize() const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + + bool Z3LpSolver::isInfeasible() const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + + bool Z3LpSolver::isUnbounded() const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + + bool Z3LpSolver::isOptimal() const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + + double Z3LpSolver::getContinuousValue(storm::expressions::Variable const&) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + + int_fast64_t Z3LpSolver::getIntegerValue(storm::expressions::Variable const&) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + + bool Z3LpSolver::getBinaryValue(storm::expressions::Variable const&) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + + double Z3LpSolver::getObjectiveValue() const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + + void Z3LpSolver::writeModelToFile(std::string const&) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + + void Z3LpSolver::toggleOutput(bool) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support. Please choose a version of support with Z3 support."; + } + +#endif + } +} diff --git a/src/storm/solver/Z3LPSolver.h b/src/storm/solver/Z3LPSolver.h new file mode 100644 index 000000000..d6a0f1e0f --- /dev/null +++ b/src/storm/solver/Z3LPSolver.h @@ -0,0 +1,134 @@ +#ifndef STORM_SOLVER_Z3LPSOLVER +#define STORM_SOLVER_Z3LPSOLVER + +#include +#include "storm/solver/LpSolver.h" +// To detect whether the usage of Z3 is possible, this include is neccessary. +#include "storm-config.h" +#include "storm/storage/expressions/Expressions.h" +#include "storm/adapters/Z3ExpressionAdapter.h" + + +#ifdef STORM_HAVE_Z3 + #include "z3++.h" + #include "z3.h" +#endif + + +namespace storm { + namespace solver { + + /*! + * A class that implements the LpSolver interface using Z3. + */ + class Z3LpSolver : public LpSolver { + public: + /*! + * Constructs a solver with the given name and optimization direction + * + * @param name The name of the LP problem. + * @param optDir A value indicating whether the value of the objective function is to be minimized or + * maximized. + */ + Z3LpSolver(std::string const& name, OptimizationDirection const& optDir); + + /*! + * Constructs a solver with the given name. By default the objective function is assumed to be minimized, + * but this may be altered later using a call to setOptimizationDirection. + * + * @param name The name of the LP problem. + */ + Z3LpSolver(std::string const& name); + + /*! + * Constructs a solver without a name and the given optimization direction. + * + * @param optDir A value indicating whether the value of the objective function is to be minimized or + * maximized. + */ + Z3LpSolver(OptimizationDirection const& optDir); + + /*! + * Constructs a solver without a name. By default the objective function is assumed to be minimized, + * but this may be altered later using a call to setModelSense. + */ + Z3LpSolver(); + + /*! + * Destructs a solver by freeing the pointers to Z3's structures. + */ + virtual ~Z3LpSolver(); + + // Methods to add continuous variables. + virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override; + + // Methods to add integer variables. + virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override; + + // Methods to add binary variables. + virtual storm::expressions::Variable addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override; + + // Methods to incorporate recent changes. + virtual void update() const override; + + // Methods to add constraints + virtual void addConstraint(std::string const& name, storm::expressions::Expression const& constraint) override; + + // Methods to optimize and retrieve optimality status. + virtual void optimize() const override; + virtual bool isInfeasible() const override; + virtual bool isUnbounded() const override; + virtual bool isOptimal() const override; + + // Methods to retrieve values of variables and the objective function in the optimal solutions. + virtual double getContinuousValue(storm::expressions::Variable const& name) const override; + virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& name) const override; + virtual bool getBinaryValue(storm::expressions::Variable const& name) const override; + virtual double getObjectiveValue() const override; + + // Methods to print the LP problem to a file. + virtual void writeModelToFile(std::string const& filename) const override; + + private: + virtual storm::expressions::Expression getValue(storm::expressions::Variable const& name) const; + + +#ifdef STORM_HAVE_Z3 + + // The context used by the solver. + std::unique_ptr context; + + // The actual solver object. + std::unique_ptr solver; + + // The result of the most recent check + mutable z3::check_result z3CheckResult; + + // The handle for the most recent optimization call + mutable z3::optimize::handle z3Handle; + + // The model for the most recent optimization call + mutable std::unique_ptr z3Model; + + // An expression adapter that is used for translating the expression into Z3's format. + std::unique_ptr expressionAdapter; + + // The function that is to be optimized + storm::expressions::Expression optimizationFunction; + +#endif + + // The name of the solver + std::string name; + }; + + } +} + +#endif /* STORM_SOLVER_Z3LPSOLVER */ \ No newline at end of file diff --git a/src/test/solver/Z3LpSolverTest.cpp b/src/test/solver/Z3LpSolverTest.cpp new file mode 100644 index 000000000..960359b36 --- /dev/null +++ b/src/test/solver/Z3LpSolverTest.cpp @@ -0,0 +1,249 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#ifdef STORM_HAVE_Z3 +#include "storm/storage/expressions/Variable.h" +#include "storm/solver/Z3LpSolver.h" +#include "storm/exceptions/InvalidStateException.h" +#include "storm/exceptions/InvalidAccessException.h" +#include "storm/settings/SettingsManager.h" + +#include "storm/settings/modules/GeneralSettings.h" + +#include "storm/storage/expressions/Expressions.h" +#include "storm/solver/OptimizationDirection.h" + +#include + +TEST(Z3LpSolver, LPOptimizeMax) { + storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBoundedContinuousVariable("x", 0, 1, -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1)); + ASSERT_NO_THROW(solver.update()); + + ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); + ASSERT_NO_THROW(solver.update()); + + ASSERT_NO_THROW(solver.optimize()); + ASSERT_TRUE(solver.isOptimal()); + ASSERT_FALSE(solver.isUnbounded()); + ASSERT_FALSE(solver.isInfeasible()); + double xValue = 0; + ASSERT_NO_THROW(xValue = solver.getContinuousValue(x)); + ASSERT_LT(std::fabs(xValue - 1), storm::settings::getModule().getPrecision()); + double yValue = 0; + ASSERT_NO_THROW(yValue = solver.getContinuousValue(y)); + ASSERT_LT(std::fabs(yValue - 6.5), storm::settings::getModule().getPrecision()); + double zValue = 0; + ASSERT_NO_THROW(zValue = solver.getContinuousValue(z)); + ASSERT_LT(std::fabs(zValue - 2.75), storm::settings::getModule().getPrecision()); + double objectiveValue = 0; + ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue()); + ASSERT_LT(std::fabs(objectiveValue - 14.75), storm::settings::getModule().getPrecision()); +} + +TEST(Z3LpSolver, LPOptimizeMin) { + storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Minimize); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBoundedContinuousVariable("x", 0, 1, -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addBoundedContinuousVariable("z", 1, 5.7, -1)); + ASSERT_NO_THROW(solver.update()); + + ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x <= solver.getConstant(5))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); + ASSERT_NO_THROW(solver.update()); + + ASSERT_NO_THROW(solver.optimize()); + ASSERT_TRUE(solver.isOptimal()); + ASSERT_FALSE(solver.isUnbounded()); + ASSERT_FALSE(solver.isInfeasible()); + double xValue = 0; + ASSERT_NO_THROW(xValue = solver.getContinuousValue(x)); + ASSERT_LT(std::fabs(xValue - 1), storm::settings::getModule().getPrecision()); + double yValue = 0; + ASSERT_NO_THROW(yValue = solver.getContinuousValue(y)); + ASSERT_LT(std::fabs(yValue - 0), storm::settings::getModule().getPrecision()); + double zValue = 0; + ASSERT_NO_THROW(zValue = solver.getContinuousValue(z)); + ASSERT_LT(std::fabs(zValue - 5.7), storm::settings::getModule().getPrecision()); + double objectiveValue = 0; + ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue()); + ASSERT_LT(std::fabs(objectiveValue - (-6.7)), storm::settings::getModule().getPrecision()); +} + +TEST(Z3LpSolver, MILPOptimizeMax) { + storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBinaryVariable("x", -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedIntegerVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1)); + ASSERT_NO_THROW(solver.update()); + + ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); + ASSERT_NO_THROW(solver.update()); + + ASSERT_NO_THROW(solver.optimize()); + ASSERT_TRUE(solver.isOptimal()); + ASSERT_FALSE(solver.isUnbounded()); + ASSERT_FALSE(solver.isInfeasible()); + bool xValue = false; + ASSERT_NO_THROW(xValue = solver.getBinaryValue(x)); + ASSERT_EQ(true, xValue); + int_fast64_t yValue = 0; + ASSERT_NO_THROW(yValue = solver.getIntegerValue(y)); + ASSERT_EQ(6, yValue); + double zValue = 0; + ASSERT_NO_THROW(zValue = solver.getContinuousValue(z)); + ASSERT_LT(std::fabs(zValue - 3), storm::settings::getModule().getPrecision()); + double objectiveValue = 0; + ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue()); + ASSERT_LT(std::fabs(objectiveValue - 14), storm::settings::getModule().getPrecision()); +} + +TEST(Z3LpSolver, MILPOptimizeMin) { + storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Minimize); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBinaryVariable("x", -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedIntegerVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addBoundedContinuousVariable("z", 0, 5, -1)); + ASSERT_NO_THROW(solver.update()); + + ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x <= solver.getConstant(5))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); + ASSERT_NO_THROW(solver.update()); + + ASSERT_NO_THROW(solver.optimize()); + ASSERT_TRUE(solver.isOptimal()); + ASSERT_FALSE(solver.isUnbounded()); + ASSERT_FALSE(solver.isInfeasible()); + bool xValue = false; + ASSERT_NO_THROW(xValue = solver.getBinaryValue(x)); + ASSERT_EQ(true, xValue); + int_fast64_t yValue = 0; + ASSERT_NO_THROW(yValue = solver.getIntegerValue(y)); + ASSERT_EQ(0, yValue); + double zValue = 0; + ASSERT_NO_THROW(zValue = solver.getContinuousValue(z)); + ASSERT_LT(std::fabs(zValue - 5), storm::settings::getModule().getPrecision()); + double objectiveValue = 0; + ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue()); + ASSERT_LT(std::fabs(objectiveValue - (-6)), storm::settings::getModule().getPrecision()); +} + +TEST(Z3LpSolver, LPInfeasible) { + storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBoundedContinuousVariable("x", 0, 1, -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1)); + ASSERT_NO_THROW(solver.update()); + + ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); + ASSERT_NO_THROW(solver.addConstraint("", y > solver.getConstant(7))); + ASSERT_NO_THROW(solver.update()); + + ASSERT_NO_THROW(solver.optimize()); + ASSERT_FALSE(solver.isOptimal()); + ASSERT_FALSE(solver.isUnbounded()); + ASSERT_TRUE(solver.isInfeasible()); + ASSERT_THROW(solver.getContinuousValue(x), storm::exceptions::InvalidAccessException); + ASSERT_THROW(solver.getContinuousValue(y), storm::exceptions::InvalidAccessException); + ASSERT_THROW(solver.getContinuousValue(z), storm::exceptions::InvalidAccessException); + ASSERT_THROW(solver.getObjectiveValue(), storm::exceptions::InvalidAccessException); +} + +TEST(Z3LpSolver, MILPInfeasible) { + storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBinaryVariable("x", -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1)); + ASSERT_NO_THROW(solver.update()); + + ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); + ASSERT_NO_THROW(solver.addConstraint("", y > solver.getConstant(7))); + ASSERT_NO_THROW(solver.update()); + + ASSERT_NO_THROW(solver.optimize()); + ASSERT_FALSE(solver.isOptimal()); + ASSERT_FALSE(solver.isUnbounded()); + ASSERT_TRUE(solver.isInfeasible()); + ASSERT_THROW(solver.getBinaryValue(x), storm::exceptions::InvalidAccessException); + ASSERT_THROW(solver.getIntegerValue(y), storm::exceptions::InvalidAccessException); + ASSERT_THROW(solver.getContinuousValue(z), storm::exceptions::InvalidAccessException); + ASSERT_THROW(solver.getObjectiveValue(), storm::exceptions::InvalidAccessException); +} + +TEST(Z3LpSolver, LPUnbounded) { + storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBoundedContinuousVariable("x", 0, 1, -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1)); + ASSERT_NO_THROW(solver.update()); + + ASSERT_NO_THROW(solver.addConstraint("", x + y - z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); + ASSERT_NO_THROW(solver.update()); + + ASSERT_NO_THROW(solver.optimize()); + ASSERT_FALSE(solver.isOptimal()); + ASSERT_TRUE(solver.isUnbounded()); + ASSERT_FALSE(solver.isInfeasible()); + ASSERT_THROW(solver.getContinuousValue(x), storm::exceptions::InvalidAccessException); + ASSERT_THROW(solver.getContinuousValue(y), storm::exceptions::InvalidAccessException); + ASSERT_THROW(solver.getContinuousValue(z), storm::exceptions::InvalidAccessException); + ASSERT_THROW(solver.getObjectiveValue(), storm::exceptions::InvalidAccessException); +} + +TEST(Z3LpSolver, MILPUnbounded) { + storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize); + storm::expressions::Variable x; + storm::expressions::Variable y; + storm::expressions::Variable z; + ASSERT_NO_THROW(x = solver.addBinaryVariable("x", -1)); + ASSERT_NO_THROW(y = solver.addLowerBoundedContinuousVariable("y", 0, 2)); + ASSERT_NO_THROW(z = solver.addLowerBoundedContinuousVariable("z", 0, 1)); + ASSERT_NO_THROW(solver.update()); + + ASSERT_NO_THROW(solver.addConstraint("", x + y - z <= solver.getConstant(12))); + ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); + ASSERT_NO_THROW(solver.update()); + + ASSERT_NO_THROW(solver.optimize()); + ASSERT_FALSE(solver.isOptimal()); + ASSERT_TRUE(solver.isUnbounded()); + ASSERT_FALSE(solver.isInfeasible()); + ASSERT_THROW(solver.getBinaryValue(x), storm::exceptions::InvalidAccessException); + ASSERT_THROW(solver.getIntegerValue(y), storm::exceptions::InvalidAccessException); + ASSERT_THROW(solver.getContinuousValue(z), storm::exceptions::InvalidAccessException); + ASSERT_THROW(solver.getObjectiveValue(), storm::exceptions::InvalidAccessException); +} +#endif