cmake: Build fully static binaries with option --static.

13 files changed, 148 insertions, 55 deletions

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 011ff2fe5..b733b65d1 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -173,15 +173,31 @@ if(ENABLE_BEST)
   cvc4_set_option(USE_READLINE ON)
 endif()
 
-#-----------------------------------------------------------------------------#
-# Static libraries
+# Only enable unit testing if assertions are enabled. Otherwise, unit tests
+# that expect AssertionException to be thrown will fail.
+if(NOT ENABLE_ASSERTIONS)
+  set(ENABLE_UNIT_TESTING OFF)
+endif()
+
+# Never build unit tests as static binaries, otherwise we'll end up with
+# ~300MB per unit test.
+if(ENABLE_UNIT_TESTING)
+  set(ENABLE_SHARED ON)
+endif()
 
+#-----------------------------------------------------------------------------#
+# Shared/static libraries
+#
 # This needs to be set before any find_package(...) command since we want to
 # search for static libraries with suffix .a.
-if(NOT ENABLE_SHARED)
-  set(CMAKE_FIND_LIBRARY_SUFFIXES ".a")
-  set(CMAKE_EXE_LINKER_FLAGS "-static")
+
+if(ENABLE_SHARED)
+  set(BUILD_SHARED_LIBS ON)
+else()
+  set(CMAKE_FIND_LIBRARY_SUFFIXES ".a ${CMAKE_FIND_LIBRARY_SUFFIXES}")
   set(BUILD_SHARED_LIBS OFF)
+  # This is required to force find_package(Boost) to use static libraries.
+  set(Boost_USE_STATIC_LIBS ON)
 endif()
 
 #-----------------------------------------------------------------------------#
@@ -203,8 +219,6 @@ endif()
 
 set(GMP_HOME ${GMP_DIR})
 find_package(GMP REQUIRED)
-libcvc4_link_libraries(${GMP_LIBRARIES})
-libcvc4_include_directories(${GMP_INCLUDE_DIR})
 
 if(ENABLE_ASAN)
   # -fsanitize=address requires CMAKE_REQUIRED_FLAGS to be explicitely set,
@@ -220,9 +234,6 @@ if(ENABLE_ASSERTIONS)
   add_definitions(-DCVC4_ASSERTIONS)
 else()
   add_definitions(-DNDEBUG)
-  # Only enable unit testing if assertions are enabled. Otherwise, unit tests
-  # that expect AssertionException to be thrown will fail.
-  set(ENABLE_UNIT_TESTING OFF)
 endif()
 
 if(ENABLE_COVERAGE)
@@ -293,13 +304,6 @@ endif()
 
 if(ENABLE_UNIT_TESTING)
   find_package(CxxTest REQUIRED)
-  # Force shared libs for unit tests, static libs with unit tests are not
-  # working right now.
-  set(ENABLE_SHARED ON)
-endif()
-
-if(ENABLE_SHARED)
-  set(BUILD_SHARED_LIBS ON)
 endif()
 
 if(ENABLE_STATISTICS)
@@ -308,31 +312,24 @@ endif()
 
 if(ENABLE_VALGRIND)
   find_package(Valgrind REQUIRED)
-  libcvc4_include_directories(${Valgrind_INCLUDE_DIR})
   add_definitions(-DCVC4_VALGRIND)
 endif()
 
 if(USE_ABC)
   set(ABC_HOME "${ABC_DIR}")
   find_package(ABC REQUIRED)
-  libcvc4_link_libraries(${ABC_LIBRARIES})
-  libcvc4_include_directories(${ABC_INCLUDE_DIR})
   add_definitions(-DCVC4_USE_ABC ${ABC_ARCH_FLAGS})
 endif()
 
 if(USE_CADICAL)
   set(CaDiCaL_HOME ${CADICAL_DIR})
   find_package(CaDiCaL REQUIRED)
-  libcvc4_link_libraries(${CaDiCaL_LIBRARIES})
-  libcvc4_include_directories(${CaDiCaL_INCLUDE_DIR})
   add_definitions(-DCVC4_USE_CADICAL)
 endif()
 
 if(USE_CLN)
   set(GPL_LIBS "${GPL_LIBS} cln")
   find_package(CLN 1.2.2 REQUIRED)
-  libcvc4_link_libraries(${CLN_LIBRARIES})
-  libcvc4_include_directories(${CLN_INCLUDE_DIR})
   set(CVC4_USE_CLN_IMP 1)
   set(CVC4_USE_GMP_IMP 0)
 else()
