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/command_executor_portfolio.cpp | |
parent | c9ad9015ac941f5fe5c99d7234fe74cbd40da030 (diff) |
Fix portfolio command executor for changes from #2240. (#2294)
Diffstat (limited to 'src/main/command_executor_portfolio.cpp')
-rw-r--r-- | src/main/command_executor_portfolio.cpp | 39 |
1 files changed, 19 insertions, 20 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(); |