From: Morgan Deters Date: Sat, 8 Sep 2012 22:31:44 +0000 (+0000) Subject: Some minor changes after reviewing the portfolio "unified driver" commit. X-Git-Tag: cvc5-1.0.0~7822 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=480d440174c565bec9aba412c0d35221c9169ff6;p=cvc5.git Some minor changes after reviewing the portfolio "unified driver" commit. (this commit was certified error- and warning-free by the test-and-commit script.) --- diff --git a/src/expr/command.h b/src/expr/command.h index 3c919c374..70e71a111 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -50,13 +50,12 @@ std::ostream& operator<<(std::ostream&, const Command*) throw() CVC4_PUBLIC; std::ostream& operator<<(std::ostream&, const CommandStatus&) throw() CVC4_PUBLIC; std::ostream& operator<<(std::ostream&, const CommandStatus*) throw() CVC4_PUBLIC; -class ExportToUnsupportedException : public Exception { +class CVC4_PUBLIC ExportToUnsupportedException : public Exception { public: ExportToUnsupportedException() throw() : Exception("exportTo unsupported for command") { } -};/* class NoMoreValuesException */ - +};/* class ExportToUnsupportedException */ /** The status an SMT benchmark can have */ enum BenchmarkStatus { diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 4009bc610..08c3a2b1e 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -137,9 +137,11 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC } else if(n.getKind() == kind::VARIABLE) { to_e = to->mkVar(name, type);// FIXME thread safety } else if(n.getKind() == kind::SKOLEM) { - Assert(false, "Skolem exporting not yet supported properly."); - // to fix this, get the node manager and do the appropriate - to_e = to->mkVar(name, type);// FIXME thread safety + // skolems are only available at the Node level (not the Expr level) + TypeNode typeNode = TypeNode::fromType(type); + NodeManager* to_nm = NodeManager::fromExprManager(to); + Node n = to_nm->mkSkolem(name, typeNode);// FIXME thread safety + to_e = n.toExpr(); } else { Unhandled(); } diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 9b0200231..2a1ce0d55 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -20,8 +20,10 @@ pcvc4_SOURCES = \ portfolio.cpp \ portfolio.h \ portfolio_util.cpp \ - command_executer.cpp \ - command_executer_portfolio.cpp \ + command_executor.cpp \ + command_executor_portfolio.cpp \ + command_executor.h \ + command_executor_portfolio.h \ driver_unified.cpp pcvc4_LDADD = \ libmain.a \ @@ -42,7 +44,7 @@ endif cvc4_SOURCES = \ main.cpp \ - command_executer.cpp \ + command_executor.cpp \ driver_unified.cpp cvc4_LDADD = \ libmain.a \ diff --git a/src/main/command_executer.cpp b/src/main/command_executer.cpp deleted file mode 100644 index 039ab664c..000000000 --- a/src/main/command_executer.cpp +++ /dev/null @@ -1,93 +0,0 @@ -/********************* */ -/*! \file command_executer.cpp - ** \verbatim - ** Original author: kshitij - ** Major contributors: none - ** Minor contributors (to current version): - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief An additional layer between commands and invoking them. - **/ - -#include - -#include "main/command_executer.h" -#include "expr/command.h" - -#include "main/main.h" - -namespace CVC4 { -namespace main { - - -CommandExecuter::CommandExecuter(ExprManager &exprMgr, Options &options): - d_exprMgr(exprMgr), - d_smtEngine(SmtEngine(&exprMgr)), - d_options(options) { - - // signal handlers need access - main::pStatistics = d_smtEngine.getStatisticsRegistry(); - d_exprMgr.getStatisticsRegistry()->setName("ExprManager"); - main::pStatistics->registerStat_(d_exprMgr.getStatisticsRegistry()); -} - -bool CommandExecuter::doCommand(Command* cmd) -{ - if( d_options[options::parseOnly] ) { - return true; - } - - CommandSequence *seq = dynamic_cast(cmd); - if(seq != NULL) { - // assume no error - bool status = true; - - for(CommandSequence::iterator subcmd = seq->begin(); - status && subcmd != seq->end(); - ++subcmd) { - status = doCommand(*subcmd); - } - - return status; - } else { - if(d_options[options::verbosity] > 0) { - *d_options[options::out] << "Invoking: " << *cmd << std::endl; - } - - return doCommandSingleton(cmd); - } -} - -bool CommandExecuter::doCommandSingleton(Command *cmd) -{ - bool status = true; - if(d_options[options::verbosity] >= 0) { - status = smtEngineInvoke(&d_smtEngine, cmd, d_options[options::out]); - } else { - status = smtEngineInvoke(&d_smtEngine, cmd, NULL); - } - return status; -} - -std::string CommandExecuter::getSmtEngineStatus() -{ - return d_smtEngine.getInfo("status").getValue(); -} - -bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out) -{ - if(out == NULL) { - cmd->invoke(smt); - } else { - cmd->invoke(smt, *out); - } - return !cmd->fail(); -} - -}/*main namespace*/ -}/*CVC4 namespace*/ diff --git a/src/main/command_executer.h b/src/main/command_executer.h deleted file mode 100644 index 245857c04..000000000 --- a/src/main/command_executer.h +++ /dev/null @@ -1,69 +0,0 @@ -/********************* */ -/*! \file command_executer.cpp - ** \verbatim - ** Original author: kshitij - ** Major contributors: mdeters - ** Minor contributors (to current version): - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief An additional layer between commands and invoking them. - **/ - -#ifndef __CVC4__COMMAND_EXECUTER_H -#define __CVC4__COMMAND_EXECUTER_H - -#include "expr/expr_manager.h" -#include "smt/smt_engine.h" - -namespace CVC4 { - -namespace main { - -class CommandExecuter { - -protected: - ExprManager& d_exprMgr; - SmtEngine d_smtEngine; - Options& d_options; - -public: - // Note: though the options are not cached (instead a reference is - // used), the portfolio command executer currently parses them - // during initalization, creating thread-specific options and - // storing them - CommandExecuter(ExprManager &exprMgr, Options &options); - - ~CommandExecuter() {} - - /** - * Executes a command. Recursively handles if cmd is a command - * sequence. Eventually uses doCommandSingleton (which can be - * overridden by a derived class). - */ - bool doCommand(CVC4::Command* cmd); - - virtual std::string getSmtEngineStatus(); - -protected: - /** Executes treating cmd as a singleton */ - virtual bool doCommandSingleton(CVC4::Command* cmd); - -private: - CommandExecuter(); - -}; - -bool smtEngineInvoke(SmtEngine* smt, - Command* cmd, - std::ostream *out); - - -}/*main namespace*/ -}/*CVC4 namespace*/ - -#endif /* __CVC4__COMMAND_EXECUTER_H */ diff --git a/src/main/command_executer_portfolio.cpp b/src/main/command_executer_portfolio.cpp deleted file mode 100644 index 85180c9a9..000000000 --- a/src/main/command_executer_portfolio.cpp +++ /dev/null @@ -1,314 +0,0 @@ -/********************* */ -/*! \file command_executer_portfolio.cpp - ** \verbatim - ** Original author: kshitij - ** Major contributors: mdeters, taking - ** Minor contributors (to current version): - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief An additional layer between commands and invoking them. - ** - ** The portfolio executer branches check-sat queries to several - ** threads. - **/ - -#include -#include -#include -#include - -#include "expr/command.h" -#include "expr/pickler.h" -#include "main/command_executer_portfolio.h" -#include "main/main.h" -#include "main/options.h" -#include "main/portfolio.h" -#include "options/options.h" -#include "smt/options.h" - -using namespace std; - -namespace CVC4 { -namespace main { - -CommandExecuterPortfolio::CommandExecuterPortfolio -(ExprManager &exprMgr, Options &options, vector& tOpts): - CommandExecuter(exprMgr, options), - d_numThreads(options[options::threads]), - d_smts(), - d_seq(new CommandSequence()), - d_threadOptions(tOpts), - d_vmaps(), - d_lastWinner(0), - d_channelsOut(), - d_channelsIn(), - d_ostringstreams() -{ - Assert(d_threadOptions.size() == d_numThreads); - - /* Duplication, Individualisation */ - 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])); - } - - for(unsigned i = 1; i < d_numThreads; ++i) { - // Register the statistics registry of the thread - string emTag = "ExprManager thread #" - + boost::lexical_cast(d_threadOptions[i][options::thread_id]); - string smtTag = "SmtEngine thread #" - + boost::lexical_cast(d_threadOptions[i][options::thread_id]); - d_exprMgrs[i]->getStatisticsRegistry()->setName(emTag); - d_smts[i]->getStatisticsRegistry()->setName(smtTag); - pStatistics->registerStat_ - (d_exprMgrs[i]->getStatisticsRegistry() ); - pStatistics->registerStat_ - (d_smts[i]->getStatisticsRegistry() ); - } - - Assert(d_vmaps.size() == 0); - for(unsigned i = 0; i < d_numThreads; ++i) { - d_vmaps.push_back(new ExprManagerMapCollection()); - } - - -} - -CommandExecuterPortfolio::~CommandExecuterPortfolio() -{ - Assert(d_seq != NULL); - delete d_seq; - - Assert(d_smts.size() == d_numThreads); - for(unsigned i = 1; i < d_numThreads; ++i) { - // the 0-th one is responsibility of parent class - - delete d_exprMgrs[i]; - delete d_smts[i]; - } - d_exprMgrs.clear(); - d_smts.clear(); -} - -void CommandExecuterPortfolio::lemmaSharingInit() -{ - /* Sharing channels */ - Assert(d_channelsIn.size() == 0); - Assert(d_channelsOut.size() == 0); - - if(d_numThreads == 1) { - // Disable sharing - d_threadOptions[0].set(options::sharingFilterByLength, 0); - } else { - // Setup sharing channels - const unsigned int sharingChannelSize = 1000000; - - for(unsigned i = 0; i < d_numThreads; ++i){ - if(Debug.isOn("channel-empty")) { - d_channelsOut.push_back - (new EmptySharedChannel(sharingChannelSize)); - d_channelsIn.push_back - (new EmptySharedChannel(sharingChannelSize)); - continue; - } - d_channelsOut.push_back - (new SynchronizedSharedChannel(sharingChannelSize)); - d_channelsIn.push_back - (new SynchronizedSharedChannel(sharingChannelSize)); - } - - /* Lemma I/O channels */ - for(unsigned i = 0; i < d_numThreads; ++i) { - string tag = "thread #" + - boost::lexical_cast(d_threadOptions[i][options::thread_id]); - d_threadOptions[i].set - (options::lemmaOutputChannel, - new PortfolioLemmaOutputChannel(tag, d_channelsOut[i], d_exprMgrs[i], - d_vmaps[i]->d_from, d_vmaps[i]->d_to)); - d_threadOptions[i].set - (options::lemmaInputChannel, - new PortfolioLemmaInputChannel(tag, d_channelsIn[i], d_exprMgrs[i], - d_vmaps[i]->d_from, d_vmaps[i]->d_to)); - } - - /* Output to string stream */ - if(d_options[options::verbosity] == 0 - || d_options[options::separateOutput]) { - Assert(d_ostringstreams.size() == 0); - for(unsigned i = 0; i < d_numThreads; ++i) { - d_ostringstreams.push_back(new ostringstream); - d_threadOptions[i].set(options::out, d_ostringstreams[i]); - } - } - } -} - -void CommandExecuterPortfolio::lemmaSharingCleanup() -{ - Assert(d_numThreads == d_options[options::threads]); - - // Channel cleanup - Assert(d_channelsIn.size() == d_numThreads); - Assert(d_channelsOut.size() == d_numThreads); - for(unsigned i = 0; i < d_numThreads; ++i) { - delete d_channelsIn[i]; - delete d_channelsOut[i]; - d_threadOptions[i].set(options::lemmaInputChannel, NULL); - d_threadOptions[i].set(options::lemmaOutputChannel, NULL); - } - d_channelsIn.clear(); - d_channelsOut.clear(); - - // sstreams cleanup (if used) - if(d_ostringstreams.size() != 0) { - Assert(d_ostringstreams.size() == d_numThreads); - for(unsigned i = 0; i < d_numThreads; ++i) { - d_threadOptions[i].set(options::out, d_options[options::out]); - delete d_ostringstreams[i]; - } - d_ostringstreams.clear(); - } - -} - -bool CommandExecuterPortfolio::doCommandSingleton(Command* cmd) -{ - /** - * save the command and if check sat or query command, run a - * porfolio of SMT solvers. - */ - - int mode = 0; - // mode = 0 : run the first thread - // mode = 1 : run a porfolio - // mode = 2 : run the last winner - - // if(dynamic_cast(cmd) != NULL || - // dynamic_cast(cmd) != NULL) { - // mode = 1; - // } else if(dynamic_cast(cmd) != NULL) { - // mode = 2; - // } - - if(mode == 0) { - d_seq->addCommand(cmd->clone()); - return CommandExecuter::doCommandSingleton(cmd); - } else if(mode == 1) { // portfolio - d_seq->addCommand(cmd->clone()); - - // We currently don't support changing number of threads for each - // command, but things have been architected in a way so that this - // can be acheived with not a lot of work - Command *seqs[d_numThreads]; - - seqs[0] = cmd; - - /* variable maps and exporting */ - for(unsigned i = 1; i < d_numThreads; ++i) { - /** - * vmaps[i].d_from [x] = y means - * that in thread #0's expr manager id is y - * and in thread #i's expr manager id is x - * opposite for d_to - * - * d_from[x] : in a sense gives the id if converting *from* it to - * first thread - */ - try { - seqs[i] = d_seq->exportTo(d_exprMgrs[i], *(d_vmaps[i]) ); - }catch(ExportToUnsupportedException& e){ - return CommandExecuter::doCommandSingleton(cmd); - } - } - - /** - * Create identity variable map for the first thread, with only - * those variables which have a corresponding variable in - * another thread. (TODO: Also assert, all threads have the same - * set of variables mapped.) - */ - if(d_numThreads >= 2) { - for(typeof(d_vmaps[1]->d_to.begin()) i=d_vmaps[1]->d_to.begin(); - i!=d_vmaps[1]->d_to.end(); ++i) { - (d_vmaps[0]->d_from)[i->first] = i->first; - } - d_vmaps[0]->d_to = d_vmaps[0]->d_from; - } - - lemmaSharingInit(); - - /* Portfolio */ - boost::function fns[d_numThreads]; - for(unsigned i = 0; i < d_numThreads; ++i) { - fns[i] = boost::bind(smtEngineInvoke, - d_smts[i], - seqs[i], - d_threadOptions[i][options::out] - ); - } - - Assert(d_channelsIn.size() == d_numThreads); - Assert(d_channelsOut.size() == d_numThreads); - Assert(d_smts.size() == d_numThreads); - boost::function - smFn = boost::bind(sharingManager, - d_numThreads, - &d_channelsOut[0], - &d_channelsIn[0], - &d_smts[0]); - - pair portfolioReturn = - runPortfolio(d_numThreads, smFn, fns, true); - - d_seq = NULL; - delete d_seq; - d_seq = new CommandSequence(); - - d_lastWinner = portfolioReturn.first; - - // *d_options[options::out] - // << "Winner = " - // << portfolioReturn.first - // << std::endl; - - if(d_ostringstreams.size() != 0) { - Assert(d_numThreads == d_options[options::threads]); - Assert(portfolioReturn.first >= 0); - Assert(unsigned(portfolioReturn.first) < d_numThreads); - - *d_options[options::out] - << d_ostringstreams[portfolioReturn.first]->str(); - } - - /* cleanup this check sat specific stuff */ - lemmaSharingCleanup(); - - return portfolioReturn.second; - } else if(mode == 2) { - return smtEngineInvoke(d_smts[d_lastWinner], - cmd, - d_threadOptions[d_lastWinner][options::out]); - } else { - Unreachable(); - } - -} - -std::string CommandExecuterPortfolio::getSmtEngineStatus() -{ - return d_smts[d_lastWinner]->getInfo("status").getValue(); -} - -}/*main namespace*/ -}/*CVC4 namespace*/ diff --git a/src/main/command_executer_portfolio.h b/src/main/command_executer_portfolio.h deleted file mode 100644 index db9db6509..000000000 --- a/src/main/command_executer_portfolio.h +++ /dev/null @@ -1,69 +0,0 @@ -/********************* */ -/*! \file command_executer_portfolio.h - ** \verbatim - ** Original author: kshitij - ** Major contributors: none - ** Minor contributors (to current version): - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief An additional layer between commands and invoking them. - ** - ** The portfolio executer branches check-sat queries to several - ** threads. - **/ - -#ifndef __CVC4__COMMAND_EXECUTER_PORTFOLIO_H -#define __CVC4__COMMAND_EXECUTER_PORTFOLIO_H - -#include "main/command_executer.h" -#include "main/portfolio_util.h" - -namespace CVC4 { - -class CommandSequence; - -namespace main { - -class CommandExecuterPortfolio : public CommandExecuter { - - // These shall be created/deleted during initalization - std::vector d_exprMgrs; - const unsigned d_numThreads; // Currently const, but designed so it is - // not too hard to support this changing - std::vector d_smts; - CommandSequence* d_seq; - std::vector& d_threadOptions; - std::vector d_vmaps; - - int d_lastWinner; - - // These shall be reset for each check-sat - std::vector< SharedChannel* > d_channelsOut; - std::vector< SharedChannel* > d_channelsIn; - std::vector d_ostringstreams; - -public: - CommandExecuterPortfolio(ExprManager &exprMgr, - Options &options, - std::vector& tOpts); - - ~CommandExecuterPortfolio(); - - std::string getSmtEngineStatus(); -protected: - bool doCommandSingleton(Command* cmd); -private: - CommandExecuterPortfolio(); - void lemmaSharingInit(); - void lemmaSharingCleanup(); -}; - -}/*main namespace*/ -}/*CVC4 namespace*/ - -#endif /* __CVC4__COMMAND_EXECUTER_PORTFOLIO_H */ diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp new file mode 100644 index 000000000..1bffd5e35 --- /dev/null +++ b/src/main/command_executor.cpp @@ -0,0 +1,93 @@ +/********************* */ +/*! \file command_executor.cpp + ** \verbatim + ** Original author: kshitij + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief An additional layer between commands and invoking them. + **/ + +#include + +#include "main/command_executor.h" +#include "expr/command.h" + +#include "main/main.h" + +namespace CVC4 { +namespace main { + + +CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options): + d_exprMgr(exprMgr), + d_smtEngine(SmtEngine(&exprMgr)), + d_options(options) { + + // signal handlers need access + main::pStatistics = d_smtEngine.getStatisticsRegistry(); + d_exprMgr.getStatisticsRegistry()->setName("ExprManager"); + main::pStatistics->registerStat_(d_exprMgr.getStatisticsRegistry()); +} + +bool CommandExecutor::doCommand(Command* cmd) +{ + if( d_options[options::parseOnly] ) { + return true; + } + + CommandSequence *seq = dynamic_cast(cmd); + if(seq != NULL) { + // assume no error + bool status = true; + + for(CommandSequence::iterator subcmd = seq->begin(); + status && subcmd != seq->end(); + ++subcmd) { + status = doCommand(*subcmd); + } + + return status; + } else { + if(d_options[options::verbosity] > 0) { + *d_options[options::out] << "Invoking: " << *cmd << std::endl; + } + + return doCommandSingleton(cmd); + } +} + +bool CommandExecutor::doCommandSingleton(Command *cmd) +{ + bool status = true; + if(d_options[options::verbosity] >= 0) { + status = smtEngineInvoke(&d_smtEngine, cmd, d_options[options::out]); + } else { + status = smtEngineInvoke(&d_smtEngine, cmd, NULL); + } + return status; +} + +std::string CommandExecutor::getSmtEngineStatus() +{ + return d_smtEngine.getInfo("status").getValue(); +} + +bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out) +{ + if(out == NULL) { + cmd->invoke(smt); + } else { + cmd->invoke(smt, *out); + } + return !cmd->fail(); +} + +}/*main namespace*/ +}/*CVC4 namespace*/ diff --git a/src/main/command_executor.h b/src/main/command_executor.h new file mode 100644 index 000000000..273225e69 --- /dev/null +++ b/src/main/command_executor.h @@ -0,0 +1,67 @@ +/********************* */ +/*! \file command_executor.h + ** \verbatim + ** Original author: kshitij + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief An additional layer between commands and invoking them. + **/ + +#ifndef __CVC4__MAIN__COMMAND_EXECUTOR_H +#define __CVC4__MAIN__COMMAND_EXECUTOR_H + +#include "expr/expr_manager.h" +#include "smt/smt_engine.h" + +namespace CVC4 { +namespace main { + +class CommandExecutor { + +protected: + ExprManager& d_exprMgr; + SmtEngine d_smtEngine; + Options& d_options; + +public: + // Note: though the options are not cached (instead a reference is + // used), the portfolio command executer currently parses them + // during initalization, creating thread-specific options and + // storing them + CommandExecutor(ExprManager &exprMgr, Options &options); + + ~CommandExecutor() {} + + /** + * Executes a command. Recursively handles if cmd is a command + * sequence. Eventually uses doCommandSingleton (which can be + * overridden by a derived class). + */ + bool doCommand(CVC4::Command* cmd); + + virtual std::string getSmtEngineStatus(); + +protected: + /** Executes treating cmd as a singleton */ + virtual bool doCommandSingleton(CVC4::Command* cmd); + +private: + CommandExecutor(); + +};/* class CommandExecutor */ + +bool smtEngineInvoke(SmtEngine* smt, + Command* cmd, + std::ostream *out); + +}/* CVC4::main namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__MAIN__COMMAND_EXECUTOR_H */ diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp new file mode 100644 index 000000000..045cac8f1 --- /dev/null +++ b/src/main/command_executor_portfolio.cpp @@ -0,0 +1,314 @@ +/********************* */ +/*! \file command_executor_portfolio.cpp + ** \verbatim + ** Original author: kshitij + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief An additional layer between commands and invoking them. + ** + ** The portfolio executer branches check-sat queries to several + ** threads. + **/ + +#include +#include +#include +#include + +#include "expr/command.h" +#include "expr/pickler.h" +#include "main/command_executor_portfolio.h" +#include "main/main.h" +#include "main/options.h" +#include "main/portfolio.h" +#include "options/options.h" +#include "smt/options.h" + +using namespace std; + +namespace CVC4 { +namespace main { + +CommandExecutorPortfolio::CommandExecutorPortfolio +(ExprManager &exprMgr, Options &options, vector& tOpts): + CommandExecutor(exprMgr, options), + d_numThreads(options[options::threads]), + d_smts(), + d_seq(new CommandSequence()), + d_threadOptions(tOpts), + d_vmaps(), + d_lastWinner(0), + d_channelsOut(), + d_channelsIn(), + d_ostringstreams() +{ + Assert(d_threadOptions.size() == d_numThreads); + + /* Duplication, Individualisation */ + 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])); + } + + for(unsigned i = 1; i < d_numThreads; ++i) { + // Register the statistics registry of the thread + string emTag = "ExprManager thread #" + + boost::lexical_cast(d_threadOptions[i][options::thread_id]); + string smtTag = "SmtEngine thread #" + + boost::lexical_cast(d_threadOptions[i][options::thread_id]); + d_exprMgrs[i]->getStatisticsRegistry()->setName(emTag); + d_smts[i]->getStatisticsRegistry()->setName(smtTag); + pStatistics->registerStat_ + (d_exprMgrs[i]->getStatisticsRegistry() ); + pStatistics->registerStat_ + (d_smts[i]->getStatisticsRegistry() ); + } + + Assert(d_vmaps.size() == 0); + for(unsigned i = 0; i < d_numThreads; ++i) { + d_vmaps.push_back(new ExprManagerMapCollection()); + } + + +} + +CommandExecutorPortfolio::~CommandExecutorPortfolio() +{ + Assert(d_seq != NULL); + delete d_seq; + + Assert(d_smts.size() == d_numThreads); + for(unsigned i = 1; i < d_numThreads; ++i) { + // the 0-th one is responsibility of parent class + + delete d_exprMgrs[i]; + delete d_smts[i]; + } + d_exprMgrs.clear(); + d_smts.clear(); +} + +void CommandExecutorPortfolio::lemmaSharingInit() +{ + /* Sharing channels */ + Assert(d_channelsIn.size() == 0); + Assert(d_channelsOut.size() == 0); + + if(d_numThreads == 1) { + // Disable sharing + d_threadOptions[0].set(options::sharingFilterByLength, 0); + } else { + // Setup sharing channels + const unsigned int sharingChannelSize = 1000000; + + for(unsigned i = 0; i < d_numThreads; ++i){ + if(Debug.isOn("channel-empty")) { + d_channelsOut.push_back + (new EmptySharedChannel(sharingChannelSize)); + d_channelsIn.push_back + (new EmptySharedChannel(sharingChannelSize)); + continue; + } + d_channelsOut.push_back + (new SynchronizedSharedChannel(sharingChannelSize)); + d_channelsIn.push_back + (new SynchronizedSharedChannel(sharingChannelSize)); + } + + /* Lemma I/O channels */ + for(unsigned i = 0; i < d_numThreads; ++i) { + string tag = "thread #" + + boost::lexical_cast(d_threadOptions[i][options::thread_id]); + d_threadOptions[i].set + (options::lemmaOutputChannel, + new PortfolioLemmaOutputChannel(tag, d_channelsOut[i], d_exprMgrs[i], + d_vmaps[i]->d_from, d_vmaps[i]->d_to)); + d_threadOptions[i].set + (options::lemmaInputChannel, + new PortfolioLemmaInputChannel(tag, d_channelsIn[i], d_exprMgrs[i], + d_vmaps[i]->d_from, d_vmaps[i]->d_to)); + } + + /* Output to string stream */ + if(d_options[options::verbosity] == 0 + || d_options[options::separateOutput]) { + Assert(d_ostringstreams.size() == 0); + for(unsigned i = 0; i < d_numThreads; ++i) { + d_ostringstreams.push_back(new ostringstream); + d_threadOptions[i].set(options::out, d_ostringstreams[i]); + } + } + } +} + +void CommandExecutorPortfolio::lemmaSharingCleanup() +{ + Assert(d_numThreads == d_options[options::threads]); + + // Channel cleanup + Assert(d_channelsIn.size() == d_numThreads); + Assert(d_channelsOut.size() == d_numThreads); + for(unsigned i = 0; i < d_numThreads; ++i) { + delete d_channelsIn[i]; + delete d_channelsOut[i]; + d_threadOptions[i].set(options::lemmaInputChannel, NULL); + d_threadOptions[i].set(options::lemmaOutputChannel, NULL); + } + d_channelsIn.clear(); + d_channelsOut.clear(); + + // sstreams cleanup (if used) + if(d_ostringstreams.size() != 0) { + Assert(d_ostringstreams.size() == d_numThreads); + for(unsigned i = 0; i < d_numThreads; ++i) { + d_threadOptions[i].set(options::out, d_options[options::out]); + delete d_ostringstreams[i]; + } + d_ostringstreams.clear(); + } + +} + +bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) +{ + /** + * save the command and if check sat or query command, run a + * porfolio of SMT solvers. + */ + + int mode = 0; + // mode = 0 : run the first thread + // mode = 1 : run a porfolio + // mode = 2 : run the last winner + + // if(dynamic_cast(cmd) != NULL || + // dynamic_cast(cmd) != NULL) { + // mode = 1; + // } else if(dynamic_cast(cmd) != NULL) { + // mode = 2; + // } + + if(mode == 0) { + d_seq->addCommand(cmd->clone()); + return CommandExecutor::doCommandSingleton(cmd); + } else if(mode == 1) { // portfolio + d_seq->addCommand(cmd->clone()); + + // We currently don't support changing number of threads for each + // command, but things have been architected in a way so that this + // can be acheived with not a lot of work + Command *seqs[d_numThreads]; + + seqs[0] = cmd; + + /* variable maps and exporting */ + for(unsigned i = 1; i < d_numThreads; ++i) { + /** + * vmaps[i].d_from [x] = y means + * that in thread #0's expr manager id is y + * and in thread #i's expr manager id is x + * opposite for d_to + * + * d_from[x] : in a sense gives the id if converting *from* it to + * first thread + */ + try { + seqs[i] = d_seq->exportTo(d_exprMgrs[i], *(d_vmaps[i]) ); + }catch(ExportToUnsupportedException& e){ + return CommandExecutor::doCommandSingleton(cmd); + } + } + + /** + * Create identity variable map for the first thread, with only + * those variables which have a corresponding variable in + * another thread. (TODO: Also assert, all threads have the same + * set of variables mapped.) + */ + if(d_numThreads >= 2) { + for(typeof(d_vmaps[1]->d_to.begin()) i=d_vmaps[1]->d_to.begin(); + i!=d_vmaps[1]->d_to.end(); ++i) { + (d_vmaps[0]->d_from)[i->first] = i->first; + } + d_vmaps[0]->d_to = d_vmaps[0]->d_from; + } + + lemmaSharingInit(); + + /* Portfolio */ + boost::function fns[d_numThreads]; + for(unsigned i = 0; i < d_numThreads; ++i) { + fns[i] = boost::bind(smtEngineInvoke, + d_smts[i], + seqs[i], + d_threadOptions[i][options::out] + ); + } + + Assert(d_channelsIn.size() == d_numThreads); + Assert(d_channelsOut.size() == d_numThreads); + Assert(d_smts.size() == d_numThreads); + boost::function + smFn = boost::bind(sharingManager, + d_numThreads, + &d_channelsOut[0], + &d_channelsIn[0], + &d_smts[0]); + + pair portfolioReturn = + runPortfolio(d_numThreads, smFn, fns, true); + + d_seq = NULL; + delete d_seq; + d_seq = new CommandSequence(); + + d_lastWinner = portfolioReturn.first; + + // *d_options[options::out] + // << "Winner = " + // << portfolioReturn.first + // << std::endl; + + if(d_ostringstreams.size() != 0) { + Assert(d_numThreads == d_options[options::threads]); + Assert(portfolioReturn.first >= 0); + Assert(unsigned(portfolioReturn.first) < d_numThreads); + + *d_options[options::out] + << d_ostringstreams[portfolioReturn.first]->str(); + } + + /* cleanup this check sat specific stuff */ + lemmaSharingCleanup(); + + return portfolioReturn.second; + } else if(mode == 2) { + return smtEngineInvoke(d_smts[d_lastWinner], + cmd, + d_threadOptions[d_lastWinner][options::out]); + } else { + Unreachable(); + } + +} + +std::string CommandExecutorPortfolio::getSmtEngineStatus() +{ + return d_smts[d_lastWinner]->getInfo("status").getValue(); +} + +}/*main namespace*/ +}/*CVC4 namespace*/ diff --git a/src/main/command_executor_portfolio.h b/src/main/command_executor_portfolio.h new file mode 100644 index 000000000..cc0a77698 --- /dev/null +++ b/src/main/command_executor_portfolio.h @@ -0,0 +1,69 @@ +/********************* */ +/*! \file command_executor_portfolio.h + ** \verbatim + ** Original author: kshitij + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief An additional layer between commands and invoking them. + ** + ** The portfolio executer branches check-sat queries to several + ** threads. + **/ + +#ifndef __CVC4__MAIN__COMMAND_EXECUTOR_PORTFOLIO_H +#define __CVC4__MAIN__COMMAND_EXECUTOR_PORTFOLIO_H + +#include "main/command_executor.h" +#include "main/portfolio_util.h" + +namespace CVC4 { + +class CommandSequence; + +namespace main { + +class CommandExecutorPortfolio : public CommandExecutor { + + // These shall be created/deleted during initalization + std::vector d_exprMgrs; + const unsigned d_numThreads; // Currently const, but designed so it is + // not too hard to support this changing + std::vector d_smts; + CommandSequence* d_seq; + std::vector& d_threadOptions; + std::vector d_vmaps; + + int d_lastWinner; + + // These shall be reset for each check-sat + std::vector< SharedChannel* > d_channelsOut; + std::vector< SharedChannel* > d_channelsIn; + std::vector d_ostringstreams; + +public: + CommandExecutorPortfolio(ExprManager &exprMgr, + Options &options, + std::vector& tOpts); + + ~CommandExecutorPortfolio(); + + std::string getSmtEngineStatus(); +protected: + bool doCommandSingleton(Command* cmd); +private: + CommandExecutorPortfolio(); + void lemmaSharingInit(); + void lemmaSharingCleanup(); +};/* class CommandExecutorPortfolio */ + +}/* CVC4::main namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__MAIN__COMMAND_EXECUTOR_PORTFOLIO_H */ diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 061e34223..f91f951c6 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -35,9 +35,9 @@ #include "util/Assert.h" #include "util/configuration.h" #include "options/options.h" -#include "main/command_executer.h" +#include "main/command_executor.h" # ifdef PORTFOLIO_BUILD -# include "main/command_executer_portfolio.h" +# include "main/command_executor_portfolio.h" # endif #include "main/options.h" #include "smt/options.h" @@ -226,11 +226,11 @@ int runCvc4(int argc, char* argv[], Options& opts) { ExprManager exprMgr(threadOpts[0]); # endif - CommandExecuter* cmdExecuter = + CommandExecutor* cmdExecutor = # ifndef PORTFOLIO_BUILD - new CommandExecuter(exprMgr, opts); + new CommandExecutor(exprMgr, opts); # else - new CommandExecuterPortfolio(exprMgr, opts, threadOpts); + new CommandExecutorPortfolio(exprMgr, opts, threadOpts); #endif // Create the SmtEngine @@ -280,7 +280,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { replayParser->useDeclarationsFrom(shell.getParser()); } while((cmd = shell.readCommand())) { - status = cmdExecuter->doCommand(cmd) && status; + status = cmdExecutor->doCommand(cmd) && status; delete cmd; } } else { @@ -304,7 +304,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { delete cmd; break; } - status = cmdExecuter->doCommand(cmd); + status = cmdExecutor->doCommand(cmd); delete cmd; } // Remove the parser @@ -320,7 +320,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { int returnValue; string result = "unknown"; if(status) { - result = cmdExecuter->getSmtEngineStatus(); + result = cmdExecutor->getSmtEngineStatus(); if(result == "sat") { returnValue = 10; diff --git a/src/main/portfolio_util.cpp b/src/main/portfolio_util.cpp index bad532d30..b208b2479 100644 --- a/src/main/portfolio_util.cpp +++ b/src/main/portfolio_util.cpp @@ -15,6 +15,7 @@ **/ #include +#include #include "options/options.h" #include "main/options.h" #include "prop/options.h" diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h index eed993b9f..1955a29a7 100644 --- a/src/main/portfolio_util.h +++ b/src/main/portfolio_util.h @@ -14,8 +14,8 @@ ** \brief Code relevant only for portfolio builds **/ -#ifndef __CVC4_PORTFOLIO_UTIL_H -#define __CVC4_PORTFOLIO_UTIL_H +#ifndef __CVC4__PORTFOLIO_UTIL_H +#define __CVC4__PORTFOLIO_UTIL_H #include @@ -37,7 +37,7 @@ public: T pop() { return T(); } bool empty() { return true; } bool full() { return false; } -}; +};/* class EmptySharedChannel */ class PortfolioLemmaOutputChannel : public LemmaOutputChannel { private: @@ -202,8 +202,8 @@ void sharingManager(unsigned numThreads, } Trace("sharing") << "sharing: Interrupted, exiting." << std::endl; -} +}/* sharingManager() */ -}/*CVC4 namespace*/ +}/* CVC4 namespace */ -#endif /* __CVC4_PORTFOLIO_UTIL_H */ +#endif /* __CVC4__PORTFOLIO_UTIL_H */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 281645317..a82e1b735 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -272,8 +272,6 @@ bool PropEngine::isRunning() const { void PropEngine::interrupt() throw(ModalException) { if(! d_inCheckSat) { return; - throw ModalException("SAT solver is not currently solving anything; " - "cannot interrupt it"); } d_interrupted = true; diff --git a/src/util/channel.h b/src/util/channel.h index eae7a4f11..4a07f265d 100644 --- a/src/util/channel.h +++ b/src/util/channel.h @@ -17,6 +17,8 @@ ** \todo document this file **/ +#include "cvc4_public.h" + #ifndef __CVC4__CHANNEL_H #define __CVC4__CHANNEL_H @@ -31,12 +33,13 @@ namespace CVC4 { template -class SharedChannel { +class CVC4_PUBLIC SharedChannel { private: int d_maxsize; // just call it size? public: SharedChannel() {} SharedChannel(int maxsize) : d_maxsize(maxsize) {} + virtual ~SharedChannel() {} /* Tries to add element and returns true if successful */ virtual bool push(const T&) = 0; @@ -59,7 +62,7 @@ http://live.boost.org/doc/libs/1_46_1/libs/circular_buffer/doc/circular_buffer.h and is covered by the Boost Software License, version 1.0. */ template -class SynchronizedSharedChannel : public SharedChannel { +class CVC4_PUBLIC SynchronizedSharedChannel : public SharedChannel { public: typedef boost::circular_buffer container_type; typedef typename container_type::size_type size_type; @@ -108,6 +111,6 @@ private: boost::condition m_not_full; };/* class SynchronizedSharedChannel */ -} +}/* CVC4 namespace */ #endif /* __CVC4__CHANNEL_H */