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 dba12006e067d30a6f6ed62bcb33b1c177d22e7b..be9575f5db8372d001123d061cafa7c38fb51597 100644 (file)
--- 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 d9932fb430bdba238be4dd53462b266a7b2a8ccb..de2348973c5ada7fdbd70f24b7485e3f49529fea 100644 (file)
--- 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;