summaryrefslogtreecommitdiff
path: root/src/main/driver_unified.cpp
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2018-10-22 16:07:26 -0700
committerGitHub <noreply@github.com>2018-10-22 16:07:26 -0700
commit93f4888b6bce4766ef3af0830b5c057a1cd11399 (patch)
treef5e4ae149f19eb002e82ab27985195d9269c8432 /src/main/driver_unified.cpp
parent5cdd2d16670725e29b1f43510fc5246e9c861fe3 (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.cpp13
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback