(this commit was certified error- and warning-free by the test-and-commit script.)
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 {
} 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();
}
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 \
cvc4_SOURCES = \
main.cpp \
- command_executer.cpp \
+ command_executor.cpp \
driver_unified.cpp
cvc4_LDADD = \
libmain.a \
+++ /dev/null
-/********************* */
-/*! \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 <iostream>
-
-#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<CommandSequence*>(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*/
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-/********************* */
-/*! \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 <boost/thread.hpp>
-#include <boost/thread/condition.hpp>
-#include <boost/exception_ptr.hpp>
-#include <boost/lexical_cast.hpp>
-
-#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<Options>& 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<string>(d_threadOptions[i][options::thread_id]);
- string smtTag = "SmtEngine thread #"
- + boost::lexical_cast<string>(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<ChannelFormat>(sharingChannelSize));
- d_channelsIn.push_back
- (new EmptySharedChannel<ChannelFormat>(sharingChannelSize));
- continue;
- }
- d_channelsOut.push_back
- (new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize));
- d_channelsIn.push_back
- (new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize));
- }
-
- /* Lemma I/O channels */
- for(unsigned i = 0; i < d_numThreads; ++i) {
- string tag = "thread #" +
- boost::lexical_cast<string>(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<CheckSatCommand*>(cmd) != NULL ||
- // dynamic_cast<QueryCommand*>(cmd) != NULL) {
- // mode = 1;
- // } else if(dynamic_cast<GetValueCommand*>(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<bool()> 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<void()>
- smFn = boost::bind(sharingManager<ChannelFormat>,
- d_numThreads,
- &d_channelsOut[0],
- &d_channelsIn[0],
- &d_smts[0]);
-
- pair<int, bool> 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*/
+++ /dev/null
-/********************* */
-/*! \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<ExprManager*> d_exprMgrs;
- const unsigned d_numThreads; // Currently const, but designed so it is
- // not too hard to support this changing
- std::vector<SmtEngine*> d_smts;
- CommandSequence* d_seq;
- std::vector<Options>& d_threadOptions;
- std::vector<ExprManagerMapCollection*> d_vmaps;
-
- int d_lastWinner;
-
- // These shall be reset for each check-sat
- std::vector< SharedChannel<ChannelFormat>* > d_channelsOut;
- std::vector< SharedChannel<ChannelFormat>* > d_channelsIn;
- std::vector<std::ostringstream*> d_ostringstreams;
-
-public:
- CommandExecuterPortfolio(ExprManager &exprMgr,
- Options &options,
- std::vector<Options>& 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 */
--- /dev/null
+/********************* */
+/*! \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 <iostream>
+
+#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<CommandSequence*>(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*/
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 <boost/thread.hpp>
+#include <boost/thread/condition.hpp>
+#include <boost/exception_ptr.hpp>
+#include <boost/lexical_cast.hpp>
+
+#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<Options>& 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<string>(d_threadOptions[i][options::thread_id]);
+ string smtTag = "SmtEngine thread #"
+ + boost::lexical_cast<string>(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<ChannelFormat>(sharingChannelSize));
+ d_channelsIn.push_back
+ (new EmptySharedChannel<ChannelFormat>(sharingChannelSize));
+ continue;
+ }
+ d_channelsOut.push_back
+ (new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize));
+ d_channelsIn.push_back
+ (new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize));
+ }
+
+ /* Lemma I/O channels */
+ for(unsigned i = 0; i < d_numThreads; ++i) {
+ string tag = "thread #" +
+ boost::lexical_cast<string>(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<CheckSatCommand*>(cmd) != NULL ||
+ // dynamic_cast<QueryCommand*>(cmd) != NULL) {
+ // mode = 1;
+ // } else if(dynamic_cast<GetValueCommand*>(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<bool()> 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<void()>
+ smFn = boost::bind(sharingManager<ChannelFormat>,
+ d_numThreads,
+ &d_channelsOut[0],
+ &d_channelsIn[0],
+ &d_smts[0]);
+
+ pair<int, bool> 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*/
--- /dev/null
+/********************* */
+/*! \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<ExprManager*> d_exprMgrs;
+ const unsigned d_numThreads; // Currently const, but designed so it is
+ // not too hard to support this changing
+ std::vector<SmtEngine*> d_smts;
+ CommandSequence* d_seq;
+ std::vector<Options>& d_threadOptions;
+ std::vector<ExprManagerMapCollection*> d_vmaps;
+
+ int d_lastWinner;
+
+ // These shall be reset for each check-sat
+ std::vector< SharedChannel<ChannelFormat>* > d_channelsOut;
+ std::vector< SharedChannel<ChannelFormat>* > d_channelsIn;
+ std::vector<std::ostringstream*> d_ostringstreams;
+
+public:
+ CommandExecutorPortfolio(ExprManager &exprMgr,
+ Options &options,
+ std::vector<Options>& 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 */
#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"
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
replayParser->useDeclarationsFrom(shell.getParser());
}
while((cmd = shell.readCommand())) {
- status = cmdExecuter->doCommand(cmd) && status;
+ status = cmdExecutor->doCommand(cmd) && status;
delete cmd;
}
} else {
delete cmd;
break;
}
- status = cmdExecuter->doCommand(cmd);
+ status = cmdExecutor->doCommand(cmd);
delete cmd;
}
// Remove the parser
int returnValue;
string result = "unknown";
if(status) {
- result = cmdExecuter->getSmtEngineStatus();
+ result = cmdExecutor->getSmtEngineStatus();
if(result == "sat") {
returnValue = 10;
**/
#include <vector>
+#include <unistd.h>
#include "options/options.h"
#include "main/options.h"
#include "prop/options.h"
** \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 <queue>
T pop() { return T(); }
bool empty() { return true; }
bool full() { return false; }
-};
+};/* class EmptySharedChannel */
class PortfolioLemmaOutputChannel : public LemmaOutputChannel {
private:
}
Trace("sharing") << "sharing: Interrupted, exiting." << std::endl;
-}
+}/* sharingManager() */
-}/*CVC4 namespace*/
+}/* CVC4 namespace */
-#endif /* __CVC4_PORTFOLIO_UTIL_H */
+#endif /* __CVC4__PORTFOLIO_UTIL_H */
void PropEngine::interrupt() throw(ModalException) {
if(! d_inCheckSat) {
return;
- throw ModalException("SAT solver is not currently solving anything; "
- "cannot interrupt it");
}
d_interrupted = true;
** \todo document this file
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__CHANNEL_H
#define __CVC4__CHANNEL_H
namespace CVC4 {
template <typename T>
-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;
and is covered by the Boost Software License, version 1.0.
*/
template <typename T>
-class SynchronizedSharedChannel : public SharedChannel<T> {
+class CVC4_PUBLIC SynchronizedSharedChannel : public SharedChannel<T> {
public:
typedef boost::circular_buffer<T> container_type;
typedef typename container_type::size_type size_type;
boost::condition m_not_full;
};/* class SynchronizedSharedChannel<T> */
-}
+}/* CVC4 namespace */
#endif /* __CVC4__CHANNEL_H */
projects / cvc5.git / commitdiff