diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-09-17 14:16:24 -0700 |
---|---|---|
committer | Mathias Preiner <mathias.preiner@gmail.com> | 2018-09-22 16:30:59 -0700 |
commit | 4e4dc5b946d11a676a45c3bd7ff058174ab8d748 (patch) | |
tree | e137d6d8b270e42a2e145376a09a01e79d51ed2b | |
parent | 6f2daa4e9834d0348c7eeec0dcb3dddbd98ca934 (diff) |
cmake: Do not allow dumping with portfolio build.
-rw-r--r-- | CMakeLists.txt | 12 | ||||
-rw-r--r-- | cmake/ConfigDebug.cmake | 11 | ||||
-rw-r--r-- | cmake/ConfigProduction.cmake | 11 | ||||
-rw-r--r-- | cmake/ConfigTesting.cmake | 11 |
4 files changed, 38 insertions, 7 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 617ca2780..bbdc863bd 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -245,10 +245,6 @@ if(ENABLE_DEBUG_CONTEXT_MM) add_definitions(-DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER) endif() -if(ENABLE_DUMPING) - add_definitions(-DCVC4_DUMPING) -endif() - if(ENABLE_DEBUG_SYMBOLS) add_check_c_cxx_flag("-ggdb3") endif() @@ -260,6 +256,9 @@ endif() # This check needs to come before the USE_CLN check. if(ENABLE_PORTFOLIO) find_package(Boost 1.50.0 REQUIRED COMPONENTS thread) + if (ENABLE_DUMPING) + message(FATAL_ERROR "Dumping not supported with a portfolio build.") + endif() # Disable CLN for portfolio builds since it is not thread safe (uses an # unlocked hash table internally). if(USE_CLN) @@ -275,6 +274,11 @@ if(ENABLE_PORTFOLIO) set(BOOST_HAS_THREAD_ATTR 1) endif() +# This has to be processed after ENABLE_PORTFOLIO (disables dumping support). +if(ENABLE_DUMPING) + add_definitions(-DCVC4_DUMPING) +endif() + if(ENABLE_PROFILING) add_definitions(-DCVC4_PROFILING) add_check_c_cxx_flag("-pg") diff --git a/cmake/ConfigDebug.cmake b/cmake/ConfigDebug.cmake index 9f58d3548..9c9f5ec10 100644 --- a/cmake/ConfigDebug.cmake +++ b/cmake/ConfigDebug.cmake @@ -18,7 +18,16 @@ cvc4_set_option(ENABLE_PROOFS ON) # enable_tracing=yes cvc4_set_option(ENABLE_TRACING ON) # enable_dumping=yes -cvc4_set_option(ENABLE_DUMPING ON) +if(ENABLE_PORTFOLIO) + if(ENABLE_DUMPING) + message(FATAL_ERROR "Dumping not supported with a portfolio build.") + else() + message(WARNING + "Disabling dumping support, not supported with a portfolio build.") + endif() +else() + cvc4_set_option(ENABLE_DUMPING ON) +endif() # enable_muzzle=no cvc4_set_option(ENABLE_MUZZLE OFF) # enable_valgrind=optional diff --git a/cmake/ConfigProduction.cmake b/cmake/ConfigProduction.cmake index 1b30dc1aa..db63507a7 100644 --- a/cmake/ConfigProduction.cmake +++ b/cmake/ConfigProduction.cmake @@ -15,7 +15,16 @@ cvc4_set_option(ENABLE_PROOFS ON) # enable_tracing=no cvc4_set_option(ENABLE_TRACING OFF) # enable_dumping=yes -cvc4_set_option(ENABLE_DUMPING ON) +if(ENABLE_PORTFOLIO) + if(ENABLE_DUMPING) + message(FATAL_ERROR "Dumping not supported with a portfolio build.") + else() + message(WARNING + "Disabling dumping support, not supported with a portfolio build.") + endif() +else() + cvc4_set_option(ENABLE_DUMPING ON) +endif() # enable_muzzle=no cvc4_set_option(ENABLE_MUZZLE OFF) # enable_valgrind=no diff --git a/cmake/ConfigTesting.cmake b/cmake/ConfigTesting.cmake index 9627bcd52..3c995e421 100644 --- a/cmake/ConfigTesting.cmake +++ b/cmake/ConfigTesting.cmake @@ -15,7 +15,16 @@ cvc4_set_option(ENABLE_PROOFS ON) # enable_tracing=yes cvc4_set_option(ENABLE_TRACING ON) # enable_dumping=yes -cvc4_set_option(ENABLE_DUMPING ON) +if(ENABLE_PORTFOLIO) + if(ENABLE_DUMPING) + message(FATAL_ERROR "Dumping not supported with a portfolio build.") + else() + message(WARNING + "Disabling dumping support, not supported with a portfolio build.") + endif() +else() + cvc4_set_option(ENABLE_DUMPING ON) +endif() # enable_muzzle=no cvc4_set_option(ENABLE_MUZZLE OFF) # enable_valgrind=no |