Merge branch 'master' into future

Former-commit-id: b249e9706f

resources/3rdparty/glpk-4.53/CMakeLists.txt

@@ -33,6 +33,8 @@ option(DEBUG "Sets whether the DEBUG mode is used" OFF)
 set(ADDITIONAL_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.")
 set(ADDITIONAL_LINK_DIRS "" CACHE STRING "Additional directories added to the link directories.")
 
+MARK_AS_ADVANCED(WITH_GLPK_EXAMPLES WITH_GMP ENABLE_DL ENABLE_ODBC ENABLE_MYSQL)
+
 # If the DEBUG option was turned on, we will target a debug version and a release version otherwise
 if (DEBUG)
     set (CMAKE_BUILD_TYPE "DEBUG")

resources/3rdparty/gtest-1.7.0/CMakeLists.txt

@@ -22,6 +22,8 @@ option(gtest_build_samples "Build gtest's sample programs." OFF)
 
 option(gtest_disable_pthreads "Disable uses of pthreads in gtest." OFF)
 
+MARK_AS_ADVANCED(gtest_build_tests gtest_build_samples gtest_disable_pthreads gtest_force_shared_crt)
+
 # Defines pre_project_set_up_hermetic_build() and set_up_hermetic_build().
 include(cmake/hermetic_build.cmake OPTIONAL)
 

resources/3rdparty/log4cplus-1.1.3-rc1/CMakeLists.txt

@@ -139,3 +139,5 @@ endif (LOG4CPLUS_QT4)
 if (LOG4CPLUS_DEFINE_INSTALL_TARGET)
 	include(Log4CPlusCPack.cmake)
 endif()
+
+MARK_AS_ADVANCED(ENABLE_SYMBOLS_VISIBILITY _WIN32_WINNT WITH_ICONV LOG4CPLUS_WORKING_C_LOCALE LOG4CPLUS_WORKING_LOCALE LOG4CPLUS_BUILD_LOGGINGSERVER LOG4CPLUS_BUILD_TESTING LOG4CPLUS_DEFINE_INSTALL_TARGET LOG4CPLUS_QT4)

resources/3rdparty/log4cplus-1.1.3-rc1/ConfigureChecks.cmake

@@ -380,3 +380,5 @@ set(HAVE_PRETTY_FUNCTION_MACRO ${LOG4CPLUS_HAVE_PRETTY_FUNCTION_MACRO} )
 
 set(HAVE___SYNC_ADD_AND_FETCH  ${LOG4CPLUS_HAVE___SYNC_ADD_AND_FETCH} )
 set(HAVE___SYNC_SUB_AND_FETCH  ${LOG4CPLUS_HAVE___SYNC_SUB_AND_FETCH} )
+
+MARK_AS_ADVANCED(LIBADVAPI32 LIBCPOSIX LIBICONV LIBKERNEL32 LIBNSL LIBPOSIX4 LIBRT LIBSOCKET LIBWS2_32)

resources/cmake/FindGMP.cmake

@@ -51,4 +51,6 @@ elseif(GMP_FOUND)
    if(GMP_FIND_REQUIRED)
       message(FATAL_ERROR "Could not find GMP")
    endif()
-endif()
+endif()
+
+MARK_AS_ADVANCED(GMP_MPIRXX_LIBRARY GMP_MPIR_LIBRARY GMP_INCLUDE_DIR GMP_LIBRARY)

src/adapters/CarlAdapter.h

@@ -6,8 +6,7 @@
 
 #ifdef STORM_HAVE_CARL
 
-#include <cln/cln.h>
-#include <gmpxx.h>
+#include <carl/numbers/numbers.h>
 #include <carl/core/MultivariatePolynomial.h>
 #include <carl/core/RationalFunction.h>
 #include <carl/core/VariablePool.h>

src/logic/ComparisonType.h

@@ -6,7 +6,14 @@
 namespace storm {
 	namespace logic {
 		enum class ComparisonType { Less, LessEqual, Greater, GreaterEqual };
-        
+         
+                inline bool isStrict(ComparisonType t) {
+                    return (t == ComparisonType::Less || t == ComparisonType::Greater);
+                }
+                
+                inline bool isLowerBound(ComparisonType t) {
+                    return (t == ComparisonType::Greater || t == ComparisonType::GreaterEqual);
+                }
         std::ostream& operator<<(std::ostream& out, ComparisonType const& comparisonType);
 	}
 }

src/models/sparse/MarkovAutomaton.cpp

@@ -218,11 +218,11 @@ namespace storm {
             }
             
             template class MarkovAutomaton<double>;
-            template class MarkovAutomaton<float>;
+//            template class MarkovAutomaton<float>;
             
-#ifdef STORM_HAVE_CARL
-            template class MarkovAutomaton<storm::RationalFunction>;
-#endif
+//#ifdef STORM_HAVE_CARL
+//            template class MarkovAutomaton<storm::RationalFunction>;
+//#endif
 
         } // namespace sparse
     } // namespace models

src/models/sparse/StochasticTwoPlayerGame.cpp

@@ -32,11 +32,11 @@ namespace storm {
             }
             
             template class StochasticTwoPlayerGame<double>;
-            template class StochasticTwoPlayerGame<float>;
+//            template class StochasticTwoPlayerGame<float>;
             
-#ifdef STORM_HAVE_CARL
-            template class StochasticTwoPlayerGame<storm::RationalFunction>;
-#endif
+//#ifdef STORM_HAVE_CARL
+//            template class StochasticTwoPlayerGame<storm::RationalFunction>;
+//#endif
             
         } // namespace sparse
     } // namespace models

src/storage/BitVector.cpp

@@ -91,9 +91,9 @@ namespace storm {
             // Intentionally left empty.
         }
         
-        BitVector::BitVector(BitVector&& other) : bitCount(other.bitCount), bucketVector(std::move(other.bucketVector)) {
+        //BitVector::BitVector(BitVector&& other) : bitCount(other.bitCount), bucketVector(std::move(other.bucketVector)) {
             // Intentionally left empty.
-        }
+        //}
         
         BitVector& BitVector::operator=(BitVector const& other) {
             // Only perform the assignment if the source and target are not identical.

src/storage/BitVector.h

@@ -135,7 +135,7 @@ namespace storm {
              *
              * @param other The bit vector from which to move-construct.
              */
-            BitVector(BitVector&& other);
+            BitVector(BitVector&& other) = default;
             
             /*!
              * Compares the given bit vector with the current one.