From 8a8d65e2fddf88bfbd6cc67d8738510feaea05e6 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 10 Aug 2018 16:45:27 -0700 Subject: [PATCH] Fix portfolio command executor for changes from #2240. (#2294) --- src/main/command_executor_portfolio.cpp | 39 ++++++++++++------------- src/main/command_executor_portfolio.h | 22 +++++++++----- src/main/driver_unified.cpp | 4 +-- src/main/portfolio_util.h | 6 ++-- src/util/channel.h | 16 +++++----- 5 files changed, 47 insertions(+), 40 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 #include +#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 d_solvers; - // These shall be created/deleted during initialization std::vector 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 */ diff --git a/src/util/channel.h b/src/util/channel.h index 5a5610410..8587800c1 100644 --- a/src/util/channel.h +++ b/src/util/channel.h @@ -74,8 +74,10 @@ public: explicit SynchronizedSharedChannel(size_type capacity) : m_unread(0), m_container(capacity) {} - bool push(param_type item){ - // param_type represents the "best" way to pass a parameter of type value_type to a method + bool push(param_type item) override + { + // param_type represents the "best" way to pass a parameter of type + // value_type to a method boost::mutex::scoped_lock lock(m_mutex); m_not_full.wait(lock, boost::bind(&SynchronizedSharedChannel::is_not_full, this)); @@ -86,7 +88,8 @@ public: return true; }//function definitions need to be moved to cpp - value_type pop(){ + value_type pop() override + { value_type ret; boost::mutex::scoped_lock lock(m_mutex); m_not_empty.wait(lock, boost::bind(&SynchronizedSharedChannel::is_not_empty, this)); @@ -96,11 +99,10 @@ public: return ret; } + bool empty() override { return not is_not_empty(); } + bool full() override { return not is_not_full(); } - bool empty() { return not is_not_empty(); } - bool full() { return not is_not_full(); } - -private: + private: SynchronizedSharedChannel(const SynchronizedSharedChannel&); // Disabled copy constructor SynchronizedSharedChannel& operator = (const SynchronizedSharedChannel&); // Disabled assign operator -- 2.30.2