Fix trivial explantions in sequences array solver (#7973)

[cvc5.git] / CMakeLists.txt

diff --git a/CMakeLists.txt b/CMakeLists.txt
index f7ff3bac38d57cef0f093a4854215680884f1e39..ac654957ad86cdf83282e132cc98c54882f4a689 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -78,7 +78,6 @@ cvc5_option(ENABLE_ASSERTIONS     "Enable assertions")
 cvc5_option(ENABLE_COMP_INC_TRACK
             "Enable optimizations for incremental SMT-COMP tracks")
 cvc5_option(ENABLE_DEBUG_SYMBOLS  "Enable debug symbols")
-cvc5_option(ENABLE_DUMPING        "Enable dumping")
 cvc5_option(ENABLE_MUZZLE         "Suppress ALL non-result output")
 cvc5_option(ENABLE_STATISTICS     "Enable statistics")
 cvc5_option(ENABLE_TRACING        "Enable tracing")
@@ -126,6 +125,10 @@ option(BUILD_BINDINGS_JAVA "Build Java bindings based on new C++ API ")
 # Api documentation
 option(BUILD_DOCS "Build Api documentation")
 
+# Link against static system libraries
+cvc5_option(STATIC_BINARY "Link against static system libraries \
+(enabled by default for static builds)")
+
 #-----------------------------------------------------------------------------#
 # Internal cmake variables
 
@@ -247,10 +250,22 @@ endif()
 # https://gitlab.kitware.com/cmake/community/wikis/doc/cmake/RPATH-handling
 set(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR};${PROJECT_SOURCE_DIR}/deps/install/lib")
 
-# Set visibility to default if unit tests are enabled
+# Set visibility to default if unit tests are enabled. If unit tests are
+# enabled, we also check if we can execute white box unit tests (some versions
+# of Clang have issues with the required flag).
+set(ENABLE_WHITEBOX_UNIT_TESTING OFF)
 if(ENABLE_UNIT_TESTING)
   set(CMAKE_CXX_VISIBILITY_PRESET default)
   set(CMAKE_VISIBILITY_INLINES_HIDDEN 0)
+
+  # Check if Clang version has the bug that was fixed in
+  # https://reviews.llvm.org/D93104
+  set(ENABLE_WHITEBOX_UNIT_TESTING ON)
+  check_cxx_compiler_flag("-faccess-control" HAVE_CXX_FLAGfaccess_control)
+  if(NOT HAVE_CXX_FLAGfaccess_control)
+    set(ENABLE_WHITEBOX_UNIT_TESTING OFF)
+    message(STATUS "Disabling white box unit tests")
+  endif()
 endif()
 
 #-----------------------------------------------------------------------------#
@@ -342,10 +357,6 @@ if(ENABLE_MUZZLE)
   add_definitions(-DCVC5_MUZZLE)
 endif()
 
-if(ENABLE_DUMPING)
-  add_definitions(-DCVC5_DUMPING)
-endif()
-
 if(ENABLE_PROFILING)
   add_definitions(-DCVC5_PROFILING)
   add_check_c_cxx_flag("-pg")
@@ -443,6 +454,9 @@ if(BUILD_SHARED_LIBS)
   set(CVC5_STATIC_BUILD OFF)
 else()
   set(CVC5_STATIC_BUILD ON)
+  if(NOT CMAKE_SYSTEM_NAME STREQUAL "Darwin")
+    cvc5_set_option(STATIC_BINARY ON)
+  endif()
 endif()
 
 #-----------------------------------------------------------------------------#
@@ -461,7 +475,6 @@ endif()
 
 if(BUILD_BINDINGS_JAVA)
   add_subdirectory(src/api/java)
-  message(WARNING "Java API is currently under development.")
 endif()
 
 if(BUILD_DOCS)
@@ -584,7 +597,6 @@ print_config("Assertions                " ${ENABLE_ASSERTIONS})
 print_config("Debug symbols             " ${ENABLE_DEBUG_SYMBOLS})
 print_config("Debug context mem mgr     " ${ENABLE_DEBUG_CONTEXT_MM})
 message("")
-print_config("Dumping                   " ${ENABLE_DUMPING})
 print_config("Muzzle                    " ${ENABLE_MUZZLE})
 print_config("Statistics                " ${ENABLE_STATISTICS})
 print_config("Tracing                   " ${ENABLE_TRACING})