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: eb27e77ddd

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)

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})
+add_library(cudd ${CUDD_SOURCES} ${CUDD_HEADERS} ${CUDD_HEADERS_CXX} ${CUDD_SOURCES_CXX})

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<ADD> x,
   vector<ADD> 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<int>(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<ADD> x,
   vector<ADD> 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<int>(n));
     delete [] X;
     delete [] Y;
     checkReturnValue(result);
@@ -3574,7 +3574,7 @@ BDD::SwapVariables(
   std::vector<BDD> x,
   std::vector<BDD> 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<int>(n));
     delete [] X;
     delete [] Y;
     checkReturnValue(result);
@@ -3595,13 +3595,13 @@ BDD
 BDD::AdjPermuteX(
   vector<BDD> 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<int>(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<int>(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<BDD>::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<int>(n));
     delete [] nodeArray;
     checkReturnValue(n == 0 || result > 0);
     return result;

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;

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)

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)