cmake: Use target specific includes for libcvc4.

Further, print definitions added with add_definitions(...).

1 files changed, 56 insertions, 28 deletions

diff --git a/CMakeLists.txt b/CMakeLists.txt
index aa91a631f..47934d05f 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -49,12 +49,20 @@ include(CheckCCompilerFlag)
 include(CheckCXXCompilerFlag)
 
 macro(add_c_flag flag)
-  set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${flag}")
+  if(CMAKE_C_FLAGS)
+    set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${flag}")
+  else()
+    set(CMAKE_C_FLAGS "${flag}")
+  endif()
   message(STATUS "Configuring with C flag '${flag}'")
 endmacro()
 
 macro(add_cxx_flag flag)
-  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flag}")
+  if(CMAKE_CXX_FLAGS)
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flag}")
+  else()
+    set(CMAKE_CXX_FLAGS "${flag}")
+  endif()
   message(STATUS "Configuring with CXX flag '${flag}'")
 endmacro()
 
@@ -107,16 +115,31 @@ macro(add_required_c_cxx_flag flag)
   add_required_cxx_flag(${flag})
 endmacro()
 
-macro(cvc4_link_library library)
-  set(CVC4_LIBRARIES ${CVC4_LIBRARIES} ${library})
+# 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()
 
+# CVC4 Boolean options are three-valued to detect if an option was set by the
+# user. The available values are: IGNORE (default), ON, OFF
+# Default options do not override options that were set by the user, i.e.,
+# cvc4_set_option only sets an option if it's value is still IGNORE.
+# This e.g., allows the user to disable proofs for debug builds (where proofs
+# are enabled by default).
 macro(cvc4_option var description)
   set(${var} IGNORE CACHE STRING "${description}")
   # Provide drop down menu options in cmake-gui
   set_property(CACHE ${var} PROPERTY STRINGS IGNORE ON OFF)
 endmacro()
 
+# Only set option if the user did not set an option.
 macro(cvc4_set_option var value)
   if(${var} STREQUAL "IGNORE")
     set(${var} ${value})
@@ -263,8 +286,8 @@ find_package(ANTLR REQUIRED)
 
 set(GMP_HOME ${GMP_DIR})
 find_package(GMP REQUIRED)
-cvc4_link_library(${GMP_LIBRARIES})
-include_directories(${GMP_INCLUDE_DIR})
+libcvc4_link_libraries(${GMP_LIBRARIES})
+libcvc4_include_directories(${GMP_INCLUDE_DIR})
 
 
 #-----------------------------------------------------------------------------#
@@ -336,6 +359,7 @@ if(ENABLE_PROOFS)
   set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --enable-proof)
   add_definitions(-DCVC4_PROOF)
   set(CVC4_PROOF 1)
+  libcvc4_link_libraries(signatures)
 endif()
 
 if(ENABLE_REPLAY)
@@ -370,24 +394,24 @@ endif()
 if(USE_ABC)
   set(ABC_HOME "${ABC_DIR}")
   find_package(ABC REQUIRED)
-  cvc4_link_library(${ABC_LIBRARIES})
-  include_directories(${ABC_INCLUDE_DIR})
+  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)
-  cvc4_link_library(${CaDiCaL_LIBRARIES})
-  include_directories(${CaDiCaL_INCLUDE_DIR})
+  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)
-  cvc4_link_library(${CLN_LIBRARIES})
-  include_directories(${CLN_INCLUDE_DIR})
+  libcvc4_link_libraries(${CLN_LIBRARIES})
+  libcvc4_include_directories(${CLN_INCLUDE_DIR})
   set(CVC4_USE_CLN_IMP 1)
   set(CVC4_USE_GMP_IMP 0)
 else()
@@ -404,8 +428,8 @@ if(USE_CRYPTOMINISAT)
   endif()
   set(CryptoMiniSat_HOME ${CRYPTOMINISAT_DIR})
   find_package(CryptoMiniSat REQUIRED)
-  cvc4_link_library(${CryptoMiniSat_LIBRARIES})
-  include_directories(${CryptoMiniSat_INCLUDE_DIR})
+  libcvc4_link_libraries(${CryptoMiniSat_LIBRARIES})
+  libcvc4_include_directories(${CryptoMiniSat_INCLUDE_DIR})
   add_definitions(-DCVC4_USE_CRYPTOMINISAT)
 endif()
 
