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<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:
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<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,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<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() {
-
+
+ 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<z3::context> 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<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;
}
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 <typename ValueType>
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;
@@ -40,13 +50,14 @@ namespace storm {
*/
NativePolytope(NativePolytope<ValueType> const& other);
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;
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<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>
@@ -190,6 +191,11 @@ namespace storm {
bool Polytope<ValueType>::isHyproPolytope() const {
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;
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<std::vector<uint_fast64_t>>& HyperplaneEnumeration<ValueType>::getVertexSets() {
return this->vertexSets;
}
+
+ template class HyperplaneEnumeration<double>;
+ template class HyperplaneEnumeration<storm::RationalNumber>;
+
}
}
}
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<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>>;
}
}
}
\ 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