From cdfa32846463872bfa51a87c86c09bd14e297879 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 22 Jun 2018 10:57:52 +0200 Subject: [PATCH] first attempt at adapting to Z3 interface change --- resources/3rdparty/CMakeLists.txt | 9 +++++++++ src/storm/adapters/Z3ExpressionAdapter.cpp | 19 ++++++++++++++----- .../DynamicStatePriorityQueue.h | 2 +- .../MaximalEndComponentDecompositionTest.cpp | 4 ++-- src/test/storm/utility/KSPTest.cpp | 4 ++-- storm-config.h.in | 7 +++++++ 6 files changed, 35 insertions(+), 10 deletions(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index caaa2a0f1..18a68a23f 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -168,6 +168,15 @@ else() message (WARNING "Storm - Z3 not found. Building of Prism/JANI models will not be supported.") endif(Z3_FOUND) +# split Z3 version into its components +string(REPLACE "." ";" Z3_VERSION_LIST ${Z3_VERSION}) +list(GET Z3_VERSION_LIST 0 STORM_Z3_VERSION_MAJOR) +list(GET Z3_VERSION_LIST 1 STORM_Z3_VERSION_MINOR) +list(GET Z3_VERSION_LIST 2 STORM_Z3_VERSION_PATCH) +if (NOT "${Z3_VERSION}" VERSION_LESS "4.7.1") + set(STORM_Z3_API_USES_STANDARD_INTEGERS ON) +endif() + ############################################################# ## ## glpk diff --git a/src/storm/adapters/Z3ExpressionAdapter.cpp b/src/storm/adapters/Z3ExpressionAdapter.cpp index c7e27756d..fec9068b0 100644 --- a/src/storm/adapters/Z3ExpressionAdapter.cpp +++ b/src/storm/adapters/Z3ExpressionAdapter.cpp @@ -12,6 +12,15 @@ namespace storm { namespace adapters { #ifdef STORM_HAVE_Z3 + +#ifdef STORM_Z3_API_USES_STANDARD_INTEGERS + typedef int64_t Z3_SIGNED_INTEGER; + typedef int64_t Z3_UNSIGNED_INTEGER; +#else + typedef long long Z3_SIGNED_INTEGER; + typedef unsigned long long Z3_UNSIGNED_INTEGER; +#endif + Z3ExpressionAdapter::Z3ExpressionAdapter(storm::expressions::ExpressionManager& manager, z3::context& context) : manager(manager), context(context), additionalAssertions(), variableToExpressionMapping() { // Intentionally left empty. } @@ -133,17 +142,17 @@ namespace storm { case Z3_OP_ANUM: // Arithmetic numeral. if (expr.is_int() && expr.is_const()) { - long long value; + Z3_SIGNED_INTEGER value; if (Z3_get_numeral_int64(expr.ctx(), expr, &value)) { return manager.integer(value); } else { STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Expression is constant integer and value does not fit into 64-bit integer."); } } else if (expr.is_real() && expr.is_const()) { - long long num; - long long den; + Z3_SIGNED_INTEGER num; + Z3_SIGNED_INTEGER den; if (Z3_get_numeral_rational_int64(expr.ctx(), expr, &num, &den)) { - return manager.rational(storm::utility::convertNumber((int_fast64_t) num) / storm::utility::convertNumber((int_fast64_t) den)); + return manager.rational(storm::utility::convertNumber(static_cast(num)) / storm::utility::convertNumber(static_cast(den))); } else { return manager.rational(storm::utility::convertNumber(std::string(Z3_get_numeral_string(expr.ctx(), expr)))); } @@ -304,7 +313,7 @@ namespace storm { return cacheIt->second; } - z3::expr result = context.int_val(static_cast(expression.getValue())); + z3::expr result = context.int_val(static_cast(expression.getValue())); expressionCache.emplace(&expression, result); return result; diff --git a/src/storm/solver/stateelimination/DynamicStatePriorityQueue.h b/src/storm/solver/stateelimination/DynamicStatePriorityQueue.h index 0ac38769d..4065ee265 100644 --- a/src/storm/solver/stateelimination/DynamicStatePriorityQueue.h +++ b/src/storm/solver/stateelimination/DynamicStatePriorityQueue.h @@ -17,7 +17,7 @@ namespace storm { namespace stateelimination { struct PriorityComparator { - bool operator()(std::pair const& first, std::pair const& second) { + bool operator()(std::pair const& first, std::pair const& second) const { return (first.second < second.second) || (first.second == second.second && first.first < second.first) ; } }; diff --git a/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp b/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp index b30b5259b..ced1cd6b0 100644 --- a/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp +++ b/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp @@ -148,7 +148,7 @@ TEST(MaximalEndComponentDecomposition, Example1) { storm::storage::MaximalEndComponentDecomposition mecDecomposition(*mdp); - EXPECT_EQ(mecDecomposition.size(), 2); + EXPECT_EQ(2ull, mecDecomposition.size()); ASSERT_TRUE(mecDecomposition[0].getStateSet() == storm::storage::MaximalEndComponent::set_type{2}); EXPECT_TRUE(mecDecomposition[0].getChoicesForState(2) == storm::storage::MaximalEndComponent::set_type{3}); @@ -167,7 +167,7 @@ TEST(MaximalEndComponentDecomposition, Example2) { storm::storage::MaximalEndComponentDecomposition mecDecomposition(*mdp); - EXPECT_EQ(mecDecomposition.size(), 2); + EXPECT_EQ(2ull, mecDecomposition.size()); ASSERT_TRUE(mecDecomposition[0].getStateSet() == storm::storage::MaximalEndComponent::set_type{2}); EXPECT_TRUE(mecDecomposition[0].getChoicesForState(2) == storm::storage::MaximalEndComponent::set_type{4}); diff --git a/src/test/storm/utility/KSPTest.cpp b/src/test/storm/utility/KSPTest.cpp index dfe14e817..d584a7660 100644 --- a/src/test/storm/utility/KSPTest.cpp +++ b/src/test/storm/utility/KSPTest.cpp @@ -81,7 +81,7 @@ TEST(KSPTest, kspStateSet) { storm::utility::ksp::ShortestPathsGenerator spg(*model, testState); auto bv = spg.getStates(7); - EXPECT_EQ(50, bv.getNumberOfSetBits()); + EXPECT_EQ(50ull, bv.getNumberOfSetBits()); // The result may sadly depend on the compiler/system, so checking a particular outcome is not feasible. // storm::storage::BitVector referenceBV(model->getNumberOfStates(), false); @@ -97,7 +97,7 @@ TEST(KSPTest, kspPathAsList) { storm::utility::ksp::ShortestPathsGenerator spg(*model, testState); auto list = spg.getPathAsList(7); - EXPECT_EQ(50, list.size()); + EXPECT_EQ(50ull, list.size()); // TODO: use path that actually has a loop or something to make this more interesting // auto reference = storm::utility::ksp::OrderedStateList{296, 288, 281, 272, 266, 260, 253, 245, 238, 230, 224, 218, 211, 203, 196, 188, 182, 176, 169, 161, 154, 146, 140, 134, 127, 119, 112, 104, 98, 92, 85, 77, 70, 81, 74, 65, 58, 52, 45, 37, 30, 22, 17, 12, 9, 6, 4, 2, 1, 0}; diff --git a/storm-config.h.in b/storm-config.h.in index b0290b751..55d2247d3 100644 --- a/storm-config.h.in +++ b/storm-config.h.in @@ -41,6 +41,13 @@ // Whether the optimization feature of Z3 is available and to be used (define/undef) #cmakedefine STORM_HAVE_Z3_OPTIMIZE +// Version of Z3 used by Storm. +#define STORM_Z3_VERSION_MAJOR @STORM_Z3_VERSION_MAJOR@ +#define STORM_Z3_VERSION_MINOR @STORM_Z3_VERSION_MINOR@ +#define STORM_Z3_VERSION_PATCH @STORM_Z3_VERSION_PATCH@ +#define STORM_Z3_VERSION @Z3_VERSION@ +#cmakedefine STORM_Z3_API_USES_STANDARD_INTEGERS + // Whether MathSAT is available and to be used (define/undef) #cmakedefine STORM_HAVE_MSAT