From bf64fa2b3fb44b667cb9f1100a75c93b9f66cdfc Mon Sep 17 00:00:00 2001 From: Roman Andriushchenko Date: Wed, 13 Nov 2024 14:15:39 +0100 Subject: [PATCH] require newer boost version --- install.sh | 2 +- payntbind/CMakeLists.txt | 11 +---------- payntbind/src/synthesis/quotient/ColoringSmt.cpp | 2 +- 3 files changed, 3 insertions(+), 12 deletions(-) diff --git a/install.sh b/install.sh index ad50b10c..5354283a 100755 --- a/install.sh +++ b/install.sh @@ -35,7 +35,7 @@ git clone https://github.com/moves-rwth/storm.git storm mkdir -p ${PREREQUISITES}/storm/build cd ${PREREQUISITES}/storm/build cmake .. -make storm storm-pomdp storm-counterexamples --jobs ${COMPILE_JOBS} +make storm storm-cli storm-pomdp --jobs ${COMPILE_JOBS} # make check --jobs ${COMPILE_JOBS} # setup and activate python environment diff --git a/payntbind/CMakeLists.txt b/payntbind/CMakeLists.txt index e2bac441..c04bd013 100644 --- a/payntbind/CMakeLists.txt +++ b/payntbind/CMakeLists.txt @@ -29,16 +29,7 @@ set(CMAKE_INTERPROCEDURAL_OPTIMIZATION OFF) # which is recommended *not* to do, but leads to errors otherwise. set(CMAKE_CXX_VISIBILITY_PRESET "default") - -# Workaround for issue with Boost >= 1.81 -find_package(Boost 1.65.1 QUIET REQUIRED COMPONENTS filesystem system) -if (Boost_FOUND) - if (${Boost_VERSION} VERSION_GREATER_EQUAL "1.81.0") - message(STATUS "Stormpy - Using workaround for Boost >= 1.81") - set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DBOOST_PHOENIX_STL_TUPLE_H_") - endif() -endif () - +find_package(Boost 1.83 REQUIRED) #+ # Set configurations set(STORM_VERSION ${storm_VERSION}) diff --git a/payntbind/src/synthesis/quotient/ColoringSmt.cpp b/payntbind/src/synthesis/quotient/ColoringSmt.cpp index 3c9723a7..298d9c2d 100644 --- a/payntbind/src/synthesis/quotient/ColoringSmt.cpp +++ b/payntbind/src/synthesis/quotient/ColoringSmt.cpp @@ -514,7 +514,7 @@ std::pair>> ColoringSmt::areCh } STORM_LOG_THROW(harmonizing_hole_found, storm::exceptions::UnexpectedException, "harmonized UNSAT core is not SAT");*/ - solver.add(0 <= harmonizing_variable and harmonizing_variable < family.numHoles(), "harmonizing_domain"); + solver.add(0 <= harmonizing_variable and harmonizing_variable < (int)(family.numHoles()), "harmonizing_domain"); consistent = check(); STORM_LOG_THROW(consistent, storm::exceptions::UnexpectedException, "harmonized UNSAT core is not SAT"); model = solver.get_model();