From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 22 Oct 2018 23:07:26 +0000 (-0700)
Subject: CMake: Set PORTFOLIO_BUILD when building pcvc4 (#2666)
X-Git-Tag: cvc5-1.0.0~4390
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=93f4888b6bce4766ef3af0830b5c057a1cd11399;p=cvc5.git

CMake: Set PORTFOLIO_BUILD when building pcvc4 (#2666)

Back when we used Autotools, we set the PORTFOLIO_BUILD macro when
building pcvc4. Our CMake build system is currently not doing that, so
setting thread options when running pcvc4 results in an error message
saying that "thread options cannot be used with sequential CVC4."
This commit fixes that behavior by recompiling driver_unified.cpp with
different options for the cvc4 and the pcvc4 binary.

[0] https://github.com/CVC4/CVC4/blob/7de0540252b62080ee9f98617f5718cb1ae08579/src/main/Makefile.am#L36
---

diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
index dba12006e..be9575f5d 100644
--- a/src/main/CMakeLists.txt
+++ b/src/main/CMakeLists.txt
@@ -3,7 +3,6 @@
 
 set(libmain_src_files
   command_executor.cpp
-  driver_unified.cpp
   interactive_shell.cpp
   interactive_shell.h
   main.h
@@ -32,13 +31,14 @@ target_include_directories(main PRIVATE ${LIBCVC4_INCLUDES})
 # main-test library is only used for linking against system and unit tests so
 # that we don't have to include all object files of main into each unit/system
 # test. Do not link against main-test in any other case.
-add_library(main-test $<TARGET_OBJECTS:main>)
+add_library(main-test driver_unified.cpp $<TARGET_OBJECTS:main>)
+target_compile_definitions(main-test PRIVATE -D__BUILDING_CVC4DRIVER)
 target_link_libraries(main-test cvc4 cvc4parser)
 
 #-----------------------------------------------------------------------------#
 # cvc4 binary configuration
 
-add_executable(cvc4-bin main.cpp $<TARGET_OBJECTS:main>)
+add_executable(cvc4-bin driver_unified.cpp main.cpp $<TARGET_OBJECTS:main>)
 target_compile_definitions(cvc4-bin PRIVATE -D__BUILDING_CVC4DRIVER)
 set_target_properties(cvc4-bin
   PROPERTIES
@@ -64,17 +64,19 @@ endif()
 
 if(ENABLE_PORTFOLIO)
   set(pcvc4_src_files
+    command_executor_portfolio.cpp
+    command_executor_portfolio.h
+    driver_unified.cpp
     main.cpp
     portfolio.cpp
     portfolio.h
     portfolio_util.cpp
     portfolio_util.h
-    command_executor_portfolio.cpp
-    command_executor_portfolio.h
   )
 
   add_executable(pcvc4-bin ${pcvc4_src_files} $<TARGET_OBJECTS:main>)
   target_compile_definitions(pcvc4-bin PRIVATE -D__BUILDING_CVC4DRIVER)
+  target_compile_definitions(pcvc4-bin PRIVATE -DPORTFOLIO_BUILD)
   set_target_properties(pcvc4-bin
     PROPERTIES
       OUTPUT_NAME pcvc4
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index d9932fb43..de2348973 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -23,7 +23,6 @@
 #include <memory>
 #include <new>
 
-// This must come before PORTFOLIO_BUILD.
 #include "cvc4autoconfig.h"
 
 #include "api/cvc4cpp.h"
@@ -32,11 +31,6 @@
 #include "expr/expr_iomanip.h"
 #include "expr/expr_manager.h"
 #include "main/command_executor.h"
-
-#ifdef PORTFOLIO_BUILD
-#  include "main/command_executor_portfolio.h"
-#endif
-
 #include "main/interactive_shell.h"
 #include "main/main.h"
 #include "options/options.h"
@@ -48,6 +42,13 @@
 #include "util/result.h"
 #include "util/statistics_registry.h"
 
+// The PORTFOLIO_BUILD is defined when compiling pcvc4 (the parallel version of
+// CVC4) and undefined otherwise. The macro can only be used in
+// driver_unified.cpp because we do not recompile all files for pcvc4.
+#ifdef PORTFOLIO_BUILD
+#  include "main/command_executor_portfolio.h"
+#endif
+
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::parser;