cmake: Do not link against main object library. (#6269)

CMake 3.10.2 (default on Ubuntu 18.04) does not allow target_link_libraries on object libraries.

diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
index fd2d415b2dc064e0bb8173ab83f5c67752d7d06f..4a8e7e1bc024f7582ca00f54bd5b578b66ba492b 100644 (file)
--- a/src/main/CMakeLists.txt
+++ b/src/main/CMakeLists.txt
@@ -23,8 +23,8 @@ set(libmain_src_files
 )
 
 #-----------------------------------------------------------------------------#
-# Build object library since we will use the object files for cvc4-bin,
-# pcvc4-bin, and main-test library.
+# Build object library since we will use the object files for cvc4-bin and
+# main-test library.
 
 add_library(main OBJECT ${libmain_src_files})
 target_compile_definitions(main PRIVATE -D__BUILDING_CVC4DRIVER)
@@ -32,18 +32,22 @@ 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
-# cmake version >= 3.12. Hence, we have to manually add the library
-# dependencies for main. As a consequence, include directories from
+# We can't use target_link_libraries(main ...) here since this is only
+# supported for cmake version >= 3.12. Hence, we have to manually add the
+# library dependencies for main. As a consequence, include directories from
 # 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})
+
+# Note: This should not be required anymore as soon as we get rid of the
+#       smt_engine.h include in src/main. smt_engine.h has transitive includes
+#       of GMP and CLN via sexpr.h and therefore needs GMP/CLN headers.
 if(USE_CLN)
-  target_link_libraries(main PUBLIC CLN)
+  get_target_property(CLN_INCLUDES CLN INTERFACE_INCLUDE_DIRECTORIES)
+  target_include_directories(main PRIVATE ${CLN_INCLUDES})
 endif()
-target_link_libraries(main PUBLIC GMP)
+get_target_property(GMP_INCLUDES GMP INTERFACE_INCLUDE_DIRECTORIES)
+target_include_directories(main PRIVATE ${GMP_INCLUDES})
 
 # main-test library is only used for linking against api and unit tests so
 # that we don't have to include all object files of main into each api/unit
@@ -70,6 +74,7 @@ if(USE_CLN)
   target_link_libraries(cvc4-bin PUBLIC CLN)
 endif()
 target_link_libraries(cvc4-bin PUBLIC GMP)
+
 if(PROGRAM_PREFIX)
   install(PROGRAMS
     $<TARGET_FILE:cvc4-bin>

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index b7e3ad8b04ae79d8e467e6fbb77def5774740f5e..75d116f3392cbd1a107ec9715749d6f3049a9ffd 100644 (file)
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -18,6 +18,7 @@
 #  include <sys/resource.h>
 #endif /* ! __WIN32__ */
 
+#include <iomanip>
 #include <iostream>
 #include <memory>
 #include <string>
@@ -25,6 +26,7 @@
 
 #include "main/main.h"
 #include "smt/command.h"
+#include "smt/smt_engine.h"
 
 namespace cvc5 {
 namespace main {

diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 60305ff1f2ce15c0818e3f480d07aca320f57bca..d2117e109d6e60a6287f58785c5c00db620ffddc 100644 (file)
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -21,13 +21,15 @@
 #include "api/cvc4cpp.h"
 #include "expr/symbol_manager.h"
 #include "options/options.h"
-#include "smt/smt_engine.h"
-#include "util/statistics_registry.h"
 
 namespace cvc5 {
 
 class Command;
 
+namespace smt {
+class SmtEngine;
+}
+
 namespace main {
 
 class CommandExecutor

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index fdf6a83354a8206a06a23a3e56677284e6b4cbd8..6f9377a33c4bbd5929fb5c1ea76f588ed31c7e0c 100644 (file)
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -23,11 +23,10 @@
 #include <memory>
 #include <new>
 
-#include "cvc4autoconfig.h"
-
 #include "api/cvc4cpp.h"
 #include "base/configuration.h"
 #include "base/output.h"
+#include "cvc4autoconfig.h"
 #include "main/command_executor.h"
 #include "main/interactive_shell.h"
 #include "main/main.h"
@@ -38,6 +37,7 @@
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "smt/command.h"
+#include "smt/smt_engine.h"
 #include "util/result.h"
 
 using namespace std;

diff --git a/src/main/signal_handlers.cpp b/src/main/signal_handlers.cpp
index bd9ec7ee019282b02417b1e0735af8d6b5a7cd8a..02544c7e3b037e0dda91e97a682b8baf975ee7fb 100644 (file)
--- a/src/main/signal_handlers.cpp
+++ b/src/main/signal_handlers.cpp
@@ -38,7 +38,6 @@
 #include "main/command_executor.h"
 #include "main/main.h"
 #include "options/options.h"
-#include "smt/smt_engine.h"
 #include "util/safe_print.h"
 
 using cvc5::Exception;