@@ -413,8 +437,8 @@ if(USE_GLPK)
   set(GPL_LIBS "${GPL_LIBS} glpk")
   set(GLPK_HOME ${GLPK_DIR})
   find_package(GLPK REQUIRED)
-  cvc4_link_library(${GLPK_LIBRARIES})
-  include_directories(${GLPK_INCLUDE_DIR})
+  libcvc4_link_libraries(${GLPK_LIBRARIES})
+  libcvc4_include_directories(${GLPK_INCLUDE_DIR})
   add_definitions(-DCVC4_USE_GLPK)
 endif()
 
@@ -422,7 +446,8 @@ if(USE_LFSC)
   set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc)
   set(LFSC_HOME ${LFSC_DIR})
   find_package(LFSC REQUIRED)
-  include_directories(${LFSC_INCLUDE_DIR})
+  libcvc4_link_libraries(${LFSC_LIBRARIES})
+  libcvc4_include_directories(${LFSC_INCLUDE_DIR})
   add_definitions(-DCVC4_USE_LFSC)
   set(CVC4_USE_LFSC 1)
 else()
@@ -444,7 +469,7 @@ endif()
 if(USE_SYMFPU)
   set(SymFPU_HOME ${SYMFPU_DIR})
   find_package(SymFPU REQUIRED)
-  include_directories(${SymFPU_INCLUDE_DIR})
+  libcvc4_include_directories(${SymFPU_INCLUDE_DIR})
   add_definitions(-DCVC4_USE_SYMFPU)
   set(CVC4_USE_SYMFPU 1)
 else()
@@ -575,10 +600,10 @@ endif()
 
 if(ENABLE_PROOFS)
   add_subdirectory(proofs/signatures)
-  cvc4_link_library(signatures)
 endif()
 
 #-----------------------------------------------------------------------------#
+# Print build configuration
 
 if(CVC4_BUILD_PROFILE_PRODUCTION)
   set(CVC4_BUILD_PROFILE_STRING "production")
@@ -590,6 +615,10 @@ elseif(CVC4_BUILD_PROFILE_COMPETITION)
   set(CVC4_BUILD_PROFILE_STRING "competition")
 endif()
 
+# Get all definitions added via add_definitions to print it below
+get_directory_property(CVC4_DEFINITIONS COMPILE_DEFINITIONS)
+string(REPLACE ";" " " CVC4_DEFINITIONS "${CVC4_DEFINITIONS}")
+
 message("CVC4 ${CVC4_RELEASE_STRING}")
 message("")
 message("Build profile     : ${CVC4_BUILD_PROFILE_STRING}")
@@ -608,12 +637,7 @@ message("Unit tests        : ${ENABLE_UNIT_TESTING}")
 message("Coverage (gcov)   : ${ENABLE_COVERAGE}")
 message("Profiling (gprof) : ${ENABLE_PROFILING}")
 message("")
-#message("Static libs  : ${enable_static}")
-if(BUILD_SHARED_LIBS)
-	message("Shared libs       : ON")
-else()
-	message("Shared libs       : OFF")
-endif()
+message("Shared libs       : ${ENABLE_SHARED}")
 #message("Static binary: ${enable_static_binary}")
 #message("Compat lib   : ${CVC4_BUILD_LIBCOMPAT}")
 #message("Bindings     : ${bindings_to_be_built}")
@@ -626,11 +650,15 @@ message("CaDiCaL           : ${USE_CADICAL}")
 message("CryptoMiniSat     : ${USE_CRYPTOMINISAT}")
 message("GLPK              : ${USE_GLPK}")
 message("LFSC              : ${USE_LFSC}")
-#message("MP library   : ${mplibrary}")
+if(CVC4_USE_CLN_IMP)
+  message("MP library        : cln")
+else()
+  message("MP library        : gmp")
+endif()
 message("Readline          : ${USE_READLINE}")
 message("SymFPU            : ${USE_SYMFPU}")
 message("")
-#message("CPPFLAGS     : ${CPPFLAGS}")
+message("CPPLAGS (-D...)   : ${CVC4_DEFINITIONS}")
 message("CXXFLAGS          : ${CMAKE_CXX_FLAGS}")
 message("CFLAGS            : ${CMAKE_C_FLAGS}")
 #message("LIBS         : ${LIBS}")
@@ -641,7 +669,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 into : ${prefix}")
+message("Install prefix    : ${CMAKE_INSTALL_PREFIX}")
 message("")
 
 if(GPL_LIBS)