fixes for z3LP solver and nativePolytopes

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)

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<double>(num) / static_cast<double>(den));
+                                        return manager.rational(storm::utility::convertNumber<storm::RationalNumber>(num) / storm::utility::convertNumber<storm::RationalNumber>(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<storm::RationalNumber>(std::string(Z3_get_numeral_string(expr.ctx(), expr))));
                                     }
                                 }
                             case Z3_OP_UNINTERPRETED:

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<storm::RationalNumber>(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,24 +311,29 @@ 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<storm::RationalNumber>(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() {
@@ -316,127 +341,127 @@ namespace storm {
             }
 
             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.";
             }
 
 

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<z3::context> context;

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<ValueType>::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<EigenVector> eigenPoints;
                     eigenPoints.reserve(points.size());
                     for(auto const& p : points){
-                        eigenPoints.emplace_back(storm::adapters::EigenAdapter<ValueType>::toEigenVector(p));
+                        eigenPoints.emplace_back(storm::adapters::EigenAdapter::toEigenVector(p));
                     }
 
                     storm::storage::geometry::QuickHull<ValueType> qh;
@@ -92,11 +93,11 @@ namespace storm {
             
             template <typename ValueType>
             std::vector<typename Polytope<ValueType>::Point> NativePolytope<ValueType>::getVertices() const {
-                std::vector<hypro::Point<ValueType>> eigenVertices = getEigenVertices();
+                std::vector<EigenVector> eigenVertices = getEigenVertices();
                 std::vector<Point> result;
                 result.reserve(eigenVertices.size());
                 for(auto const& p : eigenVertices) {
-                    result.push_back(storm::adapters::EigenAdapter<ValueType>::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<ValueType>::toStdVector(A.row(row)), b.row(row));
+                    result.emplace_back(storm::adapters::EigenAdapter::toStdVector(EigenVector(A.row(row))), b(row));
                 }
+                return result;
             }
 
             template <typename ValueType>
             bool NativePolytope<ValueType>::isEmpty() const {
-                if(emptyStatus == emptyStatus::Unknown) {
+                if(emptyStatus == EmptyStatus::Unknown) {
                     storm::expressions::ExpressionManager manager;
                     std::unique_ptr<storm::solver::SmtSolver> 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 <typename ValueType>
@@ -140,7 +142,7 @@ namespace storm {
             
             template <typename ValueType>
             bool NativePolytope<ValueType>::contains(Point const& point) const{
-                EigenVector x = storm::adapters::EigenAdapter<ValueType>::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<NativePolytope<ValueType>>(std::move(resultA), std::move(resultb));
+                return std::make_shared<NativePolytope<ValueType>>(EmptyStatus::Unknown, std::move(resultA), std::move(resultb));
             }
             
             template <typename ValueType>
             std::shared_ptr<Polytope<ValueType>> NativePolytope<ValueType>::intersection(Halfspace<ValueType> const& halfspace) const{
                 EigenMatrix resultA(A.rows() + 1, A.cols());
-                resultA << A,
-                           storm::adapters::EigenAdapter<ValueType>::toEigenVector(halfspace.normal());
+                resultA << A, storm::adapters::EigenAdapter::toEigenVector(halfspace.normalVector());
                 EigenVector resultb(resultA.rows());
                 resultb << b,
                            halfspace.offset();
-                return std::make_shared<NativePolytope<ValueType>>(std::move(resultA), std::move(resultb));
+                return std::make_shared<NativePolytope<ValueType>>(EmptyStatus::Unknown, std::move(resultA), std::move(resultb));
             }
             
             template <typename ValueType>
@@ -202,7 +203,7 @@ namespace storm {
                     return std::make_shared<NativePolytope<ValueType>>(dynamic_cast<NativePolytope<ValueType> const&>(*rhs));
                 } else if (rhs->isEmpty()) {
                     return std::make_shared<NativePolytope<ValueType>>(*this);
-                } else if (this->isUniversal() || rhs->isUniversal) {
+                } else if (this->isUniversal() || rhs->isUniversal()) {
                     return std::make_shared<NativePolytope<ValueType>>(std::vector<Halfspace<ValueType>>());
                 }
 
@@ -270,7 +271,7 @@ namespace storm {
                 }
                 EigenVector eigenVector = storm::adapters::EigenAdapter::toEigenVector(vector);
 
-                Eigen::FullPivLU<EigenMatrix> luMatrix( eigenMatrix );
+                StormEigen::FullPivLU<EigenMatrix> 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<storm::expressions::Variable> 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<ValueType>((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<ValueType>(solver.getExactContinuousValue(variables[i]));
                     }
                     return result;
                 } else {
@@ -330,8 +331,8 @@ namespace storm {
                 return true;
             }
             template <typename ValueType>
-            std::vector<typename NativePolytope::ValueType>::EigenVector> NativePolytope<ValueType>::getEigenVertices() const {
-                storm::storage::geometry::HyperplaneEnumeration he;
+            std::vector<typename NativePolytope<ValueType>::EigenVector> NativePolytope<ValueType>::getEigenVertices() const {
+                storm::storage::geometry::HyperplaneEnumeration<ValueType> he;
                 he.generateVerticesFromConstraints(A, b, false);
                 return he.getResultVertices();
             }
@@ -341,7 +342,7 @@ namespace storm {
                 std::vector<storm::expressions::Variable> 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;
             }

src/storm/storage/geometry/NativePolytope.h

@@ -13,6 +13,16 @@ namespace storm {
             class NativePolytope : public Polytope<ValueType> {
             public:
 
+                typedef StormEigen::Matrix<ValueType, StormEigen::Dynamic, StormEigen::Dynamic> EigenMatrix;
+                typedef StormEigen::Matrix<ValueType, StormEigen::Dynamic, 1> 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<ValueType>::Point Point;
 
 
@@ -42,11 +52,12 @@ namespace storm {
                 NativePolytope(NativePolytope<ValueType>&& 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<ValueType, StormEigen::Dynamic, StormEigen::Dynamic> EigenMatrix;
-                typedef StormEigen::Matrix<ValueType, StormEigen::Dynamic, 1> EigenVector;
 
                 // returns the vertices of this polytope as EigenVectors
                 std::vector<EigenVector> getEigenVertices() const;
@@ -134,11 +143,6 @@ namespace storm {
                 storm::expressions::Expression getConstraints(storm::expressions::ExpressionManager const& manager, std::vector<storm::expressions::Variable> 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;
 

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<std::vector<Point>> const& points) {
 #ifdef STORM_HAVE_HYPRO
                 return HyproPolytope<ValueType>::create(halfspaces, points);
+#else
+                return NativePolytope<ValueType>::create(halfspaces, points);
 #endif
-                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "No polytope implementation specified.");
-                return nullptr;
             }
             
             template <typename ValueType>
@@ -191,6 +192,11 @@ namespace storm {
                 return false;
             }
 
+            template <typename ValueType>
+            bool Polytope<ValueType>::isNativePolytope() const {
+                return false;
+            }
+            
             template class Polytope<double>;
             template std::shared_ptr<Polytope<double>> Polytope<double>::convertNumberRepresentation() const;
             

src/storm/storage/geometry/Polytope.h

@@ -136,6 +136,8 @@ namespace storm {
                
                 virtual bool isHyproPolytope() const;
 
+                virtual bool isNativePolytope() const;
+
             protected:
                 
                 Polytope();

src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp

@@ -152,6 +152,10 @@ namespace storm {
             std::vector<std::vector<uint_fast64_t>>& HyperplaneEnumeration<ValueType>::getVertexSets() {
                 return this->vertexSets;
             }
+
+            template class HyperplaneEnumeration<double>;
+            template class HyperplaneEnumeration<storm::RationalNumber>;
+
         }
     }
 }

src/storm/storage/geometry/nativepolytopeconversion/SubsetEnumerator.cpp

@@ -91,6 +91,8 @@ namespace storm {
             template class SubsetEnumerator<std::nullptr_t>;
             template class SubsetEnumerator<std::vector<StormEigen::Matrix<double, StormEigen::Dynamic, 1>>>;
             template class SubsetEnumerator<std::vector<StormEigen::Matrix<storm::RationalNumber, StormEigen::Dynamic, 1>>>;
+            template class SubsetEnumerator<StormEigen::Matrix<double, StormEigen::Dynamic, StormEigen::Dynamic>>;
+            template class SubsetEnumerator<StormEigen::Matrix<storm::RationalNumber, StormEigen::Dynamic, StormEigen::Dynamic>>;
         }
     }
 }

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