From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 6 Sep 2018 22:53:13 +0000 (-0700)
Subject: cmake: Add ENABLE_DEBUG_CONTEXT_MM to enable the debug context memory manager.
X-Git-Tag: cvc5-1.0.0~4571
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=297512ce8ee4b0684c27e3bd87662a1823f6a4dd;p=cvc5.git

cmake: Add ENABLE_DEBUG_CONTEXT_MM to enable the debug context memory manager.
---

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 69229c09d..883ebc752 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -177,9 +177,10 @@ cvc4_option(ENABLE_VALGRIND      "Enable valgrind instrumentation")
 cvc4_option(ENABLE_SHARED        "Build as shared library")
 # >> 2-valued: ON OFF
 #    > for options where we don't need to detect if set by user (default: OFF)
-option(ENABLE_BEST      "Enable dependencies known to give best performance")
-option(ENABLE_COVERAGE  "Enable support for gcov coverage testing")
-option(ENABLE_PROFILING "Enable support for gprof profiling")
+option(ENABLE_BEST             "Enable dependencies known to give best performance")
+option(ENABLE_COVERAGE         "Enable support for gcov coverage testing")
+option(ENABLE_DEBUG_CONTEXT_MM "Enable the debug context memory manager")
+option(ENABLE_PROFILING        "Enable support for gprof profiling")
 
 # Optional dependencies
 #
@@ -347,6 +348,10 @@ if(ENABLE_COVERAGE)
     DEPENDENCIES cvc4-bin)
 endif()
 
+if(ENABLE_DEBUG_CONTEXT_MM)
+  add_definitions(-DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER)
+endif()
+
 if(ENABLE_DUMPING)
   add_definitions(-DCVC4_DUMPING)
 else()
@@ -579,46 +584,47 @@ string(REPLACE ";" " " CVC4_DEFINITIONS "${CVC4_DEFINITIONS}")
 
 message("CVC4 ${CVC4_RELEASE_STRING}")
 message("")
-message("Build profile     : ${CVC4_BUILD_PROFILE_STRING}")
-message("Optimized         : ${ENABLE_OPTIMIZED}")
-message("Optimization level: ${OPTIMIZATION_LEVEL}")
-message("Debug symbols     : ${ENABLE_DEBUG_SYMBOLS}")
-message("Proofs            : ${ENABLE_PROOFS}")
-message("Statistics        : ${ENABLE_STATISTICS}")
-message("Replay            : ${ENABLE_REPLAY}")
-message("Assertions        : ${ENABLE_ASSERTIONS}")
-message("Tracing           : ${ENABLE_TRACING}")
-message("Dumping           : ${ENABLE_DUMPING}")
-message("Muzzle            : ${ENABLE_MUZZLE}")
+message("Build profile        : ${CVC4_BUILD_PROFILE_STRING}")
+message("Optimized            : ${ENABLE_OPTIMIZED}")
+message("Optimization level   : ${OPTIMIZATION_LEVEL}")
+message("Debug symbols        : ${ENABLE_DEBUG_SYMBOLS}")
+message("Debug context mem mgr: ${ENABLE_DEBUG_CONTEXT_MM}")
+message("Proofs               : ${ENABLE_PROOFS}")
+message("Statistics           : ${ENABLE_STATISTICS}")
+message("Replay               : ${ENABLE_REPLAY}")
+message("Assertions           : ${ENABLE_ASSERTIONS}")
+message("Tracing              : ${ENABLE_TRACING}")
+message("Dumping              : ${ENABLE_DUMPING}")
+message("Muzzle               : ${ENABLE_MUZZLE}")
 message("")
-message("Unit tests        : ${ENABLE_UNIT_TESTING}")
-message("Coverage (gcov)   : ${ENABLE_COVERAGE}")
-message("Profiling (gprof) : ${ENABLE_PROFILING}")
+message("Unit tests           : ${ENABLE_UNIT_TESTING}")
+message("Coverage (gcov)      : ${ENABLE_COVERAGE}")
+message("Profiling (gprof)    : ${ENABLE_PROFILING}")
 message("")
-message("Shared libs       : ${ENABLE_SHARED}")
+message("Shared libs          : ${ENABLE_SHARED}")
 #message("Static binary: ${enable_static_binary}")
 #message("Compat lib   : ${CVC4_BUILD_LIBCOMPAT}")
 #message("Bindings     : ${bindings_to_be_built}")
 #message("")
 #message("Multithreaded: ${support_multithreaded}")
-message("Portfolio         : ${ENABLE_PORTFOLIO}")
+message("Portfolio            : ${ENABLE_PORTFOLIO}")
 message("")
-message("ABC               : ${USE_ABC}")
-message("CaDiCaL           : ${USE_CADICAL}")
-message("CryptoMiniSat     : ${USE_CRYPTOMINISAT}")
-message("GLPK              : ${USE_GLPK}")
-message("LFSC              : ${USE_LFSC}")
+message("ABC                  : ${USE_ABC}")
+message("CaDiCaL              : ${USE_CADICAL}")
+message("CryptoMiniSat        : ${USE_CRYPTOMINISAT}")
+message("GLPK                 : ${USE_GLPK}")
+message("LFSC                 : ${USE_LFSC}")
 if(CVC4_USE_CLN_IMP)
-  message("MP library        : cln")
+  message("MP library           : cln")
 else()
-  message("MP library        : gmp")
+  message("MP library           : gmp")
 endif()
-message("Readline          : ${USE_READLINE}")
-message("SymFPU            : ${USE_SYMFPU}")
+message("Readline             : ${USE_READLINE}")
+message("SymFPU               : ${USE_SYMFPU}")
 message("")
-message("CPPLAGS (-D...)   : ${CVC4_DEFINITIONS}")
-message("CXXFLAGS          : ${CMAKE_CXX_FLAGS}")
-message("CFLAGS            : ${CMAKE_C_FLAGS}")
+message("CPPLAGS (-D...)      : ${CVC4_DEFINITIONS}")
+message("CXXFLAGS             : ${CMAKE_CXX_FLAGS}")
+message("CFLAGS               : ${CMAKE_C_FLAGS}")
 #message("LIBS         : ${LIBS}")
 #message("LDFLAGS      : ${LDFLAGS}")
 #message("")
@@ -627,7 +633,7 @@ message("CFLAGS            : ${CMAKE_C_FLAGS}")
 #message("libcvc4compat version  : ${CVC4_COMPAT_LIBRARY_VERSION_or_nobuild}")
 #message("libcvc4bindings version: ${CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild}")
 #message("")
-message("Install prefix    : ${CMAKE_INSTALL_PREFIX}")
+message("Install prefix       : ${CMAKE_INSTALL_PREFIX}")
 message("")
 
 if(GPL_LIBS)