diff options
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(); |