diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-08-10 16:45:27 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-10 16:45:27 -0700 |
commit | 8a8d65e2fddf88bfbd6cc67d8738510feaea05e6 (patch) | |
tree | 946a8b2cc283f0da893640c2928cc86343a8b6be /src/main | |
parent | c9ad9015ac941f5fe5c99d7234fe74cbd40da030 (diff) |
Fix portfolio command executor for changes from #2240. (#2294)
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/command_executor_portfolio.cpp | 39 | ||||
-rw-r--r-- | src/main/command_executor_portfolio.h | 22 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 4 | ||||
-rw-r--r-- | src/main/portfolio_util.h | 6 |
4 files changed, 38 insertions, 33 deletions
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 0755311f3..ba75d5ff7 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -27,6 +27,7 @@ #include <boost/thread/condition.hpp> #include <string> +#include "api/cvc4cpp.h" #include "cvc4autoconfig.h" #include "expr/pickler.h" #include "main/main.h" @@ -35,15 +36,15 @@ #include "options/set_language.h" #include "smt/command.h" - using namespace std; namespace CVC4 { namespace main { -CommandExecutorPortfolio::CommandExecutorPortfolio( - ExprManager &exprMgr, Options &options, OptionsList& tOpts) - : CommandExecutor(exprMgr, options), +CommandExecutorPortfolio::CommandExecutorPortfolio(api::Solver* solver, + Options& options, + OptionsList& tOpts) + : CommandExecutor(solver, options), d_numThreads(options.getThreads()), d_smts(), d_seq(new CommandSequence()), @@ -64,19 +65,17 @@ CommandExecutorPortfolio::CommandExecutorPortfolio( d_stats.registerStat(&d_statWaitTime); /* Duplication, individualization */ - d_exprMgrs.push_back(&d_exprMgr); - for(unsigned i = 1; i < d_numThreads; ++i) { - d_exprMgrs.push_back(new ExprManager(d_threadOptions[i])); - } - - // Create the SmtEngine(s) - d_smts.push_back(d_smtEngine); - for(unsigned i = 1; i < d_numThreads; ++i) { - d_smts.push_back(new SmtEngine(d_exprMgrs[i])); - } - + d_solvers.push_back(d_solver); + d_exprMgrs.push_back(d_solver->getExprManager()); + d_smts.push_back(d_solver->getSmtEngine()); assert(d_vmaps.size() == 0); - for(unsigned i = 0; i < d_numThreads; ++i) { + d_vmaps.push_back(new ExprManagerMapCollection()); + for (unsigned i = 1; i < d_numThreads; ++i) + { + api::Solver* solver = new api::Solver(&d_threadOptions[i]); + d_solvers.push_back(solver); + d_exprMgrs.push_back(solver->getExprManager()); + d_smts.push_back(solver->getSmtEngine()); d_vmaps.push_back(new ExprManagerMapCollection()); } } @@ -87,12 +86,12 @@ CommandExecutorPortfolio::~CommandExecutorPortfolio() delete d_seq; assert(d_smts.size() == d_numThreads); - for(unsigned i = 1; i < d_numThreads; ++i) { + for (unsigned i = 1; i < d_numThreads; ++i) + { // the 0-th one is responsibility of parent class - - delete d_smts[i]; - delete d_exprMgrs[i]; + delete d_solvers[i]; } + d_solvers.clear(); d_exprMgrs.clear(); d_smts.clear(); diff --git a/src/main/command_executor_portfolio.h b/src/main/command_executor_portfolio.h index 39c577087..fe4d35640 100644 --- a/src/main/command_executor_portfolio.h +++ b/src/main/command_executor_portfolio.h @@ -30,11 +30,16 @@ namespace CVC4 { class CommandSequence; +namespace api { +class Solver; +} + namespace main { class CommandExecutorPortfolio : public CommandExecutor { + // Solvers are created/deleted during initialization + std::vector<api::Solver*> d_solvers; - // These shall be created/deleted during initialization std::vector<ExprManager*> d_exprMgrs; const unsigned d_numThreads; // Currently const, but designed so it is // not too hard to support this changing @@ -55,18 +60,19 @@ class CommandExecutorPortfolio : public CommandExecutor { TimerStat d_statWaitTime; public: - CommandExecutorPortfolio(ExprManager &exprMgr, - Options &options, - OptionsList& tOpts); + CommandExecutorPortfolio(api::Solver* solver, + Options& options, + OptionsList& tOpts); - ~CommandExecutorPortfolio(); + ~CommandExecutorPortfolio(); - std::string getSmtEngineStatus(); + std::string getSmtEngineStatus(); - void flushStatistics(std::ostream& out) const; + void flushStatistics(std::ostream& out) const override; protected: - bool doCommandSingleton(Command* cmd); + bool doCommandSingleton(Command* cmd) override; + private: CommandExecutorPortfolio(); void lemmaSharingInit(); diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index c29212c4f..390d83eba 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -233,12 +233,12 @@ int runCvc4(int argc, char* argv[], Options& opts) { // pick appropriate one if (useParallelExecutor) { - solver.reset(&threadOpts[0]); + solver.reset(new api::Solver(&threadOpts[0])); pExecutor = new CommandExecutorPortfolio(solver.get(), opts, threadOpts); } else { - solver.reset(&opts); + solver.reset(new api::Solver(&opts)); pExecutor = new CommandExecutor(solver.get(), opts); } # endif diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h index 6ebd97d3d..5b2152728 100644 --- a/src/main/portfolio_util.h +++ b/src/main/portfolio_util.h @@ -49,7 +49,7 @@ public: ~PortfolioLemmaOutputChannel() {} - void notifyNewLemma(Expr lemma); + void notifyNewLemma(Expr lemma) override; };/* class PortfolioLemmaOutputChannel */ class PortfolioLemmaInputChannel : public LemmaInputChannel { @@ -67,8 +67,8 @@ public: ~PortfolioLemmaInputChannel() {} - bool hasNewLemma(); - Expr getNewLemma(); + bool hasNewLemma() override; + Expr getNewLemma() override; };/* class PortfolioLemmaInputChannel */ |