From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 13 Sep 2010 22:13:36 +0000 (+0000)
Subject: statistics are now printed on timeout (SIGXCPU) and SIGINT if --stats is given
X-Git-Tag: cvc5-1.0.0~8870
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5e619ab6d4622403cc427c17f4282900deb940d5;p=cvc5.git

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 0b962bc9b..235ebb354 100644
--- 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 d56684d7d..350578ffa 100644
--- 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 c685766fa..968563b97 100644
--- 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);