diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-06 20:52:16 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-06 20:52:16 -0500 |
commit | 1c09572e0e2031519a103caa2a4af0d9bd34a9c5 (patch) | |
tree | 576012b4e9434bd4b8472b5df766d3836d3145b9 /src/main | |
parent | 856701f3b2154646eab6b7898fa33e5917322a7b (diff) |
Remove portfolio (#3236)
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/CMakeLists.txt | 38 | ||||
-rw-r--r-- | src/main/command_executor_portfolio.cpp | 445 | ||||
-rw-r--r-- | src/main/command_executor_portfolio.h | 85 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 58 | ||||
-rw-r--r-- | src/main/portfolio.cpp | 149 | ||||
-rw-r--r-- | src/main/portfolio.h | 41 | ||||
-rw-r--r-- | src/main/portfolio_util.cpp | 161 | ||||
-rw-r--r-- | src/main/portfolio_util.h | 180 |
8 files changed, 1 insertions, 1156 deletions
diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt index fad4e77c5..356b0e199 100644 --- a/src/main/CMakeLists.txt +++ b/src/main/CMakeLists.txt @@ -62,48 +62,10 @@ if(ENABLE_STATIC_BINARY) set_target_properties(cvc4-bin PROPERTIES LINK_SEARCH_END_STATIC ON) endif() -if(ENABLE_PORTFOLIO) - set(pcvc4_src_files - command_executor_portfolio.cpp - command_executor_portfolio.h - driver_unified.cpp - main.cpp - portfolio.cpp - portfolio.h - portfolio_util.cpp - portfolio_util.h - ) - - add_executable(pcvc4-bin ${pcvc4_src_files} $<TARGET_OBJECTS:main>) - target_compile_definitions(pcvc4-bin PRIVATE -D__BUILDING_CVC4DRIVER) - target_compile_definitions(pcvc4-bin PRIVATE -DPORTFOLIO_BUILD) - set_target_properties(pcvc4-bin - PROPERTIES - OUTPUT_NAME pcvc4 - RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin) - target_link_libraries(pcvc4-bin cvc4 cvc4parser ${Boost_LIBRARIES}) - target_include_directories(pcvc4-bin PRIVATE ${Boost_INCLUDE_DIRS}) - if(PROGRAM_PREFIX) - install(PROGRAMS - $<TARGET_FILE:pcvc4-bin> DESTINATION bin RENAME ${PROGRAM_PREFIX}pcvc4) - else() - install(TARGETS pcvc4-bin DESTINATION bin) - endif() - - if(ENABLE_STATIC_BINARY) - set_target_properties(pcvc4-bin PROPERTIES LINK_FLAGS -static) - set_target_properties(pcvc4-bin PROPERTIES LINK_SEARCH_START_STATIC ON) - set_target_properties(pcvc4-bin PROPERTIES LINK_SEARCH_END_STATIC ON) - endif() -endif() - if(USE_READLINE) target_link_libraries(cvc4-bin ${Readline_LIBRARIES}) target_link_libraries(main-test ${Readline_LIBRARIES}) target_include_directories(main PRIVATE ${Readline_INCLUDE_DIR}) - if(ENABLE_PORTFOLIO) - target_link_libraries(pcvc4-bin ${Readline_LIBRARIES}) - endif() endif() #-----------------------------------------------------------------------------# diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp deleted file mode 100644 index fde1b59d3..000000000 --- a/src/main/command_executor_portfolio.cpp +++ /dev/null @@ -1,445 +0,0 @@ -/********************* */ -/*! \file command_executor_portfolio.cpp - ** \verbatim - ** Top contributors (to current version): - ** Kshitij Bansal, Tim King, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. 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 executor branches check-sat queries to several - ** threads. - **/ - -#include "main/command_executor_portfolio.h" - -#if HAVE_UNISTD_H -# include <unistd.h> -#endif /* HAVE_UNISTD_H */ - -#include <boost/exception_ptr.hpp> -#include <boost/lexical_cast.hpp> -#include <boost/thread.hpp> -#include <boost/thread/condition.hpp> -#include <string> - -#include "api/cvc4cpp.h" -#include "cvc4autoconfig.h" -#include "expr/pickler.h" -#include "main/main.h" -#include "main/portfolio.h" -#include "options/options.h" -#include "options/set_language.h" -#include "smt/command.h" - -using namespace std; - -namespace CVC4 { -namespace main { - -CommandExecutorPortfolio::CommandExecutorPortfolio(api::Solver* solver, - Options& options, - OptionsList& tOpts) - : CommandExecutor(solver, options), - d_numThreads(options.getThreads()), - d_smts(), - d_seq(new CommandSequence()), - d_threadOptions(tOpts), - d_vmaps(), - d_lastWinner(0), - d_channelsOut(), - d_channelsIn(), - d_ostringstreams(), - d_statLastWinner("portfolio::lastWinner"), - d_statWaitTime("portfolio::waitTime") -{ - assert(d_threadOptions.size() == d_numThreads); - - d_statLastWinner.setData(d_lastWinner); - d_stats.registerStat(&d_statLastWinner); - - d_stats.registerStat(&d_statWaitTime); - - /* Duplication, individualization */ - d_solvers.push_back(d_solver); - d_exprMgrs.push_back(d_solver->getExprManager()); - d_smts.push_back(d_solver->getSmtEngine()); - assert(d_vmaps.size() == 0); - d_vmaps.push_back(new ExprManagerMapCollection()); - for (unsigned i = 1; i < d_numThreads; ++i) - { - api::Solver* solver = new api::Solver(&d_threadOptions[i]); - d_solvers.push_back(solver); - d_exprMgrs.push_back(solver->getExprManager()); - d_smts.push_back(solver->getSmtEngine()); - d_vmaps.push_back(new ExprManagerMapCollection()); - } -} - -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_solvers[i]; - } - d_solvers.clear(); - d_exprMgrs.clear(); - d_smts.clear(); - - d_stats.unregisterStat(&d_statLastWinner); - d_stats.unregisterStat(&d_statWaitTime); -} - -void CommandExecutorPortfolio::lemmaSharingInit() -{ - /* Sharing channels */ - assert(d_channelsIn.size() == 0); - assert(d_channelsOut.size() == 0); - - if(d_numThreads == 1) { - // Disable sharing - d_threadOptions[0].setSharingFilterByLength(0); - } else { - // Setup sharing channels - const unsigned int sharingChannelSize = 1000000; - - for(unsigned i = 0; i < d_numThreads; ++i){ - 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) { - int thread_id = d_threadOptions[i].getThreadId(); - string tag = "thread #" + boost::lexical_cast<string>(thread_id); - LemmaOutputChannel* outputChannel = - new PortfolioLemmaOutputChannel(tag, d_channelsOut[i], d_exprMgrs[i], - d_vmaps[i]->d_from, d_vmaps[i]->d_to); - LemmaInputChannel* inputChannel = - new PortfolioLemmaInputChannel(tag, d_channelsIn[i], d_exprMgrs[i], - d_vmaps[i]->d_from, d_vmaps[i]->d_to); - d_smts[i]->channels()->setLemmaInputChannel(inputChannel); - d_smts[i]->channels()->setLemmaOutputChannel(outputChannel); - } - - /* Output to string stream */ - assert(d_ostringstreams.size() == 0); - for(unsigned i = 0; i < d_numThreads; ++i) { - d_ostringstreams.push_back(new ostringstream); - d_threadOptions[i].setOut(d_ostringstreams[i]); - - OutputLanguage outputLanguage = d_threadOptions[i].getOutputLanguage(); - // important even for muzzled builds (to get result output right) - *(d_threadOptions[i].getOut()) << language::SetLanguage(outputLanguage); - } - } -}/* CommandExecutorPortfolio::lemmaSharingInit() */ - -void CommandExecutorPortfolio::lemmaSharingCleanup() -{ - assert(d_numThreads == d_options.getThreads()); - - if(d_numThreads == 1) - return; - - // 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]; - delete d_smts[i]->channels()->getLemmaInputChannel(); - d_smts[i]->channels()->setLemmaInputChannel(NULL); - delete d_smts[i]->channels()->getLemmaOutputChannel(); - d_smts[i]->channels()->setLemmaOutputChannel(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].setOut(d_options.getOut()); - delete d_ostringstreams[i]; - } - d_ostringstreams.clear(); - } - -}/* CommandExecutorPortfolio::lemmaSharingCleanup() */ - - -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 command on lastWinner, saving the command - // to be run on all others - // - // mode = 1 : run a race of the command, update lastWinner - // - // mode = 2 : run _only_ the lastWinner thread, not saving the - // command - - if( dynamic_cast<CheckSynthCommand*>(cmd) != NULL ){ - // sygus not supported in portfolio : FIXME: can support once datatypes exportTo is supported - return CommandExecutor::doCommandSingleton(cmd); - } - - if(dynamic_cast<CheckSatCommand*>(cmd) != NULL || - dynamic_cast<QueryCommand*>(cmd) != NULL ) { - mode = 1; - } else if(dynamic_cast<GetValueCommand*>(cmd) != NULL || - dynamic_cast<GetAssignmentCommand*>(cmd) != NULL || - dynamic_cast<GetModelCommand*>(cmd) != NULL || - dynamic_cast<GetProofCommand*>(cmd) != NULL || - dynamic_cast<GetInstantiationsCommand*>(cmd) != NULL || - dynamic_cast<GetUnsatCoreCommand*>(cmd) != NULL || - dynamic_cast<GetAssertionsCommand*>(cmd) != NULL || - dynamic_cast<GetInfoCommand*>(cmd) != NULL || - dynamic_cast<GetOptionCommand*>(cmd) != NULL || - false) { - mode = 2; - } - - Debug("portfolio::outputmode") << "Mode is " << mode - << "lastWinner is " << d_lastWinner - << "d_seq is " << d_seq << std::endl; - - if(mode == 0) { - d_seq->addCommand(cmd->clone()); - Command* cmdExported = - d_lastWinner == 0 ? - cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) ); - std::ostream* winnersOut = d_options.getVerbosity() >= -1 ? - (d_threadOptions[d_lastWinner]).getOut() : NULL; - bool ret = smtEngineInvoke(d_smts[d_lastWinner], cmdExported, winnersOut); - if(d_lastWinner != 0) delete cmdExported; - return ret; - } 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 achieved without a lot of work. - Command *seqs[d_numThreads]; - - if(d_lastWinner == 0) - seqs[0] = cmd; - else - seqs[0] = d_seq; - - /* 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] = - int(i) == d_lastWinner ? - cmd->exportTo(d_exprMgrs[i], *(d_vmaps[i])) : - d_seq->exportTo(d_exprMgrs[i], *(d_vmaps[i]) ); - } catch(ExportUnsupportedException& e) { - if(d_options.getFallbackSequential()) { - Notice() << "Unsupported theory encountered." - << "Switching to sequential mode."; - return CommandExecutor::doCommandSingleton(cmd); - } - else - throw Exception("Certain theories (e.g., datatypes) are (currently)" - " unsupported in portfolio\n mode. Please see option" - " --fallback-sequential to make this a soft error."); - } - } - - /** - * 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) { - VarMap& thread_0_from = d_vmaps[0]->d_from; - VarMap& thread_1_to = d_vmaps[1]->d_to; - for(VarMap::iterator i=thread_1_to.begin(); - i != thread_1_to.end(); ++i) { - thread_0_from[i->first] = i->first; - } - d_vmaps[0]->d_to = thread_0_from; - } - - lemmaSharingInit(); - - /* Portfolio */ - boost::function<bool()>* fns = new boost::function<bool()>[d_numThreads]; - for(unsigned i = 0; i < d_numThreads; ++i) { - std::ostream* current_out_or_null = d_options.getVerbosity() >= -1 ? - d_threadOptions[i].getOut() : NULL; - - fns[i] = boost::bind(smtEngineInvoke, d_smts[i], seqs[i], - current_out_or_null); - } - - assert(d_channelsIn.size() == d_numThreads - || d_numThreads == 1); - assert(d_channelsOut.size() == d_numThreads - || d_numThreads == 1); - assert(d_smts.size() == d_numThreads); - assert( !d_statWaitTime.running() ); - - boost::function<void()> - smFn = d_numThreads <= 1 ? boost::function<void()>() : - boost::bind(sharingManager<ChannelFormat>, - d_numThreads, - &d_channelsOut[0], - &d_channelsIn[0], - &d_smts[0]); - - size_t threadStackSize = d_options.getThreadStackSize(); - threadStackSize *= 1024 * 1024; - - pair<int, bool> portfolioReturn = - runPortfolio(d_numThreads, smFn, fns, threadStackSize, - d_options.getWaitToJoin(), d_statWaitTime); - -#ifdef CVC4_STATISTICS_ON - assert( d_statWaitTime.running() ); - d_statWaitTime.stop(); -#endif /* CVC4_STATISTICS_ON */ - - d_lastWinner = portfolioReturn.first; - d_result = d_smts[d_lastWinner]->getStatusOfLastCommand(); - - if(d_ostringstreams.size() != 0) { - assert(d_numThreads == d_options.getThreads()); - assert(portfolioReturn.first >= 0); - assert(unsigned(portfolioReturn.first) < d_numThreads); - - std::ostream& out = *d_options.getOut(); - if(Debug.isOn("treat-unknown-error")) { - if(d_ostringstreams[portfolioReturn.first]->str() == "unknown\n") { - out << "portfolioReturn = (" << portfolioReturn.first << ", " - << portfolioReturn.second << ")\n"; - for(unsigned i = 0; i < d_numThreads; ++i) - out << "thread " << i << ": " << d_ostringstreams[i]->str() - << std::endl; - throw Exception("unknown encountered"); - } - } - - out << d_ostringstreams[portfolioReturn.first]->str() - << std::flush; - -#ifdef CVC4_COMPETITION_MODE - // We use CVC4 in competition with --no-wait-to-join. If - // destructors run, they will destroy(!) us. So, just exit now. - _exit(0); -#endif /* CVC4_COMPETITION_MODE */ - } - - /* cleanup this check sat specific stuff */ - lemmaSharingCleanup(); - - delete d_seq; - d_seq = new CommandSequence(); - - delete[] fns; - - bool status = portfolioReturn.second; - - // dump the model/proof/unsat core if option is set - if(status) { - if( d_options.getProduceModels() && - d_options.getDumpModels() && - ( d_result.asSatisfiabilityResult() == Result::SAT || - (d_result.isUnknown() && - d_result.whyUnknown() == Result::INCOMPLETE) ) ) - { - Command* gm = new GetModelCommand(); - status = doCommandSingleton(gm); - } else if( d_options.getProof() && - d_options.getDumpProofs() && - d_result.asSatisfiabilityResult() == Result::UNSAT ) { - Command* gp = new GetProofCommand(); - status = doCommandSingleton(gp); - } else if( d_options.getDumpInstantiations() && - ( ( d_options.getInstFormatMode() != INST_FORMAT_MODE_SZS && - ( d_result.asSatisfiabilityResult() == Result::SAT || - (d_result.isUnknown() && - d_result.whyUnknown() == Result::INCOMPLETE) ) ) || - d_result.asSatisfiabilityResult() == Result::UNSAT ) ) { - Command* gi = new GetInstantiationsCommand(); - status = doCommandSingleton(gi); - } else if( d_options.getDumpSynth() && - d_result.asSatisfiabilityResult() == Result::UNSAT ){ - Command* gi = new GetSynthSolutionCommand(); - status = doCommandSingleton(gi); - } else if( d_options.getDumpUnsatCores() && - d_result.asSatisfiabilityResult() == Result::UNSAT ) { - Command* guc = new GetUnsatCoreCommand(); - status = doCommandSingleton(guc); - } - } - - return status; - } else if(mode == 2) { - Command* cmdExported = d_lastWinner == 0 ? - cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner])); - std::ostream* winner_out_if_verbose = d_options.getVerbosity() >= -1 ? - d_threadOptions[d_lastWinner].getOut() : NULL; - bool ret = smtEngineInvoke(d_smts[d_lastWinner], cmdExported, - winner_out_if_verbose); - if(d_lastWinner != 0){ - delete cmdExported; - } - return ret; - } else { - // Unreachable(); - assert(false); - return false; - } - -}/* CommandExecutorPortfolio::doCommandSingleton() */ - -void CommandExecutorPortfolio::flushStatistics(std::ostream& out) const { - assert(d_numThreads == d_exprMgrs.size() && - d_exprMgrs.size() == d_smts.size()); - for(size_t i = 0; i < d_numThreads; ++i) { - string emTag = "thread#" - + boost::lexical_cast<string>(d_threadOptions[i].getThreadId()); - Statistics stats = d_exprMgrs[i]->getStatistics(); - stats.setPrefix(emTag); - stats.flushInformation(out); - - string smtTag = "thread#" - + boost::lexical_cast<string>(d_threadOptions[i].getThreadId()); - stats = d_smts[i]->getStatistics(); - stats.setPrefix(smtTag); - stats.flushInformation(out); - } - d_stats.flushInformation(out); -} - -}/* CVC4::main namespace */ -}/* CVC4 namespace */ diff --git a/src/main/command_executor_portfolio.h b/src/main/command_executor_portfolio.h deleted file mode 100644 index ef3329ef5..000000000 --- a/src/main/command_executor_portfolio.h +++ /dev/null @@ -1,85 +0,0 @@ -/********************* */ -/*! \file command_executor_portfolio.h - ** \verbatim - ** Top contributors (to current version): - ** Kshitij Bansal, Morgan Deters, Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. 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" - -#include <iosfwd> -#include <sstream> -#include <string> -#include <vector> - -namespace CVC4 { - -class CommandSequence; - -namespace api { -class Solver; -} - -namespace main { - -class CommandExecutorPortfolio : public CommandExecutor { - // Solvers are created/deleted during initialization - std::vector<api::Solver*> d_solvers; - - 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; - OptionsList& 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; - - // Stats - ReferenceStat<int> d_statLastWinner; - TimerStat d_statWaitTime; - -public: - CommandExecutorPortfolio(api::Solver* solver, - Options& options, - OptionsList& tOpts); - - ~CommandExecutorPortfolio(); - - std::string getSmtEngineStatus(); - - void flushStatistics(std::ostream& out) const override; - -protected: - bool doCommandSingleton(Command* cmd) override; - -private: - CommandExecutorPortfolio(); - void lemmaSharingInit(); - void lemmaSharingCleanup(); -};/* class CommandExecutorPortfolio */ - -}/* CVC4::main namespace */ -}/* CVC4 namespace */ - -#endif /* CVC4__MAIN__COMMAND_EXECUTOR_PORTFOLIO_H */ diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index de840cb07..c4800a3ac 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -9,8 +9,7 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Driver for CVC4 executable (cvc4) unified for both - ** sequential and portfolio versions + ** \brief Driver for CVC4 executable (cvc4) **/ #include <stdio.h> @@ -42,13 +41,6 @@ #include "util/result.h" #include "util/statistics_registry.h" -// The PORTFOLIO_BUILD is defined when compiling pcvc4 (the parallel version of -// CVC4) and undefined otherwise. The macro can only be used in -// driver_unified.cpp because we do not recompile all files for pcvc4. -#ifdef PORTFOLIO_BUILD -# include "main/command_executor_portfolio.h" -#endif - using namespace std; using namespace CVC4; using namespace CVC4::parser; @@ -106,14 +98,6 @@ int runCvc4(int argc, char* argv[], Options& opts) { // Parse the options vector<string> filenames = Options::parseOptions(&opts, argc, argv); -# ifndef PORTFOLIO_BUILD - if( opts.wasSetByUserThreads() || - opts.wasSetByUserThreadStackSize() || - (! opts.getThreadArgv().empty()) ) { - throw OptionException("Thread options cannot be used with sequential CVC4. Please build and use the portfolio binary `pcvc4'."); - } -# endif - string progNameStr = opts.getBinaryName(); progName = &progNameStr; @@ -199,46 +183,8 @@ int runCvc4(int argc, char* argv[], Options& opts) { // Create the expression manager using appropriate options std::unique_ptr<api::Solver> solver; -# ifndef PORTFOLIO_BUILD solver.reset(new api::Solver(&opts)); pExecutor = new CommandExecutor(solver.get(), opts); -# else - OptionsList threadOpts; - parseThreadSpecificOptions(threadOpts, opts); - - bool useParallelExecutor = true; - // incremental? - if(opts.wasSetByUserIncrementalSolving() && - opts.getIncrementalSolving() && - (! opts.getIncrementalParallel()) ) { - Notice() << "Notice: In --incremental mode, using the sequential solver" - << " unless forced by...\n" - << "Notice: ...the experimental --incremental-parallel option.\n"; - useParallelExecutor = false; - } - // proofs? - if(opts.getCheckProofs()) { - if(opts.getFallbackSequential()) { - Warning() << "Warning: Falling back to sequential mode, as cannot run" - << " portfolio in check-proofs mode.\n"; - useParallelExecutor = false; - } - else { - throw OptionException("Cannot run portfolio in check-proofs mode."); - } - } - // pick appropriate one - if (useParallelExecutor) - { - solver.reset(new api::Solver(&threadOpts[0])); - pExecutor = new CommandExecutorPortfolio(solver.get(), opts, threadOpts); - } - else - { - solver.reset(new api::Solver(&opts)); - pExecutor = new CommandExecutor(solver.get(), opts); - } -# endif std::unique_ptr<Parser> replayParser; if (opts.getReplayInputFilename() != "") @@ -277,14 +223,12 @@ int runCvc4(int argc, char* argv[], Options& opts) { throw OptionException( "--tear-down-incremental doesn't work in interactive mode"); } -#ifndef PORTFOLIO_BUILD if(!opts.wasSetByUserIncrementalSolving()) { cmd = new SetOptionCommand("incremental", SExpr(true)); cmd->setMuted(true); pExecutor->doCommand(cmd); delete cmd; } -#endif /* PORTFOLIO_BUILD */ InteractiveShell shell(solver.get()); if(opts.getInteractivePrompt()) { Message() << Configuration::getPackageName() diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp deleted file mode 100644 index 89a6d8253..000000000 --- a/src/main/portfolio.cpp +++ /dev/null @@ -1,149 +0,0 @@ -/********************* */ -/*! \file portfolio.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Kshitij Bansal - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Provides (somewhat) generic functionality to simulate a - ** (potentially cooperative) race - **/ - -#include <boost/function.hpp> -#include <boost/thread.hpp> -#include <boost/bind.hpp> -#include <boost/thread/condition.hpp> -#include <boost/exception_ptr.hpp> - -#include "base/output.h" -#include "options/options.h" -#include "smt/smt_engine.h" -#include "util/result.h" -#include "util/statistics_registry.h" - -namespace CVC4 { - -/** Mutex to make sure at most one thread is winner */ -boost::mutex mutex_done; - -/** Mutex / condition variable to notify main when winner data written */ -boost::mutex mutex_main_wait; -boost::condition_variable condition_var_main_wait; - -bool global_flag_done; -int global_winner; - -template<typename S> -void runThread(int thread_id, boost::function<S()> threadFn, S& returnValue) -{ - /* Uncomment line to delay first thread, useful to unearth errors/debug */ - // if(thread_id == 0) { sleep(1); } - returnValue = threadFn(); - - if( mutex_done.try_lock() ) { - if(global_flag_done == false) - { - { - boost::lock_guard<boost::mutex> lock(mutex_main_wait); - global_winner = thread_id; - global_flag_done = true; - } - condition_var_main_wait.notify_all(); // we want main thread to quit - } - mutex_done.unlock(); - } -} - -template<typename T, typename S> -std::pair<int, S> runPortfolio(int numThreads, - boost::function<T()> driverFn, - boost::function<S()> threadFns[], - size_t stackSize, - bool optionWaitToJoin, - TimerStat& statWaitTime) { - boost::thread thread_driver; - boost::thread* threads = new boost::thread[numThreads]; - S* threads_returnValue = new S[numThreads]; - - global_flag_done = false; - global_winner = -1; - - for(int t = 0; t < numThreads; ++t) { - -#if BOOST_HAS_THREAD_ATTR - boost::thread::attributes attrs; - - if(stackSize > 0) { - attrs.set_stack_size(stackSize); - } - - threads[t] = - boost::thread(attrs, boost::bind(runThread<S>, t, threadFns[t], - boost::ref(threads_returnValue[t]) ) ); -#else /* BOOST_HAS_THREAD_ATTR */ - if(stackSize > 0) { - throw OptionException("cannot specify a stack size for worker threads; requires CVC4 to be built with Boost thread library >= 1.50.0"); - } - - threads[t] = - boost::thread(boost::bind(runThread<S>, t, threadFns[t], - boost::ref(threads_returnValue[t]) ) ); - -#endif /* BOOST_HAS_THREAD_ATTR */ - -#if defined(BOOST_THREAD_PLATFORM_PTHREAD) - if(Chat.isOn()) { - void *stackaddr; - size_t stacksize; - pthread_attr_t attr; - pthread_getattr_np(threads[t].native_handle(), &attr); - pthread_attr_getstack(&attr, &stackaddr, &stacksize); - Chat() << "Created worker thread " << t << " with stack size " << stacksize << std::endl; - } -#endif - } - - if(not driverFn.empty()) - thread_driver = boost::thread(driverFn); - - boost::unique_lock<boost::mutex> lock(mutex_main_wait); - while(global_flag_done == false) { - condition_var_main_wait.wait(lock); - } - - statWaitTime.start(); - - if(not driverFn.empty()) { - thread_driver.interrupt(); - thread_driver.join(); - } - - for(int t = 0; t < numThreads; ++t) { - if(optionWaitToJoin) { - threads[t].join(); - } - } - - std::pair<int, S> retval(global_winner, threads_returnValue[global_winner]); - - delete[] threads; - delete[] threads_returnValue; - - return retval; -} - -// instantiation -template -std::pair<int, bool> -runPortfolio<void, bool>(int, - boost::function<void()>, - boost::function<bool()>*, - size_t, - bool, - TimerStat&); - -}/* CVC4 namespace */ diff --git a/src/main/portfolio.h b/src/main/portfolio.h deleted file mode 100644 index 2cb23d5c5..000000000 --- a/src/main/portfolio.h +++ /dev/null @@ -1,41 +0,0 @@ -/********************* */ -/*! \file portfolio.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Kshitij Bansal - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Provides (somewhat) generic functionality to simulate a - ** (potentially cooperative) race - **/ - -#ifndef CVC4__PORTFOLIO_H -#define CVC4__PORTFOLIO_H - -#include <boost/function.hpp> -#include <utility> - -#include "options/options.h" -#include "smt/command.h" -#include "smt/smt_engine.h" -#include "util/statistics_registry.h" - -namespace CVC4 { - -template<typename T, typename S> -std::pair<int, S> runPortfolio(int numThreads, - boost::function<T()> driverFn, - boost::function<S()> threadFns[], - size_t stackSize, - bool optionWaitToJoin, - TimerStat& statWaitTime); -// as we have defined things, S=void would give compile errors -// do we want to fix this? yes, no, maybe? - -}/* CVC4 namespace */ - -#endif /* CVC4__PORTFOLIO_H */ diff --git a/src/main/portfolio_util.cpp b/src/main/portfolio_util.cpp deleted file mode 100644 index a3b6767c7..000000000 --- a/src/main/portfolio_util.cpp +++ /dev/null @@ -1,161 +0,0 @@ -/********************* */ -/*! \file portfolio_util.cpp - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Morgan Deters, Kshitij Bansal - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Code relevant only for portfolio builds - **/ - -#include "main/portfolio_util.h" - -#include <unistd.h> - -#include <cassert> -#include <vector> - -#include "options/options.h" - -using namespace std; - -namespace CVC4 { - -OptionsList::OptionsList() : d_options() {} - -OptionsList::~OptionsList(){ - for(std::vector<Options*>::iterator i = d_options.begin(), - iend = d_options.end(); i != iend; ++i) - { - Options* current = *i; - delete current; - } - d_options.clear(); -} - -void OptionsList::push_back_copy(const Options& opts) { - Options* copy = new Options; - copy->copyValues(opts); - d_options.push_back(copy); -} - -Options& OptionsList::operator[](size_t position){ - return *(d_options[position]); -} - -const Options& OptionsList::operator[](size_t position) const { - return *(d_options[position]); -} - -Options& OptionsList::back() { - return *(d_options.back()); -} - -size_t OptionsList::size() const { - return d_options.size(); -} - -void parseThreadSpecificOptions(OptionsList& threadOptions, const Options& opts) -{ - - unsigned numThreads = opts.getThreads(); - - for(unsigned i = 0; i < numThreads; ++i) { - threadOptions.push_back_copy(opts); - Options& tOpts = threadOptions.back(); - - // Set thread identifier - tOpts.setThreadId(i); - const std::vector<std::string>& optThreadArgvs = opts.getThreadArgv(); - if(i < optThreadArgvs.size() && (! optThreadArgvs[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(optThreadArgvs[i].c_str()); - char* p = tbuf; - // string length is certainly an upper bound on size needed - char** targv = new char*[optThreadArgvs[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 { - Options::parseOptions(&tOpts, targc, targv); - } catch(OptionException& e) { - stringstream ss; - ss << optid << ": " << e.getMessage(); - throw OptionException(ss.str()); - } - if(tOpts.getThreads() != numThreads || - tOpts.getThreadArgv() != opts.getThreadArgv()) { - 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? -} - -void PortfolioLemmaOutputChannel::notifyNewLemma(Expr lemma) { - if(int(lemma.getNumChildren()) > Options::currentGetSharingFilterByLength()) { - 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::currentGetThreadId() == 0) { - (*(Options::currentGetOut())) - << "thread #0: notifyNewLemma: " << lemma << std::endl; - } - } catch(expr::pickle::PicklingException& p){ - Trace("sharing::blocked") << lemma << std::endl; - } -} - - -PortfolioLemmaInputChannel::PortfolioLemmaInputChannel(std::string tag, - SharedChannel<ChannelFormat>* c, - ExprManager* em, - VarMap& to, - VarMap& from) - : d_tag(tag), d_sharedChannel(c), d_pickler(em, to, from) -{} - -bool PortfolioLemmaInputChannel::hasNewLemma(){ - Debug("lemmaInputChannel") << d_tag << ": " << "hasNewLemma" << std::endl; - return !d_sharedChannel->empty(); -} - -Expr PortfolioLemmaInputChannel::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::currentGetThreadId() == 0) { - (*Options::currentGetOut()) << "thread #0: getNewLemma: " << e << std::endl; - } - return e; -} - -}/*CVC4 namespace */ diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h deleted file mode 100644 index e5ca296ae..000000000 --- a/src/main/portfolio_util.h +++ /dev/null @@ -1,180 +0,0 @@ -/********************* */ -/*! \file portfolio_util.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Kshitij Bansal, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. 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 <queue> - -#include "base/output.h" -#include "expr/pickler.h" -#include "smt/smt_engine.h" -#include "smt_util/lemma_input_channel.h" -#include "smt_util/lemma_output_channel.h" -#include "util/channel.h" - -namespace CVC4 { - -typedef expr::pickle::Pickle ChannelFormat; - -class PortfolioLemmaOutputChannel : public LemmaOutputChannel { -private: - std::string d_tag; - SharedChannel<ChannelFormat>* d_sharedChannel; - expr::pickle::MapPickler d_pickler; - -public: - int cnt; - PortfolioLemmaOutputChannel(std::string tag, - SharedChannel<ChannelFormat> *c, - ExprManager* em, - VarMap& to, - VarMap& from) : - d_tag(tag), - d_sharedChannel(c), - d_pickler(em, to, from), - cnt(0) - {} - - ~PortfolioLemmaOutputChannel() {} - - void notifyNewLemma(Expr lemma) override; -};/* class PortfolioLemmaOutputChannel */ - -class PortfolioLemmaInputChannel : public LemmaInputChannel { -private: - std::string d_tag; - SharedChannel<ChannelFormat>* d_sharedChannel; - expr::pickle::MapPickler d_pickler; - -public: - PortfolioLemmaInputChannel(std::string tag, - SharedChannel<ChannelFormat>* c, - ExprManager* em, - VarMap& to, - VarMap& from); - - ~PortfolioLemmaInputChannel() {} - - bool hasNewLemma() override; - Expr getNewLemma() override; - -};/* class PortfolioLemmaInputChannel */ - -class OptionsList { - public: - OptionsList(); - ~OptionsList(); - - void push_back_copy(const Options& options); - - Options& operator[](size_t position); - const Options& operator[](size_t position) const; - - Options& back(); - - size_t size() const; - private: - OptionsList(const OptionsList&) = delete; - OptionsList& operator=(const OptionsList&) = delete; - std::vector<Options*> d_options; -}; - -void parseThreadSpecificOptions(OptionsList& list, const Options& opts); - -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 " << std::endl; - std::vector <int> cnt(numThreads); // Debug("sharing") - - std::vector< std::queue<T> > queues; - for(unsigned i = 0; i < numThreads; ++i){ - queues.push_back(std::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) { - - /* 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; -}/* sharingManager() */ - -}/* CVC4 namespace */ - -#endif /* CVC4__PORTFOLIO_UTIL_H */ |