From cfa9e2cbbdf77a325791b5548b41093a0781311c Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Sat, 8 Sep 2012 14:25:25 +0000 Subject: [PATCH] Single driver for both sequential and portfolio A "command executer" layer between parsing commands and invoking them. New implementation of portfolio driver splits only when check-sat or query command is encountered, and then switches back to sequential till the next one. As side effect, restores functionality of interactive mode and push/pops. --- src/expr/command.cpp | 12 +- src/expr/command.h | 11 +- src/expr/expr_template.cpp | 14 +- src/main/Makefile.am | 10 +- src/main/command_executer.cpp | 93 +++ src/main/command_executer.h | 69 ++ src/main/command_executer_portfolio.cpp | 314 ++++++++ src/main/command_executer_portfolio.h | 69 ++ src/main/driver_portfolio.cpp | 833 -------------------- src/main/{driver.cpp => driver_unified.cpp} | 76 +- src/main/portfolio.cpp | 36 +- src/main/portfolio.h | 6 +- src/main/portfolio_util.cpp | 104 +++ src/main/portfolio_util.h | 209 +++++ src/prop/prop_engine.cpp | 1 + 15 files changed, 944 insertions(+), 913 deletions(-) create mode 100644 src/main/command_executer.cpp create mode 100644 src/main/command_executer.h create mode 100644 src/main/command_executer_portfolio.cpp create mode 100644 src/main/command_executer_portfolio.h delete mode 100644 src/main/driver_portfolio.cpp rename src/main/{driver.cpp => driver_unified.cpp} (88%) create mode 100644 src/main/portfolio_util.cpp create mode 100644 src/main/portfolio_util.h diff --git a/src/expr/command.cpp b/src/expr/command.cpp index b058292f3..1e4a266a5 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -419,7 +419,9 @@ CommandSequence::const_iterator CommandSequence::begin() const throw() { Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { CommandSequence* seq = new CommandSequence(); for(iterator i = begin(); i != end(); ++i) { - seq->addCommand((*i)->exportTo(exprManager, variableMap)); + Command* cmd_to_export = *i; + Command* cmd = cmd_to_export->exportTo(exprManager, variableMap); + seq->addCommand(cmd); } seq->d_index = d_index; return seq; @@ -1197,8 +1199,12 @@ void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() { } Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - Warning() << "We currently do not support exportTo with Datatypes" << std::endl; - return NULL; + throw ExportToUnsupportedException(); + // vector params; + // transform(d_datatypes.begin(), d_datatypes.end(), back_inserter(params), + // ExportTransformer(exprManager, variableMap)); + // DatatypeDeclarationCommand* c = new DatatypeDeclarationCommand(params); + // return c; } Command* DatatypeDeclarationCommand::clone() const { diff --git a/src/expr/command.h b/src/expr/command.h index 0f517e7f2..3c919c374 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -50,6 +50,14 @@ 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 { +public: + ExportToUnsupportedException() throw() : + Exception("exportTo unsupported for command") { + } +};/* class NoMoreValuesException */ + + /** The status an SMT benchmark can have */ enum BenchmarkStatus { /** Benchmark is satisfiable */ @@ -233,7 +241,8 @@ public: * variableMap for the translation and extending it with any new * mappings. */ - virtual Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) = 0; + virtual Command* exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) = 0; /** * Clone this Command (make a shallow copy). diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index a6f9f2cf6..4009bc610 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -131,7 +131,19 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC // temporarily set the node manager to NULL; this gets around // a check that mkVar isn't called internally NodeManagerScope nullScope(NULL); - to_e = to->mkVar(name, type);// FIXME thread safety + + if(n.getKind() == kind::BOUND_VAR_LIST) { + to_e = to->mkBoundVar(name, type);// FIXME thread safety + } 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 + } else { + Unhandled(); + } + Debug("export") << "+ exported var `" << from_e << "'[" << from_e.getId() << "] with name `" << name << "' and type `" << from_e.getType() << "' to `" << to_e << "'[" << to_e.getId() << "] with type `" << type << "'" << std::endl; } else { // temporarily set the node manager to NULL; this gets around diff --git a/src/main/Makefile.am b/src/main/Makefile.am index c1291e7ec..9b0200231 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -19,14 +19,17 @@ pcvc4_SOURCES = \ main.cpp \ portfolio.cpp \ portfolio.h \ - driver_portfolio.cpp + portfolio_util.cpp \ + command_executer.cpp \ + command_executer_portfolio.cpp \ + driver_unified.cpp pcvc4_LDADD = \ libmain.a \ @builddir@/../parser/libcvc4parser.la \ @builddir@/../libcvc4.la \ @builddir@/../lib/libreplacements.la \ $(READLINE_LIBS) -pcvc4_CPPFLAGS = $(AM_CPPFLAGS) $(BOOST_CPPFLAGS) +pcvc4_CPPFLAGS = $(AM_CPPFLAGS) $(BOOST_CPPFLAGS) -DPORTFOLIO_BUILD pcvc4_LDADD += $(BOOST_THREAD_LIBS) -lpthread pcvc4_LDADD += $(BOOST_THREAD_LDFLAGS) @@ -39,7 +42,8 @@ endif cvc4_SOURCES = \ main.cpp \ - driver.cpp + command_executer.cpp \ + driver_unified.cpp cvc4_LDADD = \ libmain.a \ @builddir@/../parser/libcvc4parser.la \ diff --git a/src/main/command_executer.cpp b/src/main/command_executer.cpp new file mode 100644 index 000000000..039ab664c --- /dev/null +++ b/src/main/command_executer.cpp @@ -0,0 +1,93 @@ +/********************* */ +/*! \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 new file mode 100644 index 000000000..245857c04 --- /dev/null +++ b/src/main/command_executer.h @@ -0,0 +1,69 @@ +/********************* */ +/*! \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 new file mode 100644 index 000000000..85180c9a9 --- /dev/null +++ b/src/main/command_executer_portfolio.cpp @@ -0,0 +1,314 @@ +/********************* */ +/*! \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 new file mode 100644 index 000000000..db9db6509 --- /dev/null +++ b/src/main/command_executer_portfolio.h @@ -0,0 +1,69 @@ +/********************* */ +/*! \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/driver_portfolio.cpp b/src/main/driver_portfolio.cpp deleted file mode 100644 index 648c6c9f9..000000000 --- a/src/main/driver_portfolio.cpp +++ /dev/null @@ -1,833 +0,0 @@ -/********************* */ -/*! \file driver_portfolio.cpp - ** \verbatim - ** Original author: kshitij - ** Major contributors: taking, mdeters - ** 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 Driver for portfolio CVC4 executable (pcvc4) - ** - ** Driver for portfolio CVC4 executable (pcvc4). - **/ - -#include -#include -#include -#include // for gettimeofday() - -#include - -#include -#include -#include -#include - -#include "cvc4autoconfig.h" -#include "main/main.h" -#include "main/interactive_shell.h" -#include "parser/parser.h" -#include "parser/parser_builder.h" -#include "parser/parser_exception.h" -#include "expr/expr_manager.h" -#include "expr/variable_type_map.h" -#include "smt/smt_engine.h" -#include "expr/command.h" -#include "util/Assert.h" -#include "util/configuration.h" -#include "options/options.h" -#include "main/options.h" -#include "smt/options.h" -#include "prop/options.h" -#include "theory/uf/options.h" -#include "util/output.h" -#include "util/dump.h" -#include "util/result.h" -#include "util/stats.h" -#include "util/lemma_input_channel.h" -#include "util/lemma_output_channel.h" - -#include "expr/pickler.h" -#include "util/channel.h" - -#include "main/portfolio.h" - -using namespace std; -using namespace CVC4; -using namespace CVC4::parser; -using namespace CVC4::main; - -/* Global variables */ - -namespace CVC4 { - namespace main { - - StatisticsRegistry theStatisticsRegistry; - - /** A pointer to the StatisticsRegistry (the signal handlers need it) */ - CVC4::StatisticsRegistry* pStatistics; - - }/* CVC4::main namespace */ -}/* CVC4 namespace */ - -/* Function declarations */ - -static bool doCommand(SmtEngine&, Command*, Options&); - -Result doSmt(SmtEngine &smt, Command *cmd, Options &options); - -template -void sharingManager(unsigned numThreads, - SharedChannel* channelsOut[], - SharedChannel* channelsIn[], - SmtEngine* smts[]); - - -/* To monitor for activity on shared channels */ -bool global_activity; -bool global_activity_true() { return global_activity; } -bool global_activity_false() { return not global_activity; } -boost::condition global_activity_cond; - -typedef expr::pickle::Pickle channelFormat; /* Remove once we are using Pickle */ - -template -class EmptySharedChannel: public SharedChannel { -public: - EmptySharedChannel(int) {} - bool push(const T&) { return true; } - T pop() { return T(); } - bool empty() { return true; } - bool full() { return false; } -}; - -class PortfolioLemmaOutputChannel : public LemmaOutputChannel { -private: - string d_tag; - SharedChannel* d_sharedChannel; - expr::pickle::MapPickler d_pickler; - -public: - int cnt; - PortfolioLemmaOutputChannel(string tag, - SharedChannel *c, - ExprManager* em, - VarMap& to, - VarMap& from) : - d_tag(tag), - d_sharedChannel(c), - d_pickler(em, to, from) - ,cnt(0) - {} - - void notifyNewLemma(Expr lemma) { - if(Debug.isOn("disable-lemma-sharing")) { - return; - } - if(options::sharingFilterByLength() >= 0) { // 0 would mean no-sharing effectively - if(int(lemma.getNumChildren()) > options::sharingFilterByLength()) { - return; - } - } - ++cnt; - Trace("sharing") << d_tag << ": " << lemma << endl; - expr::pickle::Pickle pkl; - try { - d_pickler.toPickle(lemma, pkl); - d_sharedChannel->push(pkl); - if(Trace.isOn("showSharing") && options::thread_id() == 0) { - *options::out() << "thread #0: notifyNewLemma: " << lemma << endl; - } - } catch(expr::pickle::PicklingException& p){ - Trace("sharing::blocked") << lemma << endl; - } - } - -}; - -/* class PortfolioLemmaInputChannel */ -class PortfolioLemmaInputChannel : public LemmaInputChannel { -private: - string d_tag; - SharedChannel* d_sharedChannel; - expr::pickle::MapPickler d_pickler; - -public: - PortfolioLemmaInputChannel(string tag, - SharedChannel* c, - ExprManager* em, - VarMap& to, - VarMap& from) : - d_tag(tag), - d_sharedChannel(c), - d_pickler(em, to, from){ - } - - bool hasNewLemma(){ - Debug("lemmaInputChannel") << d_tag << ": " << "hasNewLemma" << endl; - return !d_sharedChannel->empty(); - } - - Expr getNewLemma() { - Debug("lemmaInputChannel") << d_tag << ": " << "getNewLemma" << endl; - expr::pickle::Pickle pkl = d_sharedChannel->pop(); - - Expr e = d_pickler.fromPickle(pkl); - if(Trace.isOn("showSharing") && options::thread_id() == 0) { - *options::out() << "thread #0: getNewLemma: " << e << endl; - } - return e; - } - -};/* class PortfolioLemmaInputChannel */ - - - -int runCvc4(int argc, char *argv[], Options& opts) { - -#ifdef CVC4_CLN_IMP - Warning() << "WARNING:" << endl - << "WARNING: This build of portfolio-CVC4 uses the CLN library" << endl - << "WARNING: which is not thread-safe! Expect crashes and" << endl - << "WARNING: incorrect answers." << endl - << "WARNING:" << endl; -#endif /* CVC4_CLN_IMP */ - - /************************************************************************** - * runCvc4 outline: - * -> Start a couple of timers - * -> Processing of options, including thread specific ones - * -> Statistics related stuff - * -> Create ExprManager, parse commands, duplicate exprMgrs using export - * -> Create smtEngines - * -> Lemma sharing init - * -> Run portfolio, exit/print stats etc. - * (This list might become outdated, a timestamp might be good: 7 Dec '11.) - **************************************************************************/ - - // Timer statistic - TimerStat s_totalTime("totalTime"); - TimerStat s_beforePortfolioTime("beforePortfolioTime"); - s_totalTime.start(); - s_beforePortfolioTime.start(); - - // For the signal handlers' benefit - pOptions = &opts; - - // Initialize the signal handlers - cvc4_init(); - - progPath = argv[0]; - - - /****************************** Options Processing ************************/ - - // Parse the options - int firstArgIndex = opts.parseOptions(argc, argv); - - progName = opts[options::binary_name].c_str(); - - if( opts[options::help] ) { - printUsage(opts, true); - exit(1); - } else if( opts[options::languageHelp] ) { - Options::printLanguageHelp(*opts[options::out]); - exit(1); - } else if( opts[options::version] ) { - *opts[options::out] << Configuration::about().c_str() << flush; - exit(0); - } - - unsigned numThreads = opts[options::threads]; - - if(opts[options::threadArgv].size() > size_t(numThreads)) { - stringstream ss; - ss << "--thread" << (opts[options::threadArgv].size() - 1) - << " configuration string seen but this portfolio will only contain " - << numThreads << " thread(s)!"; - throw OptionException(ss.str()); - } - - segvNoSpin = opts[options::segvNoSpin]; - - // If in competition mode, set output stream option to flush immediately -#ifdef CVC4_COMPETITION_MODE - *opts[options::out] << unitbuf; -#endif /* CVC4_COMPETITION_MODE */ - - // We only accept one input file - if(argc > firstArgIndex + 1) { - throw Exception("Too many input files specified."); - } - - // If no file supplied we will read from standard input - const bool inputFromStdin = - firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]); - - // if we're reading from stdin on a TTY, default to interactive mode - if(!opts.wasSetByUser(options::interactive)) { - opts.set(options::interactive, inputFromStdin && isatty(fileno(stdin))); - } - - // Auto-detect input language by filename extension - const char* filename = inputFromStdin ? "" : argv[firstArgIndex]; - - if(opts[options::inputLanguage] == language::input::LANG_AUTO) { - if( inputFromStdin ) { - // We can't do any fancy detection on stdin - opts.set(options::inputLanguage, language::input::LANG_CVC4); - } else { - unsigned len = strlen(filename); - if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { - opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2); - } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) { - opts.set(options::inputLanguage, language::input::LANG_SMTLIB); - } else if((len >= 2 && !strcmp(".p", filename + len - 2)) - || (len >= 5 && !strcmp(".tptp", filename + len - 5))) { - opts.set(options::inputLanguage, language::input::LANG_TPTP); - } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) - || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { - opts.set(options::inputLanguage, language::input::LANG_CVC4); - } - } - } - - // Determine which messages to show based on smtcomp_mode and verbosity - if(Configuration::isMuzzledBuild()) { - Debug.setStream(CVC4::null_os); - Trace.setStream(CVC4::null_os); - Notice.setStream(CVC4::null_os); - Chat.setStream(CVC4::null_os); - Message.setStream(CVC4::null_os); - Warning.setStream(CVC4::null_os); - Dump.setStream(CVC4::null_os); - } else { - if(opts[options::verbosity] < 2) { - Chat.setStream(CVC4::null_os); - } - if(opts[options::verbosity] < 1) { - Notice.setStream(CVC4::null_os); - } - if(opts[options::verbosity] < 0) { - Message.setStream(CVC4::null_os); - Warning.setStream(CVC4::null_os); - } - - OutputLanguage language = language::toOutputLanguage(opts[options::inputLanguage]); - Debug.getStream() << Expr::setlanguage(language); - Trace.getStream() << Expr::setlanguage(language); - Notice.getStream() << Expr::setlanguage(language); - Chat.getStream() << Expr::setlanguage(language); - Message.getStream() << Expr::setlanguage(language); - Warning.getStream() << Expr::setlanguage(language); - Dump.getStream() << Expr::setlanguage(language) - << Expr::setdepth(-1) - << Expr::printtypes(false); - } - - // important even for muzzled builds (to get result output right) - *opts[options::out] << Expr::setlanguage(opts[options::outputLanguage]); - - vector threadOptions; - for(unsigned i = 0; i < numThreads; ++i) { - threadOptions.push_back(opts); - Options& tOpts = threadOptions.back(); - - // Set thread identifier - tOpts.set(options::thread_id, i); - - // If the random-seed is negative, pick a random seed randomly - if(opts[options::satRandomSeed] < 0) { - tOpts.set(options::satRandomSeed, (double)rand()); - } - - if(i < opts[options::threadArgv].size() && !opts[options::threadArgv][i].empty()) { - // separate out the thread's individual configuration string - stringstream optidss; - optidss << "--thread" << i; - string optid = optidss.str(); - int targc = 1; - char* tbuf = strdup(opts[options::threadArgv][i].c_str()); - char* p = tbuf; - // string length is certainly an upper bound on size needed - char** targv = new char*[opts[options::threadArgv][i].size()]; - char** vp = targv; - *vp++ = strdup(optid.c_str()); - p = strtok(p, " "); - while(p != NULL) { - *vp++ = p; - ++targc; - p = strtok(NULL, " "); - } - *vp++ = NULL; - if(targc > 1) { // this is necessary in case you do e.g. --thread0=" " - try { - tOpts.parseOptions(targc, targv); - } catch(OptionException& e) { - stringstream ss; - ss << optid << ": " << e.getMessage(); - throw OptionException(ss.str()); - } - if(optind != targc) { - stringstream ss; - ss << "unused argument `" << targv[optind] - << "' in thread configuration " << optid << " !"; - throw OptionException(ss.str()); - } - if(tOpts[options::threads] != numThreads || tOpts[options::threadArgv] != opts[options::threadArgv]) { - stringstream ss; - ss << "not allowed to set thread options in " << optid << " !"; - throw OptionException(ss.str()); - } - } - free(targv[0]); - delete targv; - free(tbuf); - } - } - - // Some more options related stuff - - /* Use satRandomSeed for generating random numbers, in particular satRandomSeed-s */ - srand((unsigned int)(-opts[options::satRandomSeed])); - - assert(numThreads >= 1); //do we need this? - - /* Output to string stream */ - vector ss_out(numThreads); - if(opts[options::verbosity] == 0 || opts[options::separateOutput]) { - for(unsigned i = 0; i < numThreads; ++i) { - ss_out[i] = new stringstream; - threadOptions[i].set(options::out, ss_out[i]); - } - } - - /****************************** Driver Statistics *************************/ - - // Statistics init - pStatistics = &theStatisticsRegistry; - - StatisticsRegistry driverStatisticsRegistry("driver"); - theStatisticsRegistry.registerStat_((&driverStatisticsRegistry)); - - // Timer statistic - RegisterStatistic* statTotalTime = - new RegisterStatistic(&driverStatisticsRegistry, &s_totalTime); - RegisterStatistic* statBeforePortfolioTime = - new RegisterStatistic(&driverStatisticsRegistry, &s_beforePortfolioTime); - - // Filename statistics - ReferenceStat< const char* > s_statFilename("filename", filename); - RegisterStatistic* statFilenameReg = - new RegisterStatistic(&driverStatisticsRegistry, &s_statFilename); - - - /****************** ExprManager + CommandParsing + Export *****************/ - - // Create the expression manager - ExprManager* exprMgrs[numThreads]; - exprMgrs[0] = new ExprManager(threadOptions[0]); - ExprManager* exprMgr = exprMgrs[0]; // to avoid having to change code which uses that - - // Parse commands until we are done - Command* cmd; - // bool status = true; // Doesn't seem to be use right now: commenting it out - CommandSequence* seq = new CommandSequence(); - if( opts[options::interactive] ) { - InteractiveShell shell(*exprMgr, opts); - Message() << Configuration::getPackageName() - << " " << Configuration::getVersionString(); - if(Configuration::isSubversionBuild()) { - Message() << " [subversion " << Configuration::getSubversionBranchName() - << " r" << Configuration::getSubversionRevision() - << (Configuration::hasSubversionModifications() ? - " (with modifications)" : "") - << "]"; - } - Message() << (Configuration::isDebugBuild() ? " DEBUG" : "") - << " assertions:" - << (Configuration::isAssertionBuild() ? "on" : "off") - << endl; - while((cmd = shell.readCommand())) { - seq->addCommand(cmd); - } - } else { - ParserBuilder parserBuilder = - ParserBuilder(exprMgr, filename). - withOptions(opts); - - if( inputFromStdin ) { -#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) - parserBuilder.withStreamInput(cin); -#else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ - parserBuilder.withLineBufferedStreamInput(cin); -#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ - } - - Parser *parser = parserBuilder.build(); - while((cmd = parser->nextCommand())) { - seq->addCommand(cmd); - // doCommand(smt, cmd, opts); - // delete cmd; - } - // Remove the parser - delete parser; - } - - if(opts[options::parseOnly]) { - return 0; - } - - exprMgr = NULL; // don't want to use that variable - // after this point - - /* Duplication, Individualisation */ - ExprManagerMapCollection* vmaps[numThreads]; // vmaps[0] is generally empty - Command *seqs[numThreads]; - seqs[0] = seq; seq = NULL; - for(unsigned i = 1; i < numThreads; ++i) { - vmaps[i] = new ExprManagerMapCollection(); - exprMgrs[i] = new ExprManager(threadOptions[i]); - seqs[i] = seqs[0]->exportTo(exprMgrs[i], *(vmaps[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 - */ - - /** - * 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(numThreads >= 2) { - // Get keys from the first thread - //Set s = vmaps[1]->d_to.keys(); - vmaps[0] = new ExprManagerMapCollection(); // identity be default? - for(typeof(vmaps[1]->d_to.begin()) i=vmaps[1]->d_to.begin(); i!=vmaps[1]->d_to.end(); ++i) { - (vmaps[0]->d_from)[i->first] = i->first; - } - vmaps[0]->d_to = vmaps[0]->d_from; - } - - // Create the SmtEngine(s) - SmtEngine *smts[numThreads]; - for(unsigned i = 0; i < numThreads; ++i) { - smts[i] = new SmtEngine(exprMgrs[i]); - - // Register the statistics registry of the thread - string emTag = "ExprManager thread #" + boost::lexical_cast(threadOptions[i][options::thread_id]); - string smtTag = "SmtEngine thread #" + boost::lexical_cast(threadOptions[i][options::thread_id]); - exprMgrs[i]->getStatisticsRegistry()->setName(emTag); - smts[i]->getStatisticsRegistry()->setName(smtTag); - theStatisticsRegistry.registerStat_( exprMgrs[i]->getStatisticsRegistry() ); - theStatisticsRegistry.registerStat_( smts[i]->getStatisticsRegistry() ); - } - - /************************* Lemma sharing init ************************/ - - /* Sharing channels */ - SharedChannel *channelsOut[numThreads], *channelsIn[numThreads]; - - if(numThreads == 1) { - // Disable sharing - threadOptions[0].set(options::sharingFilterByLength, 0); - } else { - // Setup sharing channels - const unsigned int sharingChannelSize = 1000000; - - for(unsigned i = 0; i < numThreads; ++i){ - if(Debug.isOn("channel-empty")) { - channelsOut[i] = new EmptySharedChannel(sharingChannelSize); - channelsIn[i] = new EmptySharedChannel(sharingChannelSize); - continue; - } - channelsOut[i] = new SynchronizedSharedChannel(sharingChannelSize); - channelsIn[i] = new SynchronizedSharedChannel(sharingChannelSize); - } - - /* Lemma output channel */ - for(unsigned i = 0; i < numThreads; ++i) { - string tag = "thread #" + boost::lexical_cast(threadOptions[i][options::thread_id]); - threadOptions[i].set(options::lemmaOutputChannel, - new PortfolioLemmaOutputChannel(tag, channelsOut[i], exprMgrs[i], - vmaps[i]->d_from, vmaps[i]->d_to)); - threadOptions[i].set(options::lemmaInputChannel, - new PortfolioLemmaInputChannel(tag, channelsIn[i], exprMgrs[i], - vmaps[i]->d_from, vmaps[i]->d_to)); - } - } - - /************************** End of initialization ***********************/ - - /* Portfolio */ - boost::function fns[numThreads]; - - for(unsigned i = 0; i < numThreads; ++i) { - fns[i] = boost::bind(doSmt, boost::ref(*smts[i]), seqs[i], boost::ref(threadOptions[i])); - } - - boost::function - smFn = boost::bind(sharingManager, numThreads, channelsOut, channelsIn, smts); - - s_beforePortfolioTime.stop(); - pair portfolioReturn = runPortfolio(numThreads, smFn, fns, true); - int winner = portfolioReturn.first; - Result result = portfolioReturn.second; - - cout << result << endl; - - /************************* Post printing answer ***********************/ - - if(opts[options::printWinner]){ - cout << "The winner is #" << winner << endl; - } - - Result satRes = result.asSatisfiabilityResult(); - int returnValue; - if(satRes.isSat() == Result::SAT) { - returnValue = 10; - } else if(satRes.isSat() == Result::UNSAT) { - returnValue = 20; - } else { - returnValue = 0; - } - -#ifdef CVC4_COMPETITION_MODE - // exit, don't return - // (don't want destructors to run) - exit(returnValue); -#endif /* CVC4_COMPETITION_MODE */ - - // ReferenceStat< Result > s_statSatResult("sat/unsat", result); - // RegisterStatistic statSatResultReg(*exprMgr, &s_statSatResult); - - // Stop timers, enough work done - s_totalTime.stop(); - - if(opts[options::statistics]) { - pStatistics->flushInformation(*opts[options::err]); - } - - if(opts[options::separateOutput]) { - for(unsigned i = 0; i < numThreads; ++i) { - *opts[options::out] << "--- Output from thread #" << i << " ---" << endl; - *opts[options::out] << ss_out[i]->str(); - } - } - - /*if(opts[options::statistics]) { - double totalTime = double(s_totalTime.getData().tv_sec) + - double(s_totalTime.getData().tv_nsec)/1000000000.0; - cout.precision(6); - *opts[options::err] << "real time: " << totalTime << "s\n"; - int th0_lemcnt = (*static_cast(opts[options::lemmaOutputChannel])).cnt; - int th1_lemcnt = (*static_cast(threadOptions[1].lemmaOutputChannel)).cnt; - *opts[options::err] << "lemmas shared by thread #0: " << th0_lemcnt << endl; - *opts[options::err] << "lemmas shared by thread #1: " << th1_lemcnt << endl; - *opts[options::err] << "sharing rate: " << double(th0_lemcnt+th1_lemcnt)/(totalTime) - << " lem/sec" << endl; - *opts[options::err] << "winner: #" << (winner == 0 ? 0 : 1) << endl; - }*/ - - // destruction is causing segfaults, let us just exit - exit(returnValue); - - //delete vmaps; - - delete statTotalTime; - delete statBeforePortfolioTime; - delete statFilenameReg; - - // delete seq; - // delete exprMgr; - - // delete seq2; - // delete exprMgr2; - - return returnValue; -} - -/**** Code shared with driver.cpp ****/ - -namespace CVC4 { - namespace main {/* Global options variable */ - CVC4_THREADLOCAL(Options*) pOptions; - - /** Full argv[0] */ - const char *progPath; - - /** Just the basename component of argv[0] */ - const char *progName; - } -} - -void printUsage(Options& opts, bool full) { - stringstream ss; - ss << "usage: " << opts[options::binary_name] << " [options] [input-file]" << endl - << endl - << "Without an input file, or with `-', CVC4 reads from standard input." << endl - << endl - << "CVC4 options:" << endl; - if(full) { - Options::printUsage( ss.str(), *opts[options::out] ); - } else { - Options::printShortUsage( ss.str(), *opts[options::out] ); - } -} - -/** Executes a command. Deletes the command after execution. */ -static bool doCommand(SmtEngine& smt, Command* cmd, Options& opts) { - if( opts[options::parseOnly] ) { - return true; - } - - // assume no error - bool status = true; - - CommandSequence *seq = dynamic_cast(cmd); - if(seq != NULL) { - for(CommandSequence::iterator subcmd = seq->begin(); - subcmd != seq->end(); - ++subcmd) { - status = doCommand(smt, *subcmd, opts) && status; - } - } else { - if(opts[options::verbosity] > 0) { - *opts[options::out] << "Invoking: " << *cmd << endl; - } - - if(opts[options::verbosity] >= 0) { - cmd->invoke(&smt, *opts[options::out]); - } else { - cmd->invoke(&smt); - } - status = status && cmd->ok(); - } - - return status; -} - -/**** End of code shared with driver.cpp ****/ - -/** Create the SMT engine and execute the commands */ -Result doSmt(SmtEngine &smt, Command *cmd, Options &opts) { - - try { - // For the signal handlers' benefit - pOptions = &opts; - - // Execute the commands - bool status = doCommand(smt, cmd, opts); - - // if(opts[options::statistics]) { - // smt.getStatisticsRegistry()->flushInformation(*opts[options::err]); - // *opts[options::err] << "Statistics printing of my thread complete " << endl; - // } - - return status ? smt.getStatusOfLastCommand() : Result::SAT_UNKNOWN; - } catch(OptionException& e) { - *(*pOptions)[options::out] << "unknown" << endl; - cerr << "CVC4 Error:" << endl << e << endl; - printUsage(*pOptions); - } catch(Exception& e) { -#ifdef CVC4_COMPETITION_MODE - *(*pOptions)[options::out] << "unknown" << endl; -#endif - *(*pOptions)[options::err] << "CVC4 Error:" << endl << e << endl; - if((*pOptions)[options::statistics]) { - pStatistics->flushInformation(*(*pOptions)[options::err]); - } - } - return Result::SAT_UNKNOWN; -} - -template -void sharingManager(unsigned numThreads, - SharedChannel *channelsOut[], // out and in with respect - SharedChannel *channelsIn[], - SmtEngine *smts[]) // to smt engines -{ - Trace("sharing") << "sharing: thread started " << endl; - vector cnt(numThreads); // Debug("sharing") - - vector< queue > queues; - for(unsigned i = 0; i < numThreads; ++i){ - queues.push_back(queue()); - } - - const unsigned int sharingBroadcastInterval = 1; - - boost::mutex mutex_activity; - - /* Disable interruption, so that we can check manually */ - boost::this_thread::disable_interruption di; - - while(not boost::this_thread::interruption_requested()) { - - boost::this_thread::sleep(boost::posix_time::milliseconds(sharingBroadcastInterval)); - - for(unsigned t = 0; t < numThreads; ++t) { - - if(channelsOut[t]->empty()) continue; /* No activity on this channel */ - - /* Alert if channel full, so that we increase sharingChannelSize - or decrease sharingBroadcastInterval */ - Assert(not channelsOut[t]->full()); - - T data = channelsOut[t]->pop(); - - if(Trace.isOn("sharing")) { - ++cnt[t]; - Trace("sharing") << "sharing: Got data. Thread #" << t - << ". Chunk " << cnt[t] << std :: endl; - } - - for(unsigned u = 0; u < numThreads; ++u) { - if(u != t){ - Trace("sharing") << "sharing: adding to queue " << u << endl; - queues[u].push(data); - } - }/* end of inner for: broadcast activity */ - - } /* end of outer for: look for activity */ - - for(unsigned t = 0; t < numThreads; ++t){ - /* Alert if channel full, so that we increase sharingChannelSize - or decrease sharingBroadcastInterval */ - Assert(not channelsIn[t]->full()); - - while(!queues[t].empty() && !channelsIn[t]->full()){ - Trace("sharing") << "sharing: pushing on channel " << t << endl; - T data = queues[t].front(); - channelsIn[t]->push(data); - queues[t].pop(); - } - } - } /* end of infinite while */ - - Trace("interrupt") << "sharing thread interrupted, interrupting all smtEngines" << endl; - - for(unsigned t = 0; t < numThreads; ++t) { - Trace("interrupt") << "Interrupting thread #" << t << endl; - try{ - smts[t]->interrupt(); - }catch(ModalException &e){ - // It's fine, the thread is probably not there. - Trace("interrupt") << "Could not interrupt thread #" << t << endl; - } - } - - Trace("sharing") << "sharing: Interrupted, exiting." << endl; -} diff --git a/src/main/driver.cpp b/src/main/driver_unified.cpp similarity index 88% rename from src/main/driver.cpp rename to src/main/driver_unified.cpp index 1e6f87d24..061e34223 100644 --- a/src/main/driver.cpp +++ b/src/main/driver_unified.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file driver.cpp +/*! \file driver_unified.cpp ** \verbatim ** Original author: mdeters ** Major contributors: cconway @@ -11,9 +11,8 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Driver for (sequential) CVC4 executable (cvc4) - ** - ** Driver for (sequential) CVC4 executable (cvc4). + ** \brief Driver for CVC4 executable (cvc4) unified for both + ** sequential and portfolio versions **/ #include @@ -32,11 +31,14 @@ #include "parser/parser_builder.h" #include "parser/parser_exception.h" #include "expr/expr_manager.h" -#include "smt/smt_engine.h" #include "expr/command.h" #include "util/Assert.h" #include "util/configuration.h" #include "options/options.h" +#include "main/command_executer.h" +# ifdef PORTFOLIO_BUILD +# include "main/command_executer_portfolio.h" +# endif #include "main/options.h" #include "smt/options.h" #include "theory/uf/options.h" @@ -50,8 +52,6 @@ using namespace CVC4; using namespace CVC4::parser; using namespace CVC4::main; -static bool doCommand(SmtEngine&, Command*, Options&); - namespace CVC4 { namespace main { /** Global options variable */ @@ -218,12 +218,24 @@ int runCvc4(int argc, char* argv[], Options& opts) { // important even for muzzled builds (to get result output right) *opts[options::out] << Expr::setlanguage(opts[options::outputLanguage]); - // Create the expression manager + // Create the expression manager using appropriate options +# ifndef PORTFOLIO_BUILD ExprManager exprMgr(opts); +# else + vector threadOpts = parseThreadSpecificOptions(opts); + ExprManager exprMgr(threadOpts[0]); +# endif + + CommandExecuter* cmdExecuter = +# ifndef PORTFOLIO_BUILD + new CommandExecuter(exprMgr, opts); +# else + new CommandExecuterPortfolio(exprMgr, opts, threadOpts); +#endif // Create the SmtEngine StatisticsRegistry driverStats("driver"); - SmtEngine smt(&exprMgr); + pStatistics->registerStat_(&driverStats); Parser* replayParser = NULL; if( opts[options::replayFilename] != "" ) { @@ -242,12 +254,6 @@ int runCvc4(int argc, char* argv[], Options& opts) { *opts[options::replayLog] << Expr::setlanguage(opts[options::outputLanguage]) << Expr::setdepth(-1); } - // signal handlers need access - pStatistics = smt.getStatisticsRegistry(); - exprMgr.getStatisticsRegistry()->setName("ExprManager"); - pStatistics->registerStat_(exprMgr.getStatisticsRegistry()); - pStatistics->registerStat_(&driverStats); - // Timer statistic RegisterStatistic statTotalTime(&driverStats, &s_totalTime); @@ -274,7 +280,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { replayParser->useDeclarationsFrom(shell.getParser()); } while((cmd = shell.readCommand())) { - status = doCommand(smt,cmd, opts) && status; + status = cmdExecuter->doCommand(cmd) && status; delete cmd; } } else { @@ -298,7 +304,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { delete cmd; break; } - status = doCommand(smt, cmd, opts); + status = cmdExecuter->doCommand(cmd); delete cmd; } // Remove the parser @@ -314,7 +320,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { int returnValue; string result = "unknown"; if(status) { - result = smt.getInfo("status").getValue(); + result = cmdExecuter->getSmtEngineStatus(); if(result == "sat") { returnValue = 10; @@ -342,38 +348,6 @@ int runCvc4(int argc, char* argv[], Options& opts) { if(opts[options::statistics]) { pStatistics->flushInformation(*opts[options::err]); } - + exit(returnValue); return returnValue; } - -/** Executes a command. Deletes the command after execution. */ -static bool doCommand(SmtEngine& smt, Command* cmd, Options& opts) { - if( opts[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(smt, *subcmd, opts); - } - - return status; - } else { - if(opts[options::verbosity] > 0) { - *opts[options::out] << "Invoking: " << *cmd << endl; - } - - if(opts[options::verbosity] >= 0) { - cmd->invoke(&smt, *opts[options::out]); - } else { - cmd->invoke(&smt); - } - return !cmd->fail(); - } -} diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp index 10c387b14..90af26458 100644 --- a/src/main/portfolio.cpp +++ b/src/main/portfolio.cpp @@ -11,10 +11,8 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file + ** \brief Provides (somewhat) generic functionality to simulate a + ** (potentially cooperative) race **/ #include @@ -27,19 +25,18 @@ #include "util/result.h" #include "options/options.h" -using namespace boost; - namespace CVC4 { -mutex mutex_done; -mutex mutex_main_wait; -condition condition_var_main_wait; +boost::mutex mutex_done; +boost::mutex mutex_main_wait; +boost::condition condition_var_main_wait; bool global_flag_done = false; int global_winner = -1; template -void runThread(int thread_id, function threadFn, S& returnValue) { +void runThread(int thread_id, boost::function threadFn, S& returnValue) +{ returnValue = threadFn(); if( mutex_done.try_lock() ) { @@ -54,15 +51,17 @@ void runThread(int thread_id, function threadFn, S& returnValue) { template std::pair runPortfolio(int numThreads, - function driverFn, - function threadFns[], + boost::function driverFn, + boost::function threadFns[], bool optionWaitToJoin) { - thread thread_driver; - thread threads[numThreads]; + boost::thread thread_driver; + boost::thread threads[numThreads]; S threads_returnValue[numThreads]; for(int t = 0; t < numThreads; ++t) { - threads[t] = thread(bind(runThread, t, threadFns[t], ref(threads_returnValue[t]) )); + threads[t] = + boost::thread(boost::bind(runThread, t, threadFns[t], + boost::ref(threads_returnValue[t]) ) ); } if(not driverFn.empty()) @@ -87,7 +86,10 @@ std::pair runPortfolio(int numThreads, // instantiation template -std::pair -runPortfolio(int, boost::function, boost::function*, bool); +std::pair +runPortfolio(int, + boost::function, + boost::function*, + bool); }/* CVC4 namespace */ diff --git a/src/main/portfolio.h b/src/main/portfolio.h index 1a82d651b..341f243d3 100644 --- a/src/main/portfolio.h +++ b/src/main/portfolio.h @@ -11,10 +11,8 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file + ** \brief Provides (somewhat) generic functionality to simulate a + ** (potentially cooperative) race **/ #ifndef __CVC4__PORTFOLIO_H diff --git a/src/main/portfolio_util.cpp b/src/main/portfolio_util.cpp new file mode 100644 index 000000000..bad532d30 --- /dev/null +++ b/src/main/portfolio_util.cpp @@ -0,0 +1,104 @@ +/********************* */ +/*! \file portfolio_util.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 Code relevant only for portfolio builds + **/ + +#include +#include "options/options.h" +#include "main/options.h" +#include "prop/options.h" +#include "smt/options.h" + +using namespace std; + +namespace CVC4 { + +vector parseThreadSpecificOptions(Options opts) +{ + vector threadOptions; + + unsigned numThreads = opts[options::threads]; + + /** + * Use satRandomSeed for generating random numbers, in particular + * satRandomSeed-s + */ + srand((unsigned int)(-opts[options::satRandomSeed])); + + for(unsigned i = 0; i < numThreads; ++i) { + threadOptions.push_back(opts); + Options& tOpts = threadOptions.back(); + + // Set thread identifier + tOpts.set(options::thread_id, i); + + // If the random-seed is negative, pick a random seed randomly + if(opts[options::satRandomSeed] < 0) { + tOpts.set(options::satRandomSeed, (double)rand()); + } + + if(i < opts[options::threadArgv].size() && + !opts[options::threadArgv][i].empty()) { + + // separate out the thread's individual configuration string + stringstream optidss; + optidss << "--thread" << i; + string optid = optidss.str(); + int targc = 1; + char* tbuf = strdup(opts[options::threadArgv][i].c_str()); + char* p = tbuf; + // string length is certainly an upper bound on size needed + char** targv = new char*[opts[options::threadArgv][i].size()]; + char** vp = targv; + *vp++ = strdup(optid.c_str()); + p = strtok(p, " "); + while(p != NULL) { + *vp++ = p; + ++targc; + p = strtok(NULL, " "); + } + *vp++ = NULL; + if(targc > 1) { // this is necessary in case you do e.g. --thread0=" " + try { + tOpts.parseOptions(targc, targv); + } catch(OptionException& e) { + stringstream ss; + ss << optid << ": " << e.getMessage(); + throw OptionException(ss.str()); + } + if(optind != targc) { + stringstream ss; + ss << "unused argument `" << targv[optind] + << "' in thread configuration " << optid << " !"; + throw OptionException(ss.str()); + } + if(tOpts[options::threads] != numThreads + || tOpts[options::threadArgv] != opts[options::threadArgv]) { + stringstream ss; + ss << "not allowed to set thread options in " << optid << " !"; + throw OptionException(ss.str()); + } + } + free(targv[0]); + delete targv; + free(tbuf); + } + } + + Assert(numThreads >= 1); //do we need this? + + return threadOptions; +} + +}/*CVC4 namespace */ diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h new file mode 100644 index 000000000..eed993b9f --- /dev/null +++ b/src/main/portfolio_util.h @@ -0,0 +1,209 @@ +/********************* */ +/*! \file portfolio_util.h + ** \verbatim + ** Original author: kshitij + ** Major contributors: taking, 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 Code relevant only for portfolio builds + **/ + +#ifndef __CVC4_PORTFOLIO_UTIL_H +#define __CVC4_PORTFOLIO_UTIL_H + +#include + +#include "expr/pickler.h" +#include "util/channel.h" +#include "util/lemma_input_channel.h" +#include "util/lemma_output_channel.h" +#include "main/options.h" + +namespace CVC4 { + +typedef expr::pickle::Pickle ChannelFormat; + +template +class EmptySharedChannel: public SharedChannel { +public: + EmptySharedChannel(int) {} + bool push(const T&) { return true; } + T pop() { return T(); } + bool empty() { return true; } + bool full() { return false; } +}; + +class PortfolioLemmaOutputChannel : public LemmaOutputChannel { +private: + std::string d_tag; + SharedChannel* d_sharedChannel; + expr::pickle::MapPickler d_pickler; + +public: + int cnt; + PortfolioLemmaOutputChannel(std::string tag, + SharedChannel *c, + ExprManager* em, + VarMap& to, + VarMap& from) : + d_tag(tag), + d_sharedChannel(c), + d_pickler(em, to, from), + cnt(0) + {} + + void notifyNewLemma(Expr lemma) { + if(Debug.isOn("disable-lemma-sharing")) { + return; + } + if(options::sharingFilterByLength() >= 0) { + // 0 would mean no-sharing effectively + if(int(lemma.getNumChildren()) > options::sharingFilterByLength()) { + return; + } + } + ++cnt; + Trace("sharing") << d_tag << ": " << lemma << std::endl; + expr::pickle::Pickle pkl; + try { + d_pickler.toPickle(lemma, pkl); + d_sharedChannel->push(pkl); + if(Trace.isOn("showSharing") && options::thread_id() == 0) { + *options::out() << "thread #0: notifyNewLemma: " << lemma + << std::endl; + } + } catch(expr::pickle::PicklingException& p){ + Trace("sharing::blocked") << lemma << std::endl; + } + } + +};/* class PortfolioLemmaOutputChannel */ + +class PortfolioLemmaInputChannel : public LemmaInputChannel { +private: + std::string d_tag; + SharedChannel* d_sharedChannel; + expr::pickle::MapPickler d_pickler; + +public: + PortfolioLemmaInputChannel(std::string tag, + SharedChannel* c, + ExprManager* em, + VarMap& to, + VarMap& from) : + d_tag(tag), + d_sharedChannel(c), + d_pickler(em, to, from){ + } + + bool hasNewLemma(){ + Debug("lemmaInputChannel") << d_tag << ": " << "hasNewLemma" << std::endl; + return !d_sharedChannel->empty(); + } + + Expr getNewLemma() { + Debug("lemmaInputChannel") << d_tag << ": " << "getNewLemma" << std::endl; + expr::pickle::Pickle pkl = d_sharedChannel->pop(); + + Expr e = d_pickler.fromPickle(pkl); + if(Trace.isOn("showSharing") && options::thread_id() == 0) { + *options::out() << "thread #0: getNewLemma: " << e << std::endl; + } + return e; + } + +};/* class PortfolioLemmaInputChannel */ + +std::vector parseThreadSpecificOptions(Options opts); + +template +void sharingManager(unsigned numThreads, + SharedChannel *channelsOut[], // out and in with respect + SharedChannel *channelsIn[], + SmtEngine *smts[]) // to smt engines +{ + Trace("sharing") << "sharing: thread started " << std::endl; + std::vector cnt(numThreads); // Debug("sharing") + + std::vector< std::queue > queues; + for(unsigned i = 0; i < numThreads; ++i){ + queues.push_back(std::queue()); + } + + const unsigned int sharingBroadcastInterval = 1; + + boost::mutex mutex_activity; + + /* Disable interruption, so that we can check manually */ + boost::this_thread::disable_interruption di; + + while(not boost::this_thread::interruption_requested()) { + + boost::this_thread::sleep + (boost::posix_time::milliseconds(sharingBroadcastInterval)); + + for(unsigned t = 0; t < numThreads; ++t) { + + /* No activity on this channel */ + if(channelsOut[t]->empty()) continue; + + /* Alert if channel full, so that we increase sharingChannelSize + or decrease sharingBroadcastInterval */ + Assert(not channelsOut[t]->full()); + + T data = channelsOut[t]->pop(); + + if(Trace.isOn("sharing")) { + ++cnt[t]; + Trace("sharing") << "sharing: Got data. Thread #" << t + << ". Chunk " << cnt[t] << std::endl; + } + + for(unsigned u = 0; u < numThreads; ++u) { + if(u != t){ + Trace("sharing") << "sharing: adding to queue " << u << std::endl; + queues[u].push(data); + } + }/* end of inner for: broadcast activity */ + + } /* end of outer for: look for activity */ + + for(unsigned t = 0; t < numThreads; ++t){ + /* Alert if channel full, so that we increase sharingChannelSize + or decrease sharingBroadcastInterval */ + Assert(not channelsIn[t]->full()); + + while(!queues[t].empty() && !channelsIn[t]->full()){ + Trace("sharing") << "sharing: pushing on channel " << t << std::endl; + T data = queues[t].front(); + channelsIn[t]->push(data); + queues[t].pop(); + } + } + } /* end of infinite while */ + + Trace("interrupt") + << "sharing thread interrupted, interrupting all smtEngines" << std::endl; + + for(unsigned t = 0; t < numThreads; ++t) { + Trace("interrupt") << "Interrupting thread #" << t << std::endl; + try{ + smts[t]->interrupt(); + }catch(ModalException &e){ + // It's fine, the thread is probably not there. + Trace("interrupt") << "Could not interrupt thread #" << t << std::endl; + } + } + + Trace("sharing") << "sharing: Interrupted, exiting." << std::endl; +} + +}/*CVC4 namespace*/ + +#endif /* __CVC4_PORTFOLIO_UTIL_H */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 54309cd01..281645317 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -271,6 +271,7 @@ 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"); } -- 2.30.2