diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-22 16:07:26 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-22 16:07:26 -0700 |
commit | 93f4888b6bce4766ef3af0830b5c057a1cd11399 (patch) | |
tree | f5e4ae149f19eb002e82ab27985195d9269c8432 /src/main/driver_unified.cpp | |
parent | 5cdd2d16670725e29b1f43510fc5246e9c861fe3 (diff) |
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
Diffstat (limited to 'src/main/driver_unified.cpp')
-rw-r--r-- | src/main/driver_unified.cpp | 13 |
1 files changed, 7 insertions, 6 deletions
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; |