diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-07-10 16:20:42 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-07-10 16:20:42 -0400 |
commit | c30a3426c7c2cbaff88b5183b8d8c368a393ac4d (patch) | |
tree | bd621f3766d2ae330a6c11499fe0a49958afa95d /src/main | |
parent | d4f76fdfaed04bf63bb609a5fd26b0d45a9e94f4 (diff) | |
parent | e926fd162c6cee95d31044305e3b4df90b59f9fc (diff) |
Merge remote-tracking branch 'origin/master' into segfaultfix
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/command_executor.cpp | 14 | ||||
-rw-r--r-- | src/main/command_executor.h | 2 | ||||
-rw-r--r-- | src/main/command_executor_portfolio.cpp | 9 | ||||
-rw-r--r-- | src/main/command_executor_portfolio.h | 2 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 7 | ||||
-rw-r--r-- | src/main/interactive_shell.cpp | 10 | ||||
-rw-r--r-- | src/main/interactive_shell.h | 2 | ||||
-rw-r--r-- | src/main/main.cpp | 2 | ||||
-rw-r--r-- | src/main/main.h | 2 | ||||
-rw-r--r-- | src/main/options | 2 | ||||
-rw-r--r-- | src/main/options_handlers.h | 5 | ||||
-rw-r--r-- | src/main/portfolio.cpp | 22 | ||||
-rw-r--r-- | src/main/portfolio.h | 7 | ||||
-rw-r--r-- | src/main/portfolio_util.cpp | 2 | ||||
-rw-r--r-- | src/main/portfolio_util.h | 2 | ||||
-rw-r--r-- | src/main/util.cpp | 7 |
16 files changed, 67 insertions, 30 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 87836b116..5b90ca14f 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -2,10 +2,10 @@ /*! \file command_executor.cpp ** \verbatim ** Original author: Morgan Deters - ** Major contributors: Kshitij Bansal - ** Minor contributors (to current version): Andrew Reynolds + ** Major contributors: Andrew Reynolds, Kshitij Bansal + ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -13,12 +13,14 @@ **/ #include <iostream> +#include <string> #include "main/command_executor.h" #include "expr/command.h" #include "main/main.h" +#include "main/options.h" #include "smt/options.h" #ifndef __WIN32__ @@ -67,7 +69,7 @@ bool CommandExecutor::doCommand(Command* cmd) bool status = true; for(CommandSequence::iterator subcmd = seq->begin(); - status && subcmd != seq->end(); + (status || d_options[options::continuedExecution]) && subcmd != seq->end(); ++subcmd) { status = doCommand(*subcmd); } @@ -151,6 +153,10 @@ bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out) } else { cmd->invoke(smt, *out); } + // ignore the error if the command-verbosity is 0 for this command + if(smt->getOption(std::string("command-verbosity:") + cmd->getCommandName()).getIntegerValue() == 0) { + return true; + } return !cmd->fail(); } diff --git a/src/main/command_executor.h b/src/main/command_executor.h index e6e3d3411..9fe6347be 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -5,7 +5,7 @@ ** Major contributors: Kshitij Bansal ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 1a5d2f8ac..36f2abdd2 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Morgan Deters ** Major contributors: Kshitij Bansal - ** Minor contributors (to current version): none + ** Minor contributors (to current version): Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -304,8 +304,11 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) &d_channelsIn[0], &d_smts[0]); + size_t threadStackSize = d_options[options::threadStackSize]; + threadStackSize *= 1024 * 1024; + pair<int, bool> portfolioReturn = - runPortfolio(d_numThreads, smFn, fns, + runPortfolio(d_numThreads, smFn, fns, threadStackSize, d_options[options::waitToJoin], d_statWaitTime); #ifdef CVC4_STATISTICS_ON diff --git a/src/main/command_executor_portfolio.h b/src/main/command_executor_portfolio.h index 91f9a5169..b3532cea4 100644 --- a/src/main/command_executor_portfolio.h +++ b/src/main/command_executor_portfolio.h @@ -5,7 +5,7 @@ ** Major contributors: Kshitij Bansal ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 2f75c8887..1202c7882 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): Francois Bobot ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -133,6 +133,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { # ifndef PORTFOLIO_BUILD if( opts.wasSetByUser(options::threads) || + opts.wasSetByUser(options::threadStackSize) || ! opts[options::threadArgv].empty() ) { throw OptionException("Thread options cannot be used with sequential CVC4. Please build and use the portfolio binary `pcvc4'."); } @@ -337,7 +338,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { replayParser->useDeclarationsFrom(parser); } bool needReset = false; - while(status && (cmd = parser->nextCommand())) { + while((status || opts[options::continuedExecution]) && (cmd = parser->nextCommand())) { if(dynamic_cast<PushCommand*>(cmd) != NULL) { if(needReset) { pExecutor->reset(); @@ -416,7 +417,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { // have the replay parser use the file's declarations replayParser->useDeclarationsFrom(parser); } - while(status && (cmd = parser->nextCommand())) { + while((status || opts[options::continuedExecution]) && (cmd = parser->nextCommand())) { status = pExecutor->doCommand(cmd); if(dynamic_cast<QuitCommand*>(cmd) != NULL) { delete cmd; diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index a19e23725..bdc956535 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Christopher L. Conway ** Major contributors: Morgan Deters - ** Minor contributors (to current version): Francois Bobot + ** Minor contributors (to current version): Kshitij Bansal, Francois Bobot ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -43,7 +43,9 @@ #if HAVE_LIBREADLINE # include <readline/readline.h> # include <readline/history.h> -# include <ext/stdio_filebuf.h> +# if HAVE_EXT_STDIO_FILEBUF_H +# include <ext/stdio_filebuf.h> +# endif /* HAVE_EXT_STDIO_FILEBUF_H */ #endif /* HAVE_LIBREADLINE */ using namespace std; @@ -57,7 +59,9 @@ const string InteractiveShell::INPUT_FILENAME = "<shell>"; #if HAVE_LIBREADLINE +#if HAVE_EXT_STDIO_FILEBUF_H using __gnu_cxx::stdio_filebuf; +#endif /* HAVE_EXT_STDIO_FILEBUF_H */ char** commandCompletion(const char* text, int start, int end); char* commandGenerator(const char* text, int state); diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index 62d0ceeda..43054f980 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/main/main.cpp b/src/main/main.cpp index a4c4b9c0a..e99095855 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -5,7 +5,7 @@ ** Major contributors: Christopher L. Conway ** Minor contributors (to current version): Clark Barrett, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/main/main.h b/src/main/main.h index 154919aa9..01f337ef4 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/main/options b/src/main/options index fdb172c18..b9262bfa4 100644 --- a/src/main/options +++ b/src/main/options @@ -28,6 +28,8 @@ option threads --threads=N unsigned :default 2 :predicate greater(0) Total number of threads for portfolio option - --threadN=string void :handler CVC4::main::threadN :handler-include "main/options_handlers.h" configures portfolio thread N (0..#threads-1) +option threadStackSize --thread-stack=N unsigned :default 0 + stack size for worker threads in MB (0 means use Boost/thread lib default) option threadArgv std::vector<std::string> :include <vector> <string> Thread configuration (a string to be passed to parseOptions) option thread_id int :default -1 diff --git a/src/main/options_handlers.h b/src/main/options_handlers.h index ee16af2f2..00f192d2f 100644 --- a/src/main/options_handlers.h +++ b/src/main/options_handlers.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Morgan Deters ** Major contributors: none - ** Minor contributors (to current version): Tim King + ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -68,6 +68,7 @@ inline void showConfiguration(std::string option, SmtEngine* smt) { printf("gmp : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no"); printf("glpk : %s\n", Configuration::isBuiltWithGlpk() ? "yes" : "no"); printf("abc : %s\n", Configuration::isBuiltWithAbc() ? "yes" : "no"); + printf("readline : %s\n", Configuration::isBuiltWithReadline() ? "yes" : "no"); printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no"); exit(0); } diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp index 8bfbeff7c..abe27eb06 100644 --- a/src/main/portfolio.cpp +++ b/src/main/portfolio.cpp @@ -5,7 +5,7 @@ ** Major contributors: Kshitij Bansal ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -63,6 +63,7 @@ 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; @@ -74,13 +75,27 @@ std::pair<int, S> runPortfolio(int numThreads, for(int t = 0; t < numThreads; ++t) { +#if BOOST_HAS_THREAD_ATTR boost::thread::attributes attrs; - attrs.set_stack_size(256 * 1024 * 1024); - threads[t] = + 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(Chat.isOn()) { void *stackaddr; size_t stacksize; @@ -126,6 +141,7 @@ std::pair<int, bool> runPortfolio<void, bool>(int, boost::function<void()>, boost::function<bool()>*, + size_t, bool, TimerStat&); diff --git a/src/main/portfolio.h b/src/main/portfolio.h index c2d313a44..f89c8f548 100644 --- a/src/main/portfolio.h +++ b/src/main/portfolio.h @@ -2,10 +2,10 @@ /*! \file portfolio.h ** \verbatim ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Kshitij Bansal + ** Major contributors: Kshitij Bansal + ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -30,6 +30,7 @@ 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 diff --git a/src/main/portfolio_util.cpp b/src/main/portfolio_util.cpp index af8d463cb..7a4beb0d0 100644 --- a/src/main/portfolio_util.cpp +++ b/src/main/portfolio_util.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h index d22ca07d9..8ae730506 100644 --- a/src/main/portfolio_util.h +++ b/src/main/portfolio_util.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/main/util.cpp b/src/main/util.cpp index 14ee82613..5819028da 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Christopher L. Conway, Tim King, ACSYS ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -106,7 +106,8 @@ void segv_handler(int sig, siginfo_t* info, void* c) { abort(); } else { fprintf(stderr, "Spinning so that a debugger can be connected.\n"); - cerr << "Try: gdb " << progName << " " << getpid() << endl; + cerr << "Try: gdb " << progName << " " << getpid() << endl + << " or: gdb --pid=" << getpid() << " " << progName << endl; for(;;) { sleep(60); } @@ -141,6 +142,7 @@ void ill_handler(int sig, siginfo_t* info, void*) { } else { fprintf(stderr, "Spinning so that a debugger can be connected.\n"); fprintf(stderr, "Try: gdb %s %u\n", progName, getpid()); + fprintf(stderr, " or: gdb --pid=%u %s\n", getpid(), progName); for(;;) { sleep(60); } @@ -181,6 +183,7 @@ void cvc4unexpected() { } else { fprintf(stderr, "Spinning so that a debugger can be connected.\n"); fprintf(stderr, "Try: gdb %s %u\n", progName, getpid()); + fprintf(stderr, " or: gdb --pid=%u %s\n", getpid(), progName); for(;;) { sleep(60); } |