From 11198c648c1c591d4ad7e42c5aaf6c01b7cb312a Mon Sep 17 00:00:00 2001 From: PBerger Date: Sat, 21 Sep 2013 00:48:49 +0200 Subject: [PATCH] Fixed include pathes for CUDD in CMakeLists.txt Added a variadic macro for MSVC since the PrismGrammar makes use of emplace magic Patched log4cplus to disable unicode from a parent project "Patched" various serious issues in CUDD, where size_t <-> int problems and forced int to bool conversions piss of the compiler. And me. Former-commit-id: eb27e77ddd1b94b18b446f365442a28df235a238 --- CMakeLists.txt | 18 ++++- resources/3rdparty/cudd-2.5.0/CMakeLists.txt | 6 +- .../3rdparty/cudd-2.5.0/src/obj/cuddObj.cc | 76 +++++++++---------- .../3rdparty/cudd-2.5.0/src/obj/cuddObj.hh | 2 +- .../log4cplus-1.1.2-rc2/CMakeLists.txt | 14 ++-- .../log4cplus-1.1.2-rc2/src/CMakeLists.txt | 4 +- 6 files changed, 69 insertions(+), 51 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 0fd10dbaa..e76d6a05b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -63,6 +63,8 @@ elseif(MSVC) add_definitions(/D_SCL_SECURE_NO_DEPRECATE /D_CRT_SECURE_NO_WARNINGS) # required as the PRCTL Parser bloats object files (COFF) beyond their maximum size (see http://msdn.microsoft.com/en-us/library/8578y171(v=vs.110).aspx) add_definitions(/bigobj) + # required by GTest and PrismGrammar::createIntegerVariable + add_definitions(/D_VARIADIC_MAX=10) # MSVC does not do strict-aliasing, so no option needed else(CLANG) @@ -240,7 +242,13 @@ target_link_libraries(storm-performance-tests ${Boost_LIBRARIES}) ## ############################################################# add_subdirectory("${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0") +include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/src/cudd") +include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/src/epd") +include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/src/mtr") +include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/src/nanotrav") include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/src/obj") +include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/src/st") +include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/src/util") target_link_libraries(storm cudd) target_link_libraries(storm-functional-tests cudd) target_link_libraries(storm-performance-tests cudd) @@ -274,12 +282,14 @@ add_test(NAME storm-performance-tests COMMAND storm-performance-tests) ## Log4CPlus ## ############################################################# -set(BUILD_SHARED_LIBS NO) +set(BUILD_SHARED_LIBS OFF CACHE BOOL "If TRUE, log4cplus is built as a shared library, otherwise as a static library") +set(LOG4CPLUS_BUILD_TESTING NO) +set(LOG4CPLUS_USE_UNICODE OFF) add_subdirectory("${PROJECT_SOURCE_DIR}/resources/3rdparty/log4cplus-1.1.2-rc2") include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/log4cplus-1.1.2-rc2/include") -target_link_libraries(storm log4cplus) -target_link_libraries(storm-functional-tests log4cplus) -target_link_libraries(storm-performance-tests log4cplus) +target_link_libraries(storm log4cplusS) +target_link_libraries(storm-functional-tests log4cplusS) +target_link_libraries(storm-performance-tests log4cplusS) if (UNIX AND NOT APPLE) target_link_libraries(storm rt) if (STORM_USE_COTIRE) diff --git a/resources/3rdparty/cudd-2.5.0/CMakeLists.txt b/resources/3rdparty/cudd-2.5.0/CMakeLists.txt index a426553ab..c7cff2aca 100644 --- a/resources/3rdparty/cudd-2.5.0/CMakeLists.txt +++ b/resources/3rdparty/cudd-2.5.0/CMakeLists.txt @@ -1,11 +1,13 @@ cmake_minimum_required (VERSION 2.8.6) # Set project name -project (cudd C) +project (cudd C CXX) # Main Sources file(GLOB_RECURSE CUDD_HEADERS ${PROJECT_SOURCE_DIR}/src/*.h) +file(GLOB_RECURSE CUDD_HEADERS_CXX ${PROJECT_SOURCE_DIR}/src/*.hh) file(GLOB_RECURSE CUDD_SOURCES ${PROJECT_SOURCE_DIR}/src/*.c) +file(GLOB_RECURSE CUDD_SOURCES_CXX ${PROJECT_SOURCE_DIR}/src/*.cc) # Add base folder for better inclusion paths @@ -24,4 +26,4 @@ if(MSVC) endif() # Add the library -add_library(cudd ${CUDD_SOURCES} ${CUDD_HEADERS}) \ No newline at end of file +add_library(cudd ${CUDD_SOURCES} ${CUDD_HEADERS} ${CUDD_HEADERS_CXX} ${CUDD_SOURCES_CXX}) \ No newline at end of file diff --git a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc index b8a7f2179..ffbaaf826 100644 --- a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc +++ b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc @@ -352,7 +352,7 @@ BDD::operator<=( const BDD& other) const { DdManager *mgr = checkSameManager(other); - return Cudd_bddLeq(mgr,node,other.node); + return Cudd_bddLeq(mgr,node,other.node) != 0; } // BDD::operator<= @@ -362,7 +362,7 @@ BDD::operator>=( const BDD& other) const { DdManager *mgr = checkSameManager(other); - return Cudd_bddLeq(mgr,other.node,node); + return Cudd_bddLeq(mgr,other.node,node) != 0; } // BDD::operator>= @@ -372,7 +372,7 @@ BDD::operator<( const BDD& other) const { DdManager *mgr = checkSameManager(other); - return node != other.node && Cudd_bddLeq(mgr,node,other.node); + return node != other.node && (Cudd_bddLeq(mgr,node,other.node) != 0); } // BDD::operator< @@ -382,7 +382,7 @@ BDD::operator>( const BDD& other) const { DdManager *mgr = checkSameManager(other); - return node != other.node && Cudd_bddLeq(mgr,other.node,node); + return node != other.node && (Cudd_bddLeq(mgr,other.node,node) != 0); } // BDD::operator> @@ -605,7 +605,7 @@ ADD::operator<=( const ADD& other) const { DdManager *mgr = checkSameManager(other); - return Cudd_addLeq(mgr,node,other.node); + return Cudd_addLeq(mgr,node,other.node) != 0; } // ADD::operator<= @@ -615,7 +615,7 @@ ADD::operator>=( const ADD& other) const { DdManager *mgr = checkSameManager(other); - return Cudd_addLeq(mgr,other.node,node); + return Cudd_addLeq(mgr,other.node,node) != 0; } // ADD::operator>= @@ -625,7 +625,7 @@ ADD::operator<( const ADD& other) const { DdManager *mgr = checkSameManager(other); - return node != other.node && Cudd_addLeq(mgr,node,other.node); + return node != other.node && (Cudd_addLeq(mgr,node,other.node) != 0); } // ADD::operator< @@ -635,7 +635,7 @@ ADD::operator>( const ADD& other) const { DdManager *mgr = checkSameManager(other); - return node != other.node && Cudd_addLeq(mgr,other.node,node); + return node != other.node && (Cudd_addLeq(mgr,other.node,node) != 0); } // ADD::operator> @@ -1505,7 +1505,7 @@ Cudd::UnsetTimeLimit() const bool Cudd::TimeLimited() const { - return Cudd_TimeLimited(p->manager); + return Cudd_TimeLimited(p->manager) != 0; } // Cudd::TimeLimited @@ -1531,7 +1531,7 @@ bool Cudd::ReorderingStatus( Cudd_ReorderingType * method) const { - return Cudd_ReorderingStatus(p->manager, method); + return Cudd_ReorderingStatus(p->manager, method) != 0; } // Cudd::ReorderingStatus @@ -1557,7 +1557,7 @@ bool Cudd::ReorderingStatusZdd( Cudd_ReorderingType * method) const { - return Cudd_ReorderingStatusZdd(p->manager, method); + return Cudd_ReorderingStatusZdd(p->manager, method) != 0; } // Cudd::ReorderingStatusZdd @@ -1565,7 +1565,7 @@ Cudd::ReorderingStatusZdd( bool Cudd::zddRealignmentEnabled() const { - return Cudd_zddRealignmentEnabled(p->manager); + return Cudd_zddRealignmentEnabled(p->manager) != 0; } // Cudd::zddRealignmentEnabled @@ -1589,7 +1589,7 @@ Cudd::zddRealignDisable() const bool Cudd::bddRealignmentEnabled() const { - return Cudd_bddRealignmentEnabled(p->manager); + return Cudd_bddRealignmentEnabled(p->manager) != 0; } // Cudd::bddRealignmentEnabled @@ -2004,7 +2004,7 @@ Cudd::SetGroupcheck( bool Cudd::GarbageCollectionEnabled() const { - return Cudd_GarbageCollectionEnabled(p->manager); + return Cudd_GarbageCollectionEnabled(p->manager) != 0; } // Cudd::GarbageCollectionEnabled @@ -2028,7 +2028,7 @@ Cudd::DisableGarbageCollection() const bool Cudd::DeadAreCounted() const { - return Cudd_DeadAreCounted(p->manager); + return Cudd_DeadAreCounted(p->manager) != 0; } // Cudd::DeadAreCounted @@ -2210,7 +2210,7 @@ Cudd::IsInHook( DD_HFP f, Cudd_HookType where) const { - return Cudd_IsInHook(p->manager, f, where); + return Cudd_IsInHook(p->manager, f, where) != 0; } // Cudd::IsInHook @@ -2236,7 +2236,7 @@ Cudd::DisableReorderingReporting() const bool Cudd::ReorderingReporting() const { - return Cudd_ReorderingReporting(p->manager); + return Cudd_ReorderingReporting(p->manager) != 0; } // Cudd::ReorderingReporting @@ -2365,7 +2365,7 @@ Cudd::bddUnbindVar(int index) const bool Cudd::bddVarIsBound(int index) const { - return Cudd_bddVarIsBound(p->manager, index); + return Cudd_bddVarIsBound(p->manager, index) != 0; } // Cudd::bddVarIsBound @@ -2700,7 +2700,7 @@ ADD::Leq( const ADD& g) const { DdManager *mgr = checkSameManager(g); - return Cudd_addLeq(mgr, node, g.node); + return Cudd_addLeq(mgr, node, g.node) != 0; } // ADD::Leq @@ -2744,14 +2744,14 @@ Cudd::Walsh( vector x, vector y) { - int n = x.size(); + size_t n = x.size(); DdNode **X = new DdNode *[n]; DdNode **Y = new DdNode *[n]; for (int i = 0; i < n; i++) { X[i] = x[i].getNode(); Y[i] = y[i].getNode(); } - DdNode *result = Cudd_addWalsh(p->manager, X, Y, n); + DdNode *result = Cudd_addWalsh(p->manager, X, Y, static_cast(n)); delete [] X; delete [] Y; checkReturnValue(result); @@ -3172,7 +3172,7 @@ BDD::VarIsDependent( const BDD& var) const { DdManager *mgr = p->manager; - return Cudd_bddVarIsDependent(mgr, node, var.node); + return Cudd_bddVarIsDependent(mgr, node, var.node) != 0; } // BDD::VarIsDependent @@ -3335,7 +3335,7 @@ BDD::Leq( const BDD& g) const { DdManager *mgr = checkSameManager(g); - return Cudd_bddLeq(mgr, node, g.node); + return Cudd_bddLeq(mgr, node, g.node) != 0; } // BDD::Leq @@ -3540,7 +3540,7 @@ ADD::SwapVariables( vector x, vector y) const { - int n = x.size(); + size_t n = x.size(); DdManager *mgr = p->manager; DdNode **X = new DdNode *[n]; DdNode **Y = new DdNode *[n]; @@ -3548,7 +3548,7 @@ ADD::SwapVariables( X[i] = x[i].node; Y[i] = y[i].node; } - DdNode *result = Cudd_addSwapVariables(mgr, node, X, Y, n); + DdNode *result = Cudd_addSwapVariables(mgr, node, X, Y, static_cast(n)); delete [] X; delete [] Y; checkReturnValue(result); @@ -3574,7 +3574,7 @@ BDD::SwapVariables( std::vector x, std::vector y) const { - int n = x.size(); + size_t n = x.size(); DdManager *mgr = p->manager; DdNode **X = new DdNode *[n]; DdNode **Y = new DdNode *[n]; @@ -3582,7 +3582,7 @@ BDD::SwapVariables( X[i] = x[i].node; Y[i] = y[i].node; } - DdNode *result = Cudd_bddSwapVariables(mgr, node, X, Y, n); + DdNode *result = Cudd_bddSwapVariables(mgr, node, X, Y, static_cast(n)); delete [] X; delete [] Y; checkReturnValue(result); @@ -3595,13 +3595,13 @@ BDD BDD::AdjPermuteX( vector x) const { - int n = x.size(); + size_t n = x.size(); DdManager *mgr = p->manager; DdNode **X = new DdNode *[n]; for (int i = 0; i < n; i++) { X[i] = x[i].node; } - DdNode *result = Cudd_bddAdjPermuteX(mgr, node, X, n); + DdNode *result = Cudd_bddAdjPermuteX(mgr, node, X, static_cast(n)); delete [] X; checkReturnValue(result); return BDD(p, result); @@ -3811,7 +3811,7 @@ bool ABDD::IsCube() const { DdManager *mgr = p->manager; - return Cudd_CheckCube(mgr, node); + return Cudd_CheckCube(mgr, node) != 0; } // ABDD::IsCube @@ -3833,7 +3833,7 @@ BDD::IsVarEssential( int phase) const { DdManager *mgr = p->manager; - return Cudd_bddIsVarEssential(mgr, node, id, phase); + return Cudd_bddIsVarEssential(mgr, node, id, phase) != 0; } // BDD::IsVarEssential @@ -3860,12 +3860,12 @@ Cudd::DumpBlif( int mv) const { DdManager *mgr = p->manager; - int n = nodes.size(); + size_t n = nodes.size(); DdNode **F = new DdNode *[n]; - for (int i = 0; i < n; i ++) { + for (size_t i = 0; i < n; i ++) { F[i] = nodes[i].getNode(); } - int result = Cudd_DumpBlif(mgr, n, F, inames, onames, mname, fp, mv); + int result = Cudd_DumpBlif(mgr, static_cast(n), F, inames, onames, mname, fp, mv); delete [] F; checkReturnValue(result); @@ -4702,7 +4702,7 @@ ABDD::EquivDC( { DdManager *mgr = checkSameManager(G); checkSameManager(D); - return Cudd_EquivDC(mgr, node, G.node, D.node); + return Cudd_EquivDC(mgr, node, G.node, D.node) != 0; } // ABDD::EquivDC @@ -4714,7 +4714,7 @@ BDD::LeqUnless( DdManager *mgr = checkSameManager(G); checkSameManager(D); int res = Cudd_bddLeqUnless(mgr, node, G.node, D.node); - return res; + return res != 0; } // BDD::LeqUnless @@ -4726,7 +4726,7 @@ ADD::EqualSupNorm( int pr) const { DdManager *mgr = checkSameManager(g); - return Cudd_EqualSupNorm(mgr, node, g.node, tolerance, pr); + return Cudd_EqualSupNorm(mgr, node, g.node, tolerance, pr) != 0; } // ADD::EqualSupNorm @@ -5009,7 +5009,7 @@ Cudd::SharingSize( for (vector::size_type i = 0; i != n; ++i) { nodeArray[i] = v[i].getNode(); } - int result = Cudd_SharingSize(nodeArray, n); + int result = Cudd_SharingSize(nodeArray, static_cast(n)); delete [] nodeArray; checkReturnValue(n == 0 || result > 0); return result; diff --git a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh index 726476448..0dce65989 100644 --- a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh +++ b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh @@ -138,7 +138,7 @@ public: DD(Cudd const & manager, DdNode *ddNode); DD(const DD &from); virtual ~DD(); - operator bool() const { return node; } + operator bool() const { return node != 0; } DdManager *manager() const; DdNode * getNode() const; DdNode * getRegularNode() const; diff --git a/resources/3rdparty/log4cplus-1.1.2-rc2/CMakeLists.txt b/resources/3rdparty/log4cplus-1.1.2-rc2/CMakeLists.txt index be347664f..3d67ec3ec 100644 --- a/resources/3rdparty/log4cplus-1.1.2-rc2/CMakeLists.txt +++ b/resources/3rdparty/log4cplus-1.1.2-rc2/CMakeLists.txt @@ -23,7 +23,7 @@ message (STATUS "Threads: ${CMAKE_THREAD_LIBS_INIT}") set(BUILD_SHARED_LIBS TRUE CACHE BOOL "If TRUE, log4cplus is built as a shared library, otherwise as a static library") -message(STATUS "Building shared libs: ${BUILD_SHARED_LIBS}") +message(STATUS "Log4CPlus - Building shared libs: ${BUILD_SHARED_LIBS}") if (WIN32) set (UNICODE_DEFAULT ON) @@ -34,7 +34,7 @@ endif (WIN32) if (MSVC) set (LOG4CPLUS_WORKING_LOCALE_DEFAULT ON) else (MSVC) - set (CMAKE_CXX_FLAGS "-std=c++11") + set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11") set (LOG4CPLUS_WORKING_LOCALE_DEFAULT OFF) endif (MSVC) @@ -59,9 +59,13 @@ if (NOT ${BUILD_SHARED_LIBS}) set (log4cplus_postfix "${log4cplus_postfix}S") endif() -if (UNICODE) +if (UNICODE AND (DEFINED LOG4CPLUS_USE_UNICODE AND LOG4CPLUS_USE_UNICODE)) set (log4cplus_postfix "${log4cplus_postfix}U") -endif (UNICODE) + message(STATUS "Log4CPlus - Using Unicode: YES") +else() + message(STATUS "Log4CPlus - Using Unicode: NO") + set(UNICODE OFF) +endif() if (WITH_ICONV) set(LOG4CPLUS_WITH_ICONV 1) @@ -94,7 +98,7 @@ if (LOG4CPLUS_BUILD_TESTING) endif (LOG4CPLUS_BUILD_TESTING) add_subdirectory (src) -add_subdirectory (loggingserver) +#add_subdirectory (loggingserver) if (LOG4CPLUS_BUILD_TESTING) add_subdirectory (tests) endif (LOG4CPLUS_BUILD_TESTING) diff --git a/resources/3rdparty/log4cplus-1.1.2-rc2/src/CMakeLists.txt b/resources/3rdparty/log4cplus-1.1.2-rc2/src/CMakeLists.txt index 852897972..dbdb53f1e 100644 --- a/resources/3rdparty/log4cplus-1.1.2-rc2/src/CMakeLists.txt +++ b/resources/3rdparty/log4cplus-1.1.2-rc2/src/CMakeLists.txt @@ -51,7 +51,7 @@ set (log4cplus_sources #message (STATUS "Type: ${UNIX}|${CYGWIN}|${WIN32}") -if ("${UNIX}" OR "${CYGWIN}") +if ("${UNIX}" OR "${CYGWIN}" OR APPLE) set (log4cplus_sources ${log4cplus_sources} socket-unix.cxx) elseif (WIN32) @@ -67,6 +67,8 @@ endif () if (UNICODE) add_definitions (-DUNICODE -D_UNICODE -UMBCS -U_MBCS) +else(UNICODE) + add_definitions (-UUNICODE -U_UNICODE -DMBCS -D_MBCS) endif (UNICODE) if (WIN32) add_definitions (-DMINGW_HAS_SECURE_API=1)