diff options
-rw-r--r-- | src/main/CMakeLists.txt | 12 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 13 |
2 files changed, 14 insertions, 11 deletions
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; |