@@ -349,8 +346,6 @@ if(USE_CRYPTOMINISAT)
   endif()
   set(CryptoMiniSat_HOME ${CRYPTOMINISAT_DIR})
   find_package(CryptoMiniSat REQUIRED)
-  libcvc4_link_libraries(${CryptoMiniSat_LIBRARIES})
-  libcvc4_include_directories(${CryptoMiniSat_INCLUDE_DIR})
   add_definitions(-DCVC4_USE_CRYPTOMINISAT)
 endif()
 
@@ -358,8 +353,6 @@ if(USE_GLPK)
   set(GPL_LIBS "${GPL_LIBS} glpk")
   set(GLPK_HOME ${GLPK_DIR})
   find_package(GLPK REQUIRED)
-  libcvc4_link_libraries(${GLPK_LIBRARIES})
-  libcvc4_include_directories(${GLPK_INCLUDE_DIR})
   add_definitions(-DCVC4_USE_GLPK)
 endif()
 
@@ -367,8 +360,6 @@ if(USE_LFSC)
   set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc)
   set(LFSC_HOME ${LFSC_DIR})
   find_package(LFSC REQUIRED)
-  libcvc4_link_libraries(${LFSC_LIBRARIES})
-  libcvc4_include_directories(${LFSC_INCLUDE_DIR})
   add_definitions(-DCVC4_USE_LFSC)
 endif()
 
@@ -384,7 +375,6 @@ endif()
 if(USE_SYMFPU)
   set(SymFPU_HOME ${SYMFPU_DIR})
   find_package(SymFPU REQUIRED)
-  libcvc4_include_directories(${SymFPU_INCLUDE_DIR})
   add_definitions(-DCVC4_USE_SYMFPU)
   set(CVC4_USE_SYMFPU 1)
 else()
diff --git a/cmake/FindABC.cmake b/cmake/FindABC.cmake
index 0a9cea950..c44019739 100644
--- a/cmake/FindABC.cmake
+++ b/cmake/FindABC.cmake
@@ -36,3 +36,6 @@ find_package_handle_standard_args(ABC
   ABC_INCLUDE_DIR ABC_LIBRARIES ABC_ARCH_FLAGS)
 
 mark_as_advanced(ABC_INCLUDE_DIR ABC_LIBRARIES ABC_ARCH_FLAGS)
+if(ABC_LIBRARIES)
+  message(STATUS "Found ABC libs: ${ABC_LIBRARIES}")
+endif()
diff --git a/cmake/FindANTLR.cmake b/cmake/FindANTLR.cmake
index 135668006..5f574247b 100644
--- a/cmake/FindANTLR.cmake
+++ b/cmake/FindANTLR.cmake
@@ -48,3 +48,6 @@ find_package_handle_standard_args(
 
 mark_as_advanced(ANTLR_BINARY ANTLR_INCLUDE_DIR ANTLR_LIBRARIES
                  HAVE_ANTLR3_FILE_STREAM_NEW)
+if(ANTLR_LIBRARIES)
+  message(STATUS "Found ANTLR libs: ${ANTLR_LIBRARIES}")
+endif()
diff --git a/cmake/FindCLN.cmake b/cmake/FindCLN.cmake
index 2cb33eb7e..7b2e6f0f4 100644
--- a/cmake/FindCLN.cmake
+++ b/cmake/FindCLN.cmake
@@ -25,3 +25,6 @@ if(CLN_INCLUDE_DIR)
     VERSION_VAR CLN_VERSION)
   mark_as_advanced(CLN_INCLUDE_DIR CLN_LIBRARIES)
 endif()
+if(CLN_LIBRARIES)
+  message(STATUS "Found CLN libs: ${CLN_LIBRARIES}")
+endif()
diff --git a/cmake/FindCaDiCaL.cmake b/cmake/FindCaDiCaL.cmake
index 2976bb2bb..bd7de319a 100644
--- a/cmake/FindCaDiCaL.cmake
+++ b/cmake/FindCaDiCaL.cmake
@@ -32,3 +32,6 @@ find_package_handle_standard_args(CaDiCaL
   CaDiCaL_INCLUDE_DIR CaDiCaL_LIBRARIES)
 
 mark_as_advanced(CaDiCaL_INCLUDE_DIR CaDiCaL_LIBRARIES)
