summaryrefslogtreecommitdiff
path: root/src/main
diff options
context:
space:
mode:
Diffstat (limited to 'src/main')
-rw-r--r--src/main/CMakeLists.txt48
-rw-r--r--src/main/command_executor.cpp10
-rw-r--r--src/main/command_executor.h6
-rw-r--r--src/main/command_executor_portfolio.cpp445
-rw-r--r--src/main/command_executor_portfolio.h85
-rw-r--r--src/main/driver_unified.cpp68
-rw-r--r--src/main/interactive_shell.cpp9
-rw-r--r--src/main/interactive_shell.h6
-rw-r--r--src/main/main.h6
-rw-r--r--src/main/portfolio.cpp149
-rw-r--r--src/main/portfolio.h41
-rw-r--r--src/main/portfolio_util.cpp161
-rw-r--r--src/main/portfolio_util.h180
13 files changed, 26 insertions, 1188 deletions
diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
index 5fb555d70..96e0078ed 100644
--- a/src/main/CMakeLists.txt
+++ b/src/main/CMakeLists.txt
@@ -47,9 +47,12 @@ set_target_properties(cvc4-bin
target_link_libraries(cvc4-bin cvc4 cvc4parser)
if(PROGRAM_PREFIX)
install(PROGRAMS
- $<TARGET_FILE:cvc4-bin> DESTINATION bin RENAME ${PROGRAM_PREFIX}cvc4)
+ $<TARGET_FILE:cvc4-bin>
+ DESTINATION ${RUNTIME_INSTALL_DIR}
+ RENAME ${PROGRAM_PREFIX}cvc4)
else()
- install(TARGETS cvc4-bin DESTINATION bin)
+ install(TARGETS cvc4-bin
+ DESTINATION ${RUNTIME_INSTALL_DIR})
endif()
# In order to get a fully static executable we have to make sure that we also
@@ -62,54 +65,16 @@ 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()
#-----------------------------------------------------------------------------#
# Generate language tokens header files.
-foreach(lang Cvc Smt1 Smt2 Tptp)
+foreach(lang Cvc Smt2 Tptp)
string(TOLOWER ${lang} lang_lc)
add_custom_command(
OUTPUT ${lang_lc}_tokens.h
@@ -125,7 +90,6 @@ endforeach()
add_custom_target(gen-tokens
DEPENDS
cvc_tokens.h
- smt1_tokens.h
smt2_tokens.h
tptp_tokens.h
)
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 7e46b163b..241ca2b8f 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -89,9 +89,10 @@ bool CommandExecutor::doCommand(Command* cmd)
// assume no error
bool status = true;
- for(CommandSequence::iterator subcmd = seq->begin();
- (status || d_options.getContinuedExecution()) && subcmd != seq->end();
- ++subcmd) {
+ for (CommandSequence::iterator subcmd = seq->begin();
+ status && subcmd != seq->end();
+ ++subcmd)
+ {
status = doCommand(*subcmd);
}
@@ -183,7 +184,8 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
}
for (const auto& getterCommand : getterCommands) {
status = doCommandSingleton(getterCommand.get());
- if (!status && !d_options.getContinuedExecution()) {
+ if (!status)
+ {
break;
}
}
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index dde36a453..c71f4d7a5 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -12,8 +12,8 @@
** \brief An additional layer between commands and invoking them.
**/
-#ifndef __CVC4__MAIN__COMMAND_EXECUTOR_H
-#define __CVC4__MAIN__COMMAND_EXECUTOR_H
+#ifndef CVC4__MAIN__COMMAND_EXECUTOR_H
+#define CVC4__MAIN__COMMAND_EXECUTOR_H
#include <iosfwd>
#include <string>
@@ -104,4 +104,4 @@ bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out);
}/* CVC4::main namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__MAIN__COMMAND_EXECUTOR_H */
+#endif /* CVC4__MAIN__COMMAND_EXECUTOR_H */
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 c35fdbcb1..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 7af8a6fdb..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;
@@ -165,10 +149,6 @@ int runCvc4(int argc, char* argv[], Options& opts) {
unsigned len = filenameStr.size();
if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
opts.setInputLanguage(language::input::LANG_SMTLIB_V2_6);
- } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
- opts.setInputLanguage(language::input::LANG_SMTLIB_V1);
- } else if(len >= 5 && !strcmp(".smt1", filename + len - 5)) {
- opts.setInputLanguage(language::input::LANG_SMTLIB_V1);
} else if((len >= 2 && !strcmp(".p", filename + len - 2))
|| (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
opts.setInputLanguage(language::input::LANG_TPTP);
@@ -203,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() != "")
@@ -281,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()
@@ -362,7 +302,8 @@ int runCvc4(int argc, char* argv[], Options& opts) {
int needReset = 0;
// true if one of the commands was interrupted
bool interrupted = false;
- while (status || opts.getContinuedExecution()) {
+ while (status)
+ {
if (interrupted) {
(*opts.getOut()) << CommandInterrupted();
break;
@@ -515,7 +456,8 @@ int runCvc4(int argc, char* argv[], Options& opts) {
replayParser->useDeclarationsFrom(parser.get());
}
bool interrupted = false;
- while(status || opts.getContinuedExecution()) {
+ while (status)
+ {
if (interrupted) {
(*opts.getOut()) << CommandInterrupted();
pExecutor->reset();
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index e7cd8691e..f582d20e5 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -69,10 +69,6 @@ static const std::string cvc_commands[] = {
#include "main/cvc_tokens.h"
};/* cvc_commands */
-static const std::string smt1_commands[] = {
-#include "main/smt1_tokens.h"
-};/* smt1_commands */
-
static const std::string smt2_commands[] = {
#include "main/smt2_tokens.h"
};/* smt2_commands */
@@ -119,11 +115,6 @@ InteractiveShell::InteractiveShell(api::Solver* solver)
commandsBegin = cvc_commands;
commandsEnd = cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands);
break;
- case output::LANG_SMTLIB_V1:
- d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib1";
- commandsBegin = smt1_commands;
- commandsEnd = smt1_commands + sizeof(smt1_commands) / sizeof(*smt1_commands);
- break;
case output::LANG_TPTP:
d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_tptp";
commandsBegin = tptp_commands;
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index b2530dc37..7ed5a1c1f 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -12,8 +12,8 @@
** \brief Interactive shell for CVC4
**/
-#ifndef __CVC4__INTERACTIVE_SHELL_H
-#define __CVC4__INTERACTIVE_SHELL_H
+#ifndef CVC4__INTERACTIVE_SHELL_H
+#define CVC4__INTERACTIVE_SHELL_H
#include <iosfwd>
#include <string>
@@ -72,4 +72,4 @@ public:
}/* CVC4 namespace */
-#endif /* __CVC4__INTERACTIVE_SHELL_H */
+#endif /* CVC4__INTERACTIVE_SHELL_H */
diff --git a/src/main/main.h b/src/main/main.h
index 3199273cb..266d043aa 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -25,8 +25,8 @@
#include "util/statistics.h"
#include "util/statistics_registry.h"
-#ifndef __CVC4__MAIN__MAIN_H
-#define __CVC4__MAIN__MAIN_H
+#ifndef CVC4__MAIN__MAIN_H
+#define CVC4__MAIN__MAIN_H
namespace CVC4 {
namespace main {
@@ -70,4 +70,4 @@ void cvc4_shutdown() noexcept;
int runCvc4(int argc, char* argv[], CVC4::Options&);
void printUsage(CVC4::Options&, bool full = false);
-#endif /* __CVC4__MAIN__MAIN_H */
+#endif /* CVC4__MAIN__MAIN_H */
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 54e38eb3d..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 ab5f26f90..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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback