Fix portfolio command executor for changes from #2240. (#2294)

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 <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 */
 
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<value_type>::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<value_type>::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