+if(CaDiCaL_LIBRARIES)
+  message(STATUS "Found CaDiCaL libs: ${CaDiCaL_LIBRARIES}")
+endif()
diff --git a/cmake/FindCryptoMiniSat.cmake b/cmake/FindCryptoMiniSat.cmake
index aecd92226..7806b242d 100644
--- a/cmake/FindCryptoMiniSat.cmake
+++ b/cmake/FindCryptoMiniSat.cmake
@@ -32,3 +32,6 @@ find_package_handle_standard_args(CryptoMiniSat
   CryptoMiniSat_INCLUDE_DIR CryptoMiniSat_LIBRARIES)
 
 mark_as_advanced(CryptoMiniSat_INCLUDE_DIR CryptoMiniSat_LIBRARIES)
+if(CryptoMiniSat_LIBRARIES)
+  message(STATUS "Found CryptoMiniSat libs: ${CryptoMiniSat_LIBRARIES}")
+endif()
diff --git a/cmake/FindGLPK.cmake b/cmake/FindGLPK.cmake
index e2b07faff..1587ca821 100644
--- a/cmake/FindGLPK.cmake
+++ b/cmake/FindGLPK.cmake
@@ -44,3 +44,6 @@ find_package_handle_standard_args(GLPK
   GLPK_INCLUDE_DIR GLPK_LIBRARIES)
 
 mark_as_advanced(GLPK_INCLUDE_DIR GLPK_LIBRARIES)
+if(GLPK_LIBRARIES)
+  message(STATUS "Found GLPK libs: ${GLPK_LIBRARIES}")
+endif()
diff --git a/cmake/FindGMP.cmake b/cmake/FindGMP.cmake
index a835e2d5e..8125a583b 100644
--- a/cmake/FindGMP.cmake
+++ b/cmake/FindGMP.cmake
@@ -30,3 +30,6 @@ include(FindPackageHandleStandardArgs)
 find_package_handle_standard_args(GMP DEFAULT_MSG GMP_INCLUDE_DIR GMP_LIBRARIES)
 
 mark_as_advanced(GMP_INCLUDE_DIR GMP_LIBRARIES)
+if(GMP_LIBRARIES)
+  message(STATUS "Found GMP libs: ${GMP_LIBRARIES}")
+endif()
diff --git a/cmake/FindLFSC.cmake b/cmake/FindLFSC.cmake
index 2e3118669..7a666839b 100644
--- a/cmake/FindLFSC.cmake
+++ b/cmake/FindLFSC.cmake
@@ -32,3 +32,6 @@ find_package_handle_standard_args(LFSC
   LFSC_INCLUDE_DIR LFSC_LIBRARIES)
 
 mark_as_advanced(LFSC_INCLUDE_DIR LFSC_LIBRARIES)
+if(LFSC_LIBRARIES)
+  message(STATUS "Found LFSC libs: ${LFSC_LIBRARIES}")
+endif()
diff --git a/cmake/FindReadline.cmake b/cmake/FindReadline.cmake
index 16dd72236..edac03027 100644
--- a/cmake/FindReadline.cmake
+++ b/cmake/FindReadline.cmake
@@ -8,12 +8,43 @@
 find_path(Readline_INCLUDE_DIR NAMES readline/readline.h)
 find_library(Readline_LIBRARIES NAMES readline)
 
