diff options
Diffstat (limited to 'src/main/driver_portfolio.cpp')
| -rw-r--r-- | src/main/driver_portfolio.cpp | 833 |
1 files changed, 0 insertions, 833 deletions
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 <cstdio> -#include <cstdlib> -#include <iostream> -#include <sys/time.h> // for gettimeofday() - -#include <queue> - -#include <boost/thread.hpp> -#include <boost/thread/condition.hpp> -#include <boost/exception_ptr.hpp> -#include <boost/lexical_cast.hpp> - -#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<typename T> -void sharingManager(unsigned numThreads, - SharedChannel<T>* channelsOut[], - SharedChannel<T>* 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 <typename T> -class EmptySharedChannel: public SharedChannel<T> { -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<channelFormat>* d_sharedChannel; - expr::pickle::MapPickler d_pickler; - -public: - int cnt; - PortfolioLemmaOutputChannel(string tag, - SharedChannel<channelFormat> *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<channelFormat>* d_sharedChannel; - expr::pickle::MapPickler d_pickler; - -public: - PortfolioLemmaInputChannel(string tag, - SharedChannel<channelFormat>* 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 ? "<stdin>" : 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<Options> 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<stringstream*> 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<uint64_t> 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<string>(threadOptions[i][options::thread_id]); - string smtTag = "SmtEngine thread #" + boost::lexical_cast<string>(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<channelFormat> *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<channelFormat>(sharingChannelSize); - channelsIn[i] = new EmptySharedChannel<channelFormat>(sharingChannelSize); - continue; - } - channelsOut[i] = new SynchronizedSharedChannel<channelFormat>(sharingChannelSize); - channelsIn[i] = new SynchronizedSharedChannel<channelFormat>(sharingChannelSize); - } - - /* Lemma output channel */ - for(unsigned i = 0; i < numThreads; ++i) { - string tag = "thread #" + boost::lexical_cast<string>(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<Result()> 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<void()> - smFn = boost::bind(sharingManager<channelFormat>, numThreads, channelsOut, channelsIn, smts); - - s_beforePortfolioTime.stop(); - pair<int, Result> 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<PortfolioLemmaOutputChannel*>(opts[options::lemmaOutputChannel])).cnt; - int th1_lemcnt = (*static_cast<PortfolioLemmaOutputChannel*>(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<CommandSequence*>(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<typename T> -void sharingManager(unsigned numThreads, - SharedChannel<T> *channelsOut[], // out and in with respect - SharedChannel<T> *channelsIn[], - SmtEngine *smts[]) // to smt engines -{ - Trace("sharing") << "sharing: thread started " << endl; - vector <int> cnt(numThreads); // Debug("sharing") - - vector< queue<T> > queues; - for(unsigned i = 0; i < numThreads; ++i){ - queues.push_back(queue<T>()); - } - - 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; -} |