cmake: Do not allow dumping with portfolio build.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 617ca2780bf3b17bc78971a319fc64a6320df12b..bbdc863bda8264da6231ca3ef3781187531e0b8c 100644 (file)
--- 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 9f58d35480a6aca230bd8e5c174d83530113452d..9c9f5ec100401eefacced6952c3f1dbfe8ddc593 100644 (file)
--- 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 1b30dc1aa97130fe4cccd09c97d7941f67018842..db63507a7d54094a894981bd0a4ab06c5cdb310a 100644 (file)
--- 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 9627bcd5262ccb28550281c78962ebe8f29f6900..3c995e421c68ee3f23abb00ba49d492eb687499c 100644 (file)
--- 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