diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-06 20:52:16 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-06 20:52:16 -0500 |
commit | 1c09572e0e2031519a103caa2a4af0d9bd34a9c5 (patch) | |
tree | 576012b4e9434bd4b8472b5df766d3836d3145b9 /src/main/driver_unified.cpp | |
parent | 856701f3b2154646eab6b7898fa33e5917322a7b (diff) |
Remove portfolio (#3236)
Diffstat (limited to 'src/main/driver_unified.cpp')
-rw-r--r-- | src/main/driver_unified.cpp | 58 |
1 files changed, 1 insertions, 57 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index de840cb07..c4800a3ac 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -9,8 +9,7 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Driver for CVC4 executable (cvc4) unified for both - ** sequential and portfolio versions + ** \brief Driver for CVC4 executable (cvc4) **/ #include <stdio.h> @@ -42,13 +41,6 @@ #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; @@ -106,14 +98,6 @@ int runCvc4(int argc, char* argv[], Options& opts) { // Parse the options vector<string> filenames = Options::parseOptions(&opts, argc, argv); -# ifndef PORTFOLIO_BUILD - if( opts.wasSetByUserThreads() || - opts.wasSetByUserThreadStackSize() || - (! opts.getThreadArgv().empty()) ) { - throw OptionException("Thread options cannot be used with sequential CVC4. Please build and use the portfolio binary `pcvc4'."); - } -# endif - string progNameStr = opts.getBinaryName(); progName = &progNameStr; @@ -199,46 +183,8 @@ int runCvc4(int argc, char* argv[], Options& opts) { // Create the expression manager using appropriate options std::unique_ptr<api::Solver> solver; -# ifndef PORTFOLIO_BUILD solver.reset(new api::Solver(&opts)); pExecutor = new CommandExecutor(solver.get(), opts); -# else - OptionsList threadOpts; - parseThreadSpecificOptions(threadOpts, opts); - - bool useParallelExecutor = true; - // incremental? - if(opts.wasSetByUserIncrementalSolving() && - opts.getIncrementalSolving() && - (! opts.getIncrementalParallel()) ) { - Notice() << "Notice: In --incremental mode, using the sequential solver" - << " unless forced by...\n" - << "Notice: ...the experimental --incremental-parallel option.\n"; - useParallelExecutor = false; - } - // proofs? - if(opts.getCheckProofs()) { - if(opts.getFallbackSequential()) { - Warning() << "Warning: Falling back to sequential mode, as cannot run" - << " portfolio in check-proofs mode.\n"; - useParallelExecutor = false; - } - else { - throw OptionException("Cannot run portfolio in check-proofs mode."); - } - } - // pick appropriate one - if (useParallelExecutor) - { - solver.reset(new api::Solver(&threadOpts[0])); - pExecutor = new CommandExecutorPortfolio(solver.get(), opts, threadOpts); - } - else - { - solver.reset(new api::Solver(&opts)); - pExecutor = new CommandExecutor(solver.get(), opts); - } -# endif std::unique_ptr<Parser> replayParser; if (opts.getReplayInputFilename() != "") @@ -277,14 +223,12 @@ int runCvc4(int argc, char* argv[], Options& opts) { throw OptionException( "--tear-down-incremental doesn't work in interactive mode"); } -#ifndef PORTFOLIO_BUILD if(!opts.wasSetByUserIncrementalSolving()) { cmd = new SetOptionCommand("incremental", SExpr(true)); cmd->setMuted(true); pExecutor->doCommand(cmd); delete cmd; } -#endif /* PORTFOLIO_BUILD */ InteractiveShell shell(solver.get()); if(opts.getInteractivePrompt()) { Message() << Configuration::getPackageName() |