Merge remote-tracking branch 'origin/master' into segfaultfix

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);
     }