From 385ecf64fd4437ca15156a44b97f2001428dc1f5 Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Fri, 2 Apr 2021 12:12:15 -0700
Subject: [PATCH] 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.
---
 src/main/CMakeLists.txt       | 23 ++++++++++++++---------
 src/main/command_executor.cpp |  2 ++
 src/main/command_executor.h   |  6 ++++--
 src/main/driver_unified.cpp   |  4 ++--
 src/main/signal_handlers.cpp  |  1 -
 5 files changed, 22 insertions(+), 14 deletions(-)

diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
index fd2d415b2..4a8e7e1bc 100644
--- 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 b7e3ad8b0..75d116f33 100644
--- 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 60305ff1f..d2117e109 100644
--- 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 fdf6a8335..6f9377a33 100644
--- 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 bd9ec7ee0..02544c7e3 100644
--- 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;
-- 
2.30.2