google test: theory: Migrate sequences_rewriter_white. (#5975)
[cvc5.git] / CMakeLists.txt
index 7fc0af52ccc2a0dd7e2d780f1e15a053824da2ce..3dd282a8de6ec5e313e06485e41ed37d0c57b5ba 100644 (file)
@@ -1,10 +1,22 @@
-cmake_minimum_required(VERSION 3.4)
+#####################
+## CMakeLists.txt
+## Top contributors (to current version):
+##   Mathias Preiner, Aina Niemetz, Gereon Kremer
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
+## All rights reserved.  See the file COPYING in the top-level source
+## directory for licensing information.
+##
+cmake_minimum_required(VERSION 3.9)
 
 #-----------------------------------------------------------------------------#
 # Project configuration
 
 project(cvc4)
 
+include(GNUInstallDirs)
+
 set(CVC4_MAJOR   1) # Major component of the version of CVC4.
 set(CVC4_MINOR   9) # Minor component of the version of CVC4.
 set(CVC4_RELEASE 0) # Release component of the version of CVC4.
@@ -25,8 +37,9 @@ endif()
 
 set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
 set(CMAKE_C_STANDARD 99)
-set(CMAKE_CXX_STANDARD 11)
+set(CMAKE_CXX_STANDARD 17)
 set(CMAKE_CXX_EXTENSIONS OFF)
+set(CMAKE_CXX_STANDARD_REQUIRED ON)
 
 # Generate compile_commands.json, which can be used for various code completion
 # plugins.
@@ -85,12 +98,6 @@ list(APPEND CMAKE_PREFIX_PATH "${PROJECT_SOURCE_DIR}/deps/install")
 
 #-----------------------------------------------------------------------------#
 
-set(INCLUDE_INSTALL_DIR include)
-set(LIBRARY_INSTALL_DIR lib)
-set(RUNTIME_INSTALL_DIR bin)
-
-#-----------------------------------------------------------------------------#
-
 include(Helpers)
 
 #-----------------------------------------------------------------------------#
@@ -146,8 +153,7 @@ option(USE_DRAT2ER            "Include drat2er for making eager BV proofs")
 option(USE_LFSC               "Use LFSC proof checker")
 option(USE_POLY               "Use LibPoly for polynomial arithmetic")
 option(USE_SYMFPU             "Use SymFPU for floating point support")
-option(USE_PYTHON2            "Prefer using Python 2 (for Python bindings)")
-option(USE_PYTHON3            "Prefer using Python 3 (for Python bindings)")
+option(USE_PYTHON2            "Force Python 2 (deprecated)")
 
 # Custom install directories for dependencies
 # If no directory is provided by the user, we first check if the dependency was
@@ -174,6 +180,9 @@ set(PROGRAM_PREFIX    "" CACHE STRING "Program prefix on make install")
 option(BUILD_BINDINGS_PYTHON "Build Python bindings based on new C++ API ")
 option(BUILD_BINDINGS_JAVA "Build Java bindings based on new C++ API ")
 
+# Build limitations
+option(BUILD_LIB_ONLY         "Only build the library")
+
 #-----------------------------------------------------------------------------#
 # Internal cmake variables
 
@@ -280,6 +289,7 @@ endif()
 # Only enable unit testing if assertions are enabled. Otherwise, unit tests
 # that expect AssertionException to be thrown will fail.
 if(NOT ENABLE_ASSERTIONS)
+  message(WARNING "Disabling unit tests since assertions are disabled.")
   set(ENABLE_UNIT_TESTING OFF)
 endif()
 
@@ -312,9 +322,14 @@ if(ENABLE_SHARED)
   #
   # More information on RPATH in CMake:
   # https://gitlab.kitware.com/cmake/community/wikis/doc/cmake/RPATH-handling
-  set(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/${LIBRARY_INSTALL_DIR};${PROJECT_SOURCE_DIR}/deps/install/lib")
+  set(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR};${PROJECT_SOURCE_DIR}/deps/install/lib")
 else()
-  set(CMAKE_FIND_LIBRARY_SUFFIXES .a ${CMAKE_FIND_LIBRARY_SUFFIXES})
+  # When building statically, we *only* want static archives/libraries
+  if (WIN32)
+      set(CMAKE_FIND_LIBRARY_SUFFIXES .lib .a)
+  else()
+      set(CMAKE_FIND_LIBRARY_SUFFIXES .a)
+  endif()
   set(BUILD_SHARED_LIBS OFF)
   cvc4_set_option(ENABLE_STATIC_BINARY ON)
 
@@ -324,6 +339,11 @@ else()
     message(WARNING "Disabling unit tests since static build is enabled.")
     set(ENABLE_UNIT_TESTING OFF)
   endif()
+
+  if (BUILD_BINDINGS_PYTHON)
+    message(FATAL_ERROR "Building Python bindings is not possible "
+                        "when building statically")
+  endif()
 endif()
 
 #-----------------------------------------------------------------------------#
@@ -356,10 +376,8 @@ endif()
 
 if(USE_PYTHON2)
   find_package(PythonInterp 2.7 REQUIRED)
-elseif(USE_PYTHON3)
-  find_package(PythonInterp 3 REQUIRED)
 else()
-  find_package(PythonInterp REQUIRED)
+  find_package(PythonInterp REQUIRED)
 endif()
 
 find_package(GMP REQUIRED)
@@ -543,7 +561,11 @@ endif()
 # Generate CVC4's cvc4autoconfig.h header
 
 include(ConfigureCVC4)
+if(NOT ENABLE_SHARED)
+  set(CVC4_STATIC_BUILD ON)
+endif()
 configure_file(cvc4autoconfig.h.in cvc4autoconfig.h)
+unset(CVC4_STATIC_BUILD)
 include_directories(${CMAKE_CURRENT_BINARY_DIR})
 
 #-----------------------------------------------------------------------------#
@@ -559,6 +581,7 @@ add_subdirectory(src)
 add_subdirectory(test)
 
 if(BUILD_BINDINGS_PYTHON)
+  set(BUILD_BINDINGS_PYTHON_VERSION ${PYTHON_VERSION_MAJOR})
   add_subdirectory(src/api/python)
 endif()
 
@@ -623,13 +646,13 @@ endif()
 install(EXPORT cvc4-targets
   FILE CVC4Targets.cmake
   NAMESPACE CVC4::
-  DESTINATION ${LIBRARY_INSTALL_DIR}/cmake/CVC4)
+  DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/CVC4)
 
 configure_package_config_file(
   ${CMAKE_SOURCE_DIR}/cmake/CVC4Config.cmake.in
   ${CMAKE_BINARY_DIR}/cmake/CVC4Config.cmake
-  INSTALL_DESTINATION ${LIBRARY_INSTALL_DIR}/cmake/CVC4
-  PATH_VARS LIBRARY_INSTALL_DIR
+  INSTALL_DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/CVC4
+  PATH_VARS CMAKE_INSTALL_LIBDIR
 )
 
 write_basic_package_version_file(
@@ -641,7 +664,7 @@ write_basic_package_version_file(
 install(FILES
   ${CMAKE_BINARY_DIR}/cmake/CVC4Config.cmake
   ${CMAKE_BINARY_DIR}/CVC4ConfigVersion.cmake
-  DESTINATION ${LIBRARY_INSTALL_DIR}/cmake/CVC4
+  DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/CVC4
 )
 
 
@@ -690,7 +713,6 @@ print_config("Static binary             :" ENABLE_STATIC_BINARY)
 print_config("Python bindings           :" BUILD_BINDINGS_PYTHON)
 print_config("Java bindings             :" BUILD_BINDINGS_JAVA)
 print_config("Python2                   :" USE_PYTHON2)
-print_config("Python3                   :" USE_PYTHON3)
 message("")
 print_config("ABC                       :" USE_ABC)
 print_config("CaDiCaL                   :" USE_CADICAL)
@@ -700,6 +722,8 @@ print_config("GLPK                      :" USE_GLPK)
 print_config("Kissat                    :" USE_KISSAT)
 print_config("LFSC                      :" USE_LFSC)
 print_config("LibPoly                   :" USE_POLY)
+message("")
+print_config("BUILD_LIB_ONLY            :" BUILD_LIB_ONLY)
 
 if(CVC4_USE_CLN_IMP)
   message("MP library                : cln")
@@ -753,7 +777,7 @@ message("")
 
 if(GPL_LIBS)
   message(
-  "CVC4 license             : GPLv3 (due to optional libraries; see below)"
+  "CVC4 license             : ${Yellow}GPLv3 (due to optional libraries; see below)${ResetColor}"
   "\n"
   "\n"
   "Please note that CVC4 will be built against the following GPLed libraries:"