From b5e68b99147a72d23a58df54bcc2d5bc1913a254 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 15 Feb 2017 10:41:32 +0100 Subject: [PATCH] fixes for z3LP solver and nativePolytopes --- resources/3rdparty/CMakeLists.txt | 21 ++- src/storm/adapters/Z3ExpressionAdapter.cpp | 5 +- src/storm/solver/Z3LPSolver.cpp | 163 ++++++++++-------- src/storm/solver/Z3LPSolver.h | 25 ++- src/storm/storage/geometry/NativePolytope.cpp | 49 +++--- src/storm/storage/geometry/NativePolytope.h | 26 +-- src/storm/storage/geometry/Polytope.cpp | 10 +- src/storm/storage/geometry/Polytope.h | 4 +- .../HyperplaneEnumeration.cpp | 4 + .../SubsetEnumerator.cpp | 2 + storm-config.h.in | 3 + 11 files changed, 189 insertions(+), 123 deletions(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 8c013f86f..64e8ef28a 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -133,7 +133,26 @@ find_package(Z3 QUIET) set(STORM_HAVE_Z3 ${Z3_FOUND}) if(Z3_FOUND) - message (STATUS "storm - Linking with Z3.") + # Check whether the version of z3 supports optimization + if (Z3_EXEC) + execute_process (COMMAND ${Z3_EXEC} -version + OUTPUT_VARIABLE z3_version_output + ERROR_QUIET + OUTPUT_STRIP_TRAILING_WHITESPACE) + if (z3_version_output MATCHES "([0-9]*\\.[0-9]*\\.[0-9]*)") + set(Z3_VERSION "${CMAKE_MATCH_1}") + if(NOT "${Z3_VERSION}" VERSION_LESS "4.4.1") + set(STORM_HAVE_Z3_OPTIMIZE ON) + endif() + endif() + endif() + + if(STORM_HAVE_Z3_OPTIMIZE) + message (STATUS "storm - Linking with Z3. (Z3 version supports optimization)") + else() + message (STATUS "storm - Linking with Z3. (Z3 version does not support optimization)") + endif() + add_imported_library(z3 SHARED ${Z3_LIBRARIES} ${Z3_INCLUDE_DIRS}) list(APPEND STORM_DEP_TARGETS z3_SHARED) endif(Z3_FOUND) diff --git a/src/storm/adapters/Z3ExpressionAdapter.cpp b/src/storm/adapters/Z3ExpressionAdapter.cpp index fa8e9721e..17740476d 100644 --- a/src/storm/adapters/Z3ExpressionAdapter.cpp +++ b/src/storm/adapters/Z3ExpressionAdapter.cpp @@ -3,6 +3,7 @@ #include "storm/storage/expressions/Expressions.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/utility/macros.h" +#include "storm/utility/constants.h" #include "storm/exceptions/ExpressionEvaluationException.h" #include "storm/exceptions/InvalidTypeException.h" #include "storm/exceptions/NotImplementedException.h" @@ -122,9 +123,9 @@ namespace storm { long long num; long long den; if (Z3_get_numeral_rational_int64(expr.ctx(), expr, &num, &den)) { - return manager.rational(static_cast(num) / static_cast(den)); + return manager.rational(storm::utility::convertNumber(num) / storm::utility::convertNumber(den)); } else { - STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Expression is constant real and value does not fit into a fraction with 64-bit integer numerator and denominator."); + manager.rational(storm::utility::convertNumber(std::string(Z3_get_numeral_string(expr.ctx(), expr)))); } } case Z3_OP_UNINTERPRETED: diff --git a/src/storm/solver/Z3LPSolver.cpp b/src/storm/solver/Z3LPSolver.cpp index 8d4b637b1..552f11424 100644 --- a/src/storm/solver/Z3LPSolver.cpp +++ b/src/storm/solver/Z3LPSolver.cpp @@ -22,7 +22,7 @@ namespace storm { namespace solver { -#ifdef STORM_HAVE_Z3 +#ifdef STORM_HAVE_Z3_OPTIMIZE Z3LpSolver::Z3LpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver(optDir) { STORM_LOG_WARN_COND(name != "", "Z3 does not support names for solvers"); z3::config config; @@ -190,16 +190,26 @@ namespace storm { } double Z3LpSolver::getContinuousValue(storm::expressions::Variable const& variable) const { - return getValue(variable).evaluateAsDouble(); + storm::expressions::Expression value = getValue(variable); + if(value.getBaseExpression().isIntegerLiteralExpression()) { + return value.getBaseExpression().asIntegerLiteralExpression().getValue(); + } + STORM_LOG_THROW(value.getBaseExpression().isRationalLiteralExpression(), storm::exceptions::ExpressionEvaluationException, "Expected a rational literal while obtaining the value of a continuous variable. Got " << value << "instead."); + return value.getBaseExpression().asRationalLiteralExpression().getValueAsDouble(); } int_fast64_t Z3LpSolver::getIntegerValue(storm::expressions::Variable const& variable) const { - return getValue(variable).evaluateAsInt(); + storm::expressions::Expression value = getValue(variable); + STORM_LOG_THROW(value.getBaseExpression().isIntegerLiteralExpression(), storm::exceptions::ExpressionEvaluationException, "Expected an integer literal while obtaining the value of an integer variable. Got " << value << "instead."); + return value.getBaseExpression().asIntegerLiteralExpression().getValue(); } bool Z3LpSolver::getBinaryValue(storm::expressions::Variable const& variable) const { - int_fast64_t val = getValue(variable).evaluateAsInt(); - STORM_LOG_THROW((val==0 || val==1), storm::exceptions::InvalidAccessException, "Tried to get a binary value for a variable that is neither 0 nor 1."); + storm::expressions::Expression value = getValue(variable); + // Binary variables are in fact represented as integer variables! + STORM_LOG_THROW(value.getBaseExpression().isIntegerLiteralExpression(), storm::exceptions::ExpressionEvaluationException, "Expected an integer literal while obtaining the value of a binary variable. Got " << value << "instead."); + int_fast64_t val = value.getBaseExpression().asIntegerLiteralExpression().getValue(); + STORM_LOG_THROW((val==0 || val==1), storm::exceptions::ExpressionEvaluationException, "Tried to get a binary value for a variable that is neither 0 nor 1."); return val==1; } @@ -211,7 +221,12 @@ namespace storm { } STORM_LOG_ASSERT(lastCheckObjectiveValue, "Objective value has not been stored."); - return this->expressionAdapter->translateExpression(*lastCheckObjectiveValue).evaluateAsDouble(); + storm::expressions::Expression result = this->expressionAdapter->translateExpression(*lastCheckObjectiveValue); + if(result.getBaseExpression().isIntegerLiteralExpression()) { + return result.getBaseExpression().asIntegerLiteralExpression().getValue(); + } + STORM_LOG_THROW(result.getBaseExpression().isRationalLiteralExpression(), storm::exceptions::ExpressionEvaluationException, "Expected a rational literal while obtaining the objective result. Got " << result << "instead."); + return result.getBaseExpression().asRationalLiteralExpression().getValueAsDouble(); } void Z3LpSolver::writeModelToFile(std::string const& filename) const { @@ -280,7 +295,12 @@ namespace storm { } storm::RationalNumber Z3LpSolver::getExactContinuousValue(storm::expressions::Variable const& variable) const { - return getValue(variable).evaluateAsDouble(); + storm::expressions::Expression value = getValue(variable); + if(value.getBaseExpression().isIntegerLiteralExpression()) { + return storm::utility::convertNumber(value.getBaseExpression().asIntegerLiteralExpression().getValue()); + } + STORM_LOG_ASSERT(value.getBaseExpression().isRationalLiteralExpression(), "Expected a rational literal while obtaining the value of a continuous variable. Got " << value << "instead."); + return value.getBaseExpression().asRationalLiteralExpression().getValue(); } storm::RationalNumber Z3LpSolver::getExactObjectiveValue() const { @@ -291,152 +311,157 @@ namespace storm { } STORM_LOG_ASSERT(lastCheckObjectiveValue, "Objective value has not been stored."); - return this->expressionAdapter->translateExpression(*lastCheckObjectiveValue).evaluateAsDouble(); + storm::expressions::Expression result = this->expressionAdapter->translateExpression(*lastCheckObjectiveValue); + if(result.getBaseExpression().isIntegerLiteralExpression()) { + return storm::utility::convertNumber(result.getBaseExpression().asIntegerLiteralExpression().getValue()); + } + STORM_LOG_THROW(result.getBaseExpression().isRationalLiteralExpression(), storm::exceptions::ExpressionEvaluationException, "Expected a rational literal while obtaining the objective result. Got " << result << "instead."); + return result.getBaseExpression().asRationalLiteralExpression().getValue(); } #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."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this 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."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this 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."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this 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."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } - - Z3LpSolver::~Z3LpSolver() { - + + 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."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this 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."; } - + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this 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."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this 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."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this 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."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this 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."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this 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."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this 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."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this 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."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this 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."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this 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."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this 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."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this 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."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this 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."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this 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."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this 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."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this 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."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this 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."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this 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."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this 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."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } storm::expressions::Variable Z3LpSolver::addBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } storm::expressions::Variable Z3LpSolver::addLowerBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& objectiveFunctionCoefficient) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } storm::expressions::Variable Z3LpSolver::addUpperBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } storm::expressions::Variable Z3LpSolver::addUnboundedContinuousVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } storm::expressions::Variable Z3LpSolver::addBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } storm::expressions::Variable Z3LpSolver::addLowerBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& objectiveFunctionCoefficient) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } storm::expressions::Variable Z3LpSolver::addUpperBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } storm::expressions::Variable Z3LpSolver::addUnboundedIntegerVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } storm::expressions::Variable Z3LpSolver::addBinaryVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } storm::RationalNumber Z3LpSolver::getExactContinuousValue(storm::expressions::Variable const& variable) const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } storm::RationalNumber Z3LpSolver::getExactObjectiveValue() const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Z3. Yet, a method was called that requires this support."; + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } diff --git a/src/storm/solver/Z3LPSolver.h b/src/storm/solver/Z3LPSolver.h index 36b4a9c54..d3a04598f 100644 --- a/src/storm/solver/Z3LPSolver.h +++ b/src/storm/solver/Z3LPSolver.h @@ -9,7 +9,7 @@ #include "storm/adapters/Z3ExpressionAdapter.h" -#ifdef STORM_HAVE_Z3 +#ifdef STORM_HAVE_Z3_OPTIMIZE #include "z3++.h" #include "z3.h" #endif @@ -96,25 +96,24 @@ namespace storm { virtual void writeModelToFile(std::string const& filename) const override; // Methods for exact solving - virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addBinaryVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient = 0) override; + storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0); + storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0); + storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0); + storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient = 0); + storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0); + storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0); + storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0); + storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient = 0); + storm::expressions::Variable addBinaryVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient = 0); storm::RationalNumber getExactContinuousValue(storm::expressions::Variable const& variable) const; storm::RationalNumber getExactObjectiveValue() const; - private: - virtual storm::expressions::Expression getValue(storm::expressions::Variable const& name) const; + virtual storm::expressions::Expression getValue(storm::expressions::Variable const& variable) const; -#ifdef STORM_HAVE_Z3 +#ifdef STORM_HAVE_Z3_OPTIMIZE // The context used by the solver. std::unique_ptr context; diff --git a/src/storm/storage/geometry/NativePolytope.cpp b/src/storm/storage/geometry/NativePolytope.cpp index b6e05b19e..b148b5454 100644 --- a/src/storm/storage/geometry/NativePolytope.cpp +++ b/src/storm/storage/geometry/NativePolytope.cpp @@ -4,9 +4,10 @@ #include "storm/utility/macros.h" #include "storm/utility/solver.h" #include "storm/solver/Z3LPSolver.h" +#include "storm/solver/SmtSolver.h" #include "storm/storage/geometry/nativepolytopeconversion/QuickHull.h" #include "storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.h" - +#include "storm/storage/expressions/ExpressionManager.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/UnexpectedException.h" @@ -26,9 +27,9 @@ namespace storm { A = EigenMatrix(maxRow, maxCol); b = EigenVector(maxRow); for ( uint_fast64_t row = 0; row < maxRow; ++row ){ - assert(halfspaces[row].normal().rows() == maxCol); + assert(halfspaces[row].normalVector().size() == maxCol); b(row) = halfspaces[row].offset(); - A(row) = storm::adapters::EigenAdapter::toEigenVector(halfspaces[row].normal()); + A.row(row) = storm::adapters::EigenAdapter::toEigenVector(halfspaces[row].normalVector()); } emptyStatus = EmptyStatus::Unknown; } @@ -42,7 +43,7 @@ namespace storm { std::vector eigenPoints; eigenPoints.reserve(points.size()); for(auto const& p : points){ - eigenPoints.emplace_back(storm::adapters::EigenAdapter::toEigenVector(p)); + eigenPoints.emplace_back(storm::adapters::EigenAdapter::toEigenVector(p)); } storm::storage::geometry::QuickHull qh; @@ -92,11 +93,11 @@ namespace storm { template std::vector::Point> NativePolytope::getVertices() const { - std::vector> eigenVertices = getEigenVertices(); + std::vector eigenVertices = getEigenVertices(); std::vector result; result.reserve(eigenVertices.size()); for(auto const& p : eigenVertices) { - result.push_back(storm::adapters::EigenAdapter::toStdVector(p)); + result.push_back(storm::adapters::EigenAdapter::toStdVector(p)); } return result; } @@ -107,30 +108,31 @@ namespace storm { result.reserve(A.rows()); for(uint_fast64_t row=0; row < A.rows(); ++row){ - result.emplace_back(storm::adapters::EigenAdapter::toStdVector(A.row(row)), b.row(row)); + result.emplace_back(storm::adapters::EigenAdapter::toStdVector(EigenVector(A.row(row))), b(row)); } + return result; } template bool NativePolytope::isEmpty() const { - if(emptyStatus == emptyStatus::Unknown) { + if(emptyStatus == EmptyStatus::Unknown) { storm::expressions::ExpressionManager manager; std::unique_ptr solver = storm::utility::solver::SmtSolverFactory().create(manager); storm::expressions::Expression constraints = getConstraints(manager, declareVariables(manager, "x")); solver->add(constraints); switch(solver->check()) { case storm::solver::SmtSolver::CheckResult::Sat: - emptyStatus = emptyStatus::Nonempty; + emptyStatus = EmptyStatus::Nonempty; break; case storm::solver::SmtSolver::CheckResult::Unsat: - emptyStatus = emptyStatus::Empty; + emptyStatus = EmptyStatus::Empty; break; default: STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected result of SMT solver during emptyness-check of Polytope."); break; } } - return emptyStatus == emptyStatus::Empty; + return emptyStatus == EmptyStatus::Empty; } template @@ -140,7 +142,7 @@ namespace storm { template bool NativePolytope::contains(Point const& point) const{ - EigenVector x = storm::adapters::EigenAdapter::toEigenVector(point); + EigenVector x = storm::adapters::EigenAdapter::toEigenVector(point); for(uint_fast64_t row=0; row < A.rows(); ++row){ if((A.row(row) * x)(0) > b(row)){ return false; @@ -181,18 +183,17 @@ namespace storm { EigenVector resultb(resultA.rows()); resultb << b, nativeRhs.b; - return std::make_shared>(std::move(resultA), std::move(resultb)); + return std::make_shared>(EmptyStatus::Unknown, std::move(resultA), std::move(resultb)); } template std::shared_ptr> NativePolytope::intersection(Halfspace const& halfspace) const{ EigenMatrix resultA(A.rows() + 1, A.cols()); - resultA << A, - storm::adapters::EigenAdapter::toEigenVector(halfspace.normal()); + resultA << A, storm::adapters::EigenAdapter::toEigenVector(halfspace.normalVector()); EigenVector resultb(resultA.rows()); resultb << b, halfspace.offset(); - return std::make_shared>(std::move(resultA), std::move(resultb)); + return std::make_shared>(EmptyStatus::Unknown, std::move(resultA), std::move(resultb)); } template @@ -202,7 +203,7 @@ namespace storm { return std::make_shared>(dynamic_cast const&>(*rhs)); } else if (rhs->isEmpty()) { return std::make_shared>(*this); - } else if (this->isUniversal() || rhs->isUniversal) { + } else if (this->isUniversal() || rhs->isUniversal()) { return std::make_shared>(std::vector>()); } @@ -270,7 +271,7 @@ namespace storm { } EigenVector eigenVector = storm::adapters::EigenAdapter::toEigenVector(vector); - Eigen::FullPivLU luMatrix( eigenMatrix ); + StormEigen::FullPivLU luMatrix( eigenMatrix ); STORM_LOG_THROW(luMatrix.isInvertible(), storm::exceptions::NotImplementedException, "Affine Transformation of native polytope only implemented if the transformation matrix is invertable"); EigenMatrix newA = A * luMatrix.inverse(); EigenVector newb = b + (newA * eigenVector); @@ -283,7 +284,7 @@ namespace storm { std::vector variables; variables.reserve(A.rows()); for (uint_fast64_t i = 0; i < A.rows(); ++i) { - variables.push_back(solver.addUnboundedContinuousVariable("x" + std::to_string(i), direction(i))); + variables.push_back(solver.addUnboundedContinuousVariable("x" + std::to_string(i), direction[i])); } solver.addConstraint("", getConstraints(solver.getManager(), variables)); solver.update(); @@ -292,7 +293,7 @@ namespace storm { auto result = std::make_pair(Point(), true); result.first.reserve(variables.size()); for (auto const& var : variables) { - result.first.push_back(solver.getContinuousValue(var)); + result.first.push_back(storm::utility::convertNumber((solver.getExactContinuousValue(var)))); } return result; } else { @@ -316,7 +317,7 @@ namespace storm { if (solver.isOptimal()) { auto result = std::make_pair(EigenVector(variables.size()), true); for (uint_fast64_t i = 0; i < variables.size(); ++i) { - result.first(i) = solver.getContinuousValue(variables[i]); + result.first(i) = storm::utility::convertNumber(solver.getExactContinuousValue(variables[i])); } return result; } else { @@ -330,8 +331,8 @@ namespace storm { return true; } template - std::vector::EigenVector> NativePolytope::getEigenVertices() const { - storm::storage::geometry::HyperplaneEnumeration he; + std::vector::EigenVector> NativePolytope::getEigenVertices() const { + storm::storage::geometry::HyperplaneEnumeration he; he.generateVerticesFromConstraints(A, b, false); return he.getResultVertices(); } @@ -341,7 +342,7 @@ namespace storm { std::vector result; result.reserve(A.cols()); for(uint_fast64_t col=0; col < A.cols(); ++col){ - result.push_back(manager->declareVariable(namePrefix + std::to_string(col), manager->getRationalType())); + result.push_back(manager.declareVariable(namePrefix + std::to_string(col), manager.getRationalType())); } return result; } diff --git a/src/storm/storage/geometry/NativePolytope.h b/src/storm/storage/geometry/NativePolytope.h index 484e9c064..55df8cbe6 100644 --- a/src/storm/storage/geometry/NativePolytope.h +++ b/src/storm/storage/geometry/NativePolytope.h @@ -12,7 +12,17 @@ namespace storm { template class NativePolytope : public Polytope { public: - + + typedef StormEigen::Matrix EigenMatrix; + typedef StormEigen::Matrix EigenVector; + + enum class EmptyStatus{ + Unknown, //It is unknown whether the polytope is empty or not + Empty, //The polytope is empty + Nonempty //the polytope is not empty + }; + + typedef typename Polytope::Point Point; @@ -40,13 +50,14 @@ namespace storm { */ NativePolytope(NativePolytope const& other); NativePolytope(NativePolytope&& other); - + /*! - * Construction from intern data - */ + * Construction from intern data + */ NativePolytope(EmptyStatus const& emptyStatus, EigenMatrix const& halfspaceMatrix, EigenVector const& halfspaceVector); NativePolytope(EmptyStatus&& emptyStatus, EigenMatrix&& halfspaceMatrix, EigenVector&& halfspaceVector); + ~NativePolytope(); /*! @@ -117,8 +128,6 @@ namespace storm { virtual bool isNativePolytope() const override; private: - typedef StormEigen::Matrix EigenMatrix; - typedef StormEigen::Matrix EigenVector; // returns the vertices of this polytope as EigenVectors std::vector getEigenVertices() const; @@ -134,11 +143,6 @@ namespace storm { storm::expressions::Expression getConstraints(storm::expressions::ExpressionManager const& manager, std::vector const& variables) const; - enum class EmptyStatus{ - Unknown, //It is unknown whether the polytope is empty or not - Empty, //The polytope is empty - Nonempty //the polytope is not empty - }; //Stores whether the polytope is empty or not mutable EmptyStatus emptyStatus; diff --git a/src/storm/storage/geometry/Polytope.cpp b/src/storm/storage/geometry/Polytope.cpp index a0dbd7185..27a9cd046 100644 --- a/src/storm/storage/geometry/Polytope.cpp +++ b/src/storm/storage/geometry/Polytope.cpp @@ -5,6 +5,7 @@ #include "storm/adapters/CarlAdapter.h" #include "storm/adapters/HyproAdapter.h" #include "storm/storage/geometry/HyproPolytope.h" +#include "storm/storage/geometry/NativePolytope.h" #include "storm/utility/macros.h" #include "storm/exceptions/NotImplementedException.h" @@ -39,9 +40,9 @@ namespace storm { boost::optional> const& points) { #ifdef STORM_HAVE_HYPRO return HyproPolytope::create(halfspaces, points); +#else + return NativePolytope::create(halfspaces, points); #endif - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "No polytope implementation specified."); - return nullptr; } template @@ -190,6 +191,11 @@ namespace storm { bool Polytope::isHyproPolytope() const { return false; } + + template + bool Polytope::isNativePolytope() const { + return false; + } template class Polytope; template std::shared_ptr> Polytope::convertNumberRepresentation() const; diff --git a/src/storm/storage/geometry/Polytope.h b/src/storm/storage/geometry/Polytope.h index fc24c4d9a..7aadfbcbb 100644 --- a/src/storm/storage/geometry/Polytope.h +++ b/src/storm/storage/geometry/Polytope.h @@ -135,7 +135,9 @@ namespace storm { virtual std::string toString(bool numbersAsDouble = false) const; virtual bool isHyproPolytope() const; - + + virtual bool isNativePolytope() const; + protected: Polytope(); diff --git a/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp b/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp index 5e365cf13..4a10ba0a6 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp +++ b/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp @@ -152,6 +152,10 @@ namespace storm { std::vector>& HyperplaneEnumeration::getVertexSets() { return this->vertexSets; } + + template class HyperplaneEnumeration; + template class HyperplaneEnumeration; + } } } diff --git a/src/storm/storage/geometry/nativepolytopeconversion/SubsetEnumerator.cpp b/src/storm/storage/geometry/nativepolytopeconversion/SubsetEnumerator.cpp index 1a9db81cc..81c8d9ff7 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/SubsetEnumerator.cpp +++ b/src/storm/storage/geometry/nativepolytopeconversion/SubsetEnumerator.cpp @@ -91,6 +91,8 @@ namespace storm { template class SubsetEnumerator; template class SubsetEnumerator>>; template class SubsetEnumerator>>; + template class SubsetEnumerator>; + template class SubsetEnumerator>; } } } \ No newline at end of file diff --git a/storm-config.h.in b/storm-config.h.in index c5884679c..ae56a6fd9 100644 --- a/storm-config.h.in +++ b/storm-config.h.in @@ -38,6 +38,9 @@ // Whether Z3 is available and to be used (define/undef) #cmakedefine STORM_HAVE_Z3 +// Whether the optimization feature of Z3 is available and to be used (define/undef) +#cmakedefine STORM_HAVE_Z3_OPTIMIZE + // Whether MathSAT is available and to be used (define/undef) #cmakedefine STORM_HAVE_MSAT