-# Check which standard of readline is installed on the system.
-# https://github.com/CVC4/CVC4/issues/702
+# Try to compile and link a simple program against readline. 'libs' can be
+# used to specify additional required libraries.
+function(try_compile_readline libs _result)
+  set(CMAKE_REQUIRED_QUIET TRUE)
+  set(CMAKE_REQUIRED_LIBRARIES ${Readline_LIBRARIES} ${libs})
+  check_cxx_source_compiles(
+    "
+    #include <stdio.h>
+    #include <readline/readline.h>
+    int main() { readline(\"\"); return 0; }
+    "
+    ${_result}
+  )
+  set(${_result} ${${_result}} PARENT_SCOPE)
+endfunction()
+
 if(Readline_INCLUDE_DIR)
+  # We only need to figure out readline's additional libraries dependencies if
+  # we compile static.
+  # Note: It might be the case that we need to check for more/other libraries
+  # depending on what the installed version of readline is linked against
+  # (e.g., termcap, ncurses, ...).
+    find_library(TINFO_LIBRARY tinfo)
+    try_compile_readline(${TINFO_LIBRARY} OK)
+    if(OK)
+      list(APPEND Readline_LIBRARIES ${TINFO_LIBRARY})
+    else()
+      message(FATAL_ERROR
+              "Could not link against readline. "
+              "Check CMakeError.log for more details")
+    endif()
+
+  # Check which standard of readline is installed on the system.
+  # https://github.com/CVC4/CVC4/issues/702
   include(CheckCXXSourceCompiles)
   set(CMAKE_REQUIRED_QUIET TRUE)
-  set(CMAKE_REQUIRED_LIBRARIES readline)
+  set(CMAKE_REQUIRED_LIBRARIES ${Readline_LIBRARIES})
   check_cxx_source_compiles(
     "#include <stdio.h>
      #include <readline/readline.h>
@@ -33,3 +64,6 @@ mark_as_advanced(
   Readline_LIBRARIES
   Readline_COMPENTRY_FUNC_RETURNS_CHARPTR
 )
+if(Readline_LIBRARIES)
+  message(STATUS "Found Readline libs: ${Readline_LIBRARIES}")
+endif()
diff --git a/cmake/Helpers.cmake b/cmake/Helpers.cmake
index ec7216452..692e32900 100644
--- a/cmake/Helpers.cmake
+++ b/cmake/Helpers.cmake
@@ -120,21 +120,6 @@ macro(print_config str var)
 endmacro()
 
 
-#-----------------------------------------------------------------------------#
-# libcvc4 helper macros
-
-# Collect all libraries that must be linked against libcvc4. These will be
-# actually linked in src/CMakeLists.txt with target_link_libaries(...).
-macro(libcvc4_link_libraries library)
-  set(LIBCVC4_LIBRARIES ${LIBCVC4_LIBRARIES} ${library})
-endmacro()
-
-# Collect all include directories that are required for libcvc4. These will be
-# actually included in src/CMakeLists.txt with target_include_directories(...).
-macro(libcvc4_include_directories dirs)
-  set(LIBCVC4_INCLUDES ${LIBCVC4_INCLUDES} ${dirs})
-endmacro()
-
 # Collect all source files that are required to build libcvc4 in LIBCVC4_SRCS
 # or LIBCVC4_GEN_SRCS. If GENERATED is the first argument the sources are
 # added to LIBCVC4_GEN_SRCS. All sources are prepended with the absolute
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 3e32ab7bf..96d462d96 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -660,7 +660,6 @@ include_directories(. ${CMAKE_CURRENT_BINARY_DIR})
 
 add_subdirectory(base)
 add_subdirectory(expr)
-add_subdirectory(main)
 add_subdirectory(options)
 add_subdirectory(parser)
 add_subdirectory(theory)
@@ -672,6 +671,7 @@ add_subdirectory(util)
 
 set_source_files_properties(${LIBCVC4_GEN_SRCS} PROPERTIES GENERATED TRUE)
 add_library(cvc4 ${LIBCVC4_SRCS} ${LIBCVC4_GEN_SRCS})
+install(TARGETS cvc4 DESTINATION lib)
 
 set_target_properties(cvc4 PROPERTIES SOVERSION ${CVC4_SOVERSION})
 target_compile_definitions(cvc4
@@ -682,10 +682,53 @@ target_compile_definitions(cvc4
 )
 # Add libcvc4 dependencies for generated sources.
 add_dependencies(cvc4 gen-expr gen-options gen-tags gen-theory)
-target_link_libraries(cvc4 ${LIBCVC4_LIBRARIES})
-target_include_directories(cvc4 PUBLIC ${LIBCVC4_INCLUDES})
-install(TARGETS cvc4 DESTINATION lib)
 
+# Add library/include dependencies
+if(ENABLE_VALGRIND)
+  target_include_directories(cvc4 PUBLIC ${Valgrind_INCLUDE_DIR})
+endif()
+if(USE_ABC)
+  target_link_libraries(cvc4 ${ABC_LIBRARIES})
+  target_include_directories(cvc4 PUBLIC ${ABC_INCLUDE_DIR})
+endif()
+if(USE_CADICAL)
+  target_link_libraries(cvc4 ${CaDiCaL_LIBRARIES})
+  target_include_directories(cvc4 PUBLIC ${CaDiCaL_INCLUDE_DIR})
+endif()
+if(USE_CLN)
+  target_link_libraries(cvc4 ${CLN_LIBRARIES})
+  target_include_directories(cvc4 PUBLIC ${CLN_INCLUDE_DIR})
+endif()
+if(USE_CRYPTOMINISAT)
+  target_link_libraries(cvc4 ${CryptoMiniSat_LIBRARIES})
+  target_include_directories(cvc4 PUBLIC ${CryptoMiniSat_INCLUDE_DIR})
+endif()
+if(USE_GLPK)
+  target_link_libraries(cvc4 ${GLPK_LIBRARIES})
+  target_include_directories(cvc4 PUBLIC ${GLPK_INCLUDE_DIR})
+endif()
+if(USE_LFSC)
+  target_link_libraries(cvc4 ${LFSC_LIBRARIES})
+  target_include_directories(cvc4 PUBLIC ${LFSC_INCLUDE_DIR})
+endif()
+if(USE_SYMFPU)
+  target_include_directories(cvc4 PUBLIC ${SymFPU_INCLUDE_DIR})
+endif()
+
+# Note: When linked statically GMP needs to be linked after CLN since CLN
+# depends on GMP.
+target_link_libraries(cvc4 ${GMP_LIBRARIES})
+target_include_directories(cvc4 PUBLIC ${GMP_INCLUDE_DIR})
+
+#-----------------------------------------------------------------------------#
+# Visit main subdirectory after creating target cvc4. For target main, we have
+# to manually add library dependencies since we can't use
+# target_link_libraries(...) with object libraries for cmake versions <= 3.12.
+# Thus, we can only visit main as soon as all dependencies for cvc4 are set up.
+
+add_subdirectory(main)
+
+#-----------------------------------------------------------------------------#
 # Note:
 # We define all install commands for all public headers here in one
 # place so that we can easily remove them as soon as we enforce the new
diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
index 39c4b2779..30a246ba0 100644
--- a/src/main/CMakeLists.txt
+++ b/src/main/CMakeLists.txt
@@ -16,8 +16,8 @@ set(libmain_src_files
 
 add_library(main OBJECT ${libmain_src_files})
 target_compile_definitions(main PRIVATE -D__BUILDING_CVC4DRIVER)
-if(BUILD_SHARED_LIBS)
-  set_target_properties(main PROPERTIES POSITION_INDEPENDENT_CODE 1)
+if(ENABLE_SHARED)
+  set_target_properties(main PROPERTIES POSITION_INDEPENDENT_CODE ON)
 endif()
 
 # We can't use target_link_libraries(...) here since this is only supported for
@@ -26,6 +26,7 @@ endif()
 # dependencies are not propagated and we need to manually add the include
 # directories of libcvc4 to main.
 add_dependencies(main cvc4 cvc4parser gen-tokens)
+get_target_property(LIBCVC4_INCLUDES cvc4 INCLUDE_DIRECTORIES)
 target_include_directories(main PRIVATE ${LIBCVC4_INCLUDES})
 
 # main-test library is only used for linking against system and unit tests so
@@ -46,6 +47,16 @@ set_target_properties(cvc4-bin
 target_link_libraries(cvc4-bin cvc4 cvc4parser)
 install(TARGETS cvc4-bin DESTINATION bin)
 
+# In order to get a fully static executable we have to make sure that we also
+# use the static system libraries.
+#   https://cmake.org/cmake/help/v3.0/prop_tgt/LINK_SEARCH_START_STATIC.html
+#   https://cmake.org/cmake/help/v3.0/prop_tgt/LINK_SEARCH_END_STATIC.html
+if(NOT ENABLE_SHARED)
+  set_target_properties(cvc4-bin PROPERTIES LINK_FLAGS -static)
+  set_target_properties(cvc4-bin PROPERTIES LINK_SEARCH_START_STATIC ON)
+  set_target_properties(cvc4-bin PROPERTIES LINK_SEARCH_END_STATIC ON)
+endif()
+
 if(ENABLE_PORTFOLIO)
   set(pcvc4_src_files
     main.cpp
@@ -66,6 +77,12 @@ if(ENABLE_PORTFOLIO)
   target_link_libraries(pcvc4-bin cvc4 cvc4parser ${Boost_LIBRARIES})
   target_include_directories(pcvc4-bin PRIVATE ${Boost_INCLUDE_DIRS})
   install(TARGETS pcvc4-bin DESTINATION bin)
+
+  if(NOT ENABLE_SHARED)
+    set_target_properties(pcvc4-bin PROPERTIES LINK_FLAGS -static)
+    set_target_properties(pcvc4-bin PROPERTIES LINK_SEARCH_START_STATIC ON)
+    set_target_properties(pcvc4-bin PROPERTIES LINK_SEARCH_END_STATIC ON)
+  endif()
 endif()
 
 if(USE_READLINE)