statistics are now printed on timeout (SIGXCPU) and SIGINT if --stats is given

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 0b962bc9be590b7039c2b2beb08f898d6e02fd03..235ebb35485dbca42c554f95065101d0342f8eab 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -43,7 +43,12 @@ using namespace CVC4::parser;
 using namespace CVC4::main;
 
 static Result lastResult;
-static struct Options options;
+
+namespace CVC4 {
+  namespace main {
+    struct Options options;
+  }/* CVC4::main namespace */
+}/* CVC4 namespace */
 
 int runCvc4(int argc, char* argv[]);
 void doCommand(SmtEngine&, Command*);

diff --git a/src/main/main.h b/src/main/main.h
index d56684d7d01e45cc623ab8084ef1653aeb370977..350578ffa15909524e16fe89502f1b43dddae724 100644 (file)
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -52,6 +52,12 @@ extern const char *progName;
  */
 extern bool segvNoSpin;
 
+/**
+ * Keep a copy of the options around globally, so that signal handlers can
+ * access it.
+ */
+extern struct Options options;
+
 /** Parse argc/argv and put the result into a CVC4::Options struct. */
 int parseOptions(int argc, char** argv, CVC4::Options*) throw(OptionException);
 

diff --git a/src/main/util.cpp b/src/main/util.cpp
index c685766fa88f60a7daee476601a1f5631fff6017..968563b977a376388a6b8b1c58dbe55596e80052 100644 (file)
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -24,7 +24,9 @@
 #include <signal.h>
 
 #include "util/exception.h"
+#include "util/options.h"
 #include "util/Assert.h"
+#include "util/stats.h"
 
 #include "cvc4autoconfig.h"
 #include "main.h"
@@ -42,9 +44,21 @@ namespace main {
  */
 bool segvNoSpin = false;
 
+/** Handler for SIGXCPU, i.e., timeout. */
+void timeout_handler(int sig, siginfo_t* info, void*) {
+  fprintf(stderr, "CVC4 interrupted by timeout.\n");
+  if(options.statistics) {
+    StatisticsRegistry::flushStatistics(cerr);
+  }
+  abort();
+}
+
 /** Handler for SIGINT, i.e., when the user hits control C. */
 void sigint_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 interrupted by user.\n");
+  if(options.statistics) {
+    StatisticsRegistry::flushStatistics(cerr);
+  }
   abort();
 }
 
@@ -123,10 +137,17 @@ void cvc4_init() throw() {
     throw Exception(string("sigaction(SIGINT) failure: ") + strerror(errno));
 
   struct sigaction act2;
-  act2.sa_sigaction = segv_handler;
+  act2.sa_sigaction = timeout_handler;
   act2.sa_flags = SA_SIGINFO;
   sigemptyset(&act2.sa_mask);
-  if(sigaction(SIGSEGV, &act2, NULL))
+  if(sigaction(SIGXCPU, &act2, NULL))
+    throw Exception(string("sigaction(SIGXCPU) failure: ") + strerror(errno));
+
+  struct sigaction act3;
+  act3.sa_sigaction = segv_handler;
+  act3.sa_flags = SA_SIGINFO;
+  sigemptyset(&act3.sa_mask);
+  if(sigaction(SIGSEGV, &act3, NULL))
     throw Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno));
 
   set_unexpected(cvc4unexpected);