sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

first attempt at adapting to Z3 interface change

tempestpy_adaptions
dehnert 7 years ago
parent
a6e6d5993f
commit
cdfa328464
6 changed files with 35 additions and 10 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 9
      resources/3rdparty/CMakeLists.txt
  2. 19
      src/storm/adapters/Z3ExpressionAdapter.cpp
  3. 2
      src/storm/solver/stateelimination/DynamicStatePriorityQueue.h
  4. 4
      src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp
  5. 4
      src/test/storm/utility/KSPTest.cpp
  6. 7
      storm-config.h.in

9
resources/3rdparty/CMakeLists.txt
View File

@ -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

19
src/storm/adapters/Z3ExpressionAdapter.cpp
View File

@ -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<storm::RationalNumber>((int_fast64_t) num) / storm::utility::convertNumber<storm::RationalNumber>((int_fast64_t) den));
return manager.rational(storm::utility::convertNumber<storm::RationalNumber>(static_cast<int_fast64_t>(num)) / storm::utility::convertNumber<storm::RationalNumber>(static_cast<int_fast64_t>(den)));
} else {
return manager.rational(storm::utility::convertNumber<storm::RationalNumber>(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<long long>(expression.getValue()));
z3::expr result = context.int_val(static_cast<Z3_SIGNED_INTEGER>(expression.getValue()));
expressionCache.emplace(&expression, result);
return result;

2
src/storm/solver/stateelimination/DynamicStatePriorityQueue.h
View File

@ -17,7 +17,7 @@ namespace storm {
namespace stateelimination {
struct PriorityComparator {
bool operator()(std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& first, std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& second) {
bool operator()(std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& first, std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& second) const {
return (first.second < second.second) || (first.second == second.second && first.first < second.first) ;
}
};

4
src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp
View File

@ -148,7 +148,7 @@ TEST(MaximalEndComponentDecomposition, Example1) {
storm::storage::MaximalEndComponentDecomposition<double> 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<double> 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});

4
src/test/storm/utility/KSPTest.cpp
View File

@ -81,7 +81,7 @@ TEST(KSPTest, kspStateSet) {
storm::utility::ksp::ShortestPathsGenerator<double> 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<double> 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};

7
storm-config.h.in
View File

@ -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

Write Preview
Loading…
Cancel
Save