summaryrefslogtreecommitdiff
path: root/src/main
diff options
context:
space:
mode:
Diffstat (limited to 'src/main')
-rw-r--r--src/main/main.cpp68
-rw-r--r--src/main/main.h8
-rw-r--r--src/main/util.cpp40
3 files changed, 64 insertions, 52 deletions
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 563fa472e..655562512 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -51,7 +51,8 @@ void doCommand(SmtEngine&, Command*);
void printUsage();
namespace CVC4 {
- namespace main {/* Global options variable */
+ namespace main {
+ /** Global options variable */
Options options;
/** Full argv[0] */
@@ -59,6 +60,9 @@ namespace CVC4 {
/** Just the basename component of argv[0] */
const char *progName;
+
+ /** A pointer to the StatisticsRegistry (the signal handlers need it) */
+ CVC4::StatisticsRegistry* pStatistics;
}
}
@@ -104,8 +108,8 @@ int main(int argc, char* argv[]) {
*options.out << "unknown" << endl;
#endif
*options.err << "CVC4 Error:" << endl << e << endl;
- if(options.statistics) {
- StatisticsRegistry::flushStatistics(*options.err);
+ if(options.statistics && pStatistics != NULL) {
+ pStatistics->flushStatistics(*options.err);
}
exit(1);
} catch(bad_alloc) {
@@ -113,8 +117,8 @@ int main(int argc, char* argv[]) {
*options.out << "unknown" << endl;
#endif
*options.err << "CVC4 ran out of memory." << endl;
- if(options.statistics) {
- StatisticsRegistry::flushStatistics(*options.err);
+ if(options.statistics && pStatistics != NULL) {
+ pStatistics->flushStatistics(*options.err);
}
exit(1);
} catch(...) {
@@ -171,17 +175,41 @@ int runCvc4(int argc, char* argv[]) {
options.interactive = inputFromStdin && isatty(fileno(stdin));
}
+ // Determine which messages to show based on smtcomp_mode and verbosity
+ if(Configuration::isMuzzledBuild()) {
+ Debug.setStream(CVC4::null_os);
+ Trace.setStream(CVC4::null_os);
+ Notice.setStream(CVC4::null_os);
+ Chat.setStream(CVC4::null_os);
+ Message.setStream(CVC4::null_os);
+ Warning.setStream(CVC4::null_os);
+ } else {
+ if(options.verbosity < 2) {
+ Chat.setStream(CVC4::null_os);
+ }
+ if(options.verbosity < 1) {
+ Notice.setStream(CVC4::null_os);
+ }
+ if(options.verbosity < 0) {
+ Message.setStream(CVC4::null_os);
+ Warning.setStream(CVC4::null_os);
+ }
+ }
+
// Create the expression manager
ExprManager exprMgr(options);
// Create the SmtEngine
- SmtEngine smt(&exprMgr, options);
+ SmtEngine smt(&exprMgr);
+
+ // signal handlers need access
+ pStatistics = smt.getStatisticsRegistry();
// Auto-detect input language by filename extension
const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
ReferenceStat< const char* > s_statFilename("filename", filename);
- RegisterStatistic statFilenameReg(&s_statFilename);
+ RegisterStatistic statFilenameReg(exprMgr, &s_statFilename);
if(options.inputLanguage == language::input::LANG_AUTO) {
if( inputFromStdin ) {
@@ -200,26 +228,7 @@ int runCvc4(int argc, char* argv[]) {
}
}
- // Determine which messages to show based on smtcomp_mode and verbosity
- if(Configuration::isMuzzledBuild()) {
- Debug.setStream(CVC4::null_os);
- Trace.setStream(CVC4::null_os);
- Notice.setStream(CVC4::null_os);
- Chat.setStream(CVC4::null_os);
- Message.setStream(CVC4::null_os);
- Warning.setStream(CVC4::null_os);
- } else {
- if(options.verbosity < 2) {
- Chat.setStream(CVC4::null_os);
- }
- if(options.verbosity < 1) {
- Notice.setStream(CVC4::null_os);
- }
- if(options.verbosity < 0) {
- Message.setStream(CVC4::null_os);
- Warning.setStream(CVC4::null_os);
- }
-
+ if(!Configuration::isMuzzledBuild()) {
OutputLanguage language = language::toOutputLanguage(options.inputLanguage);
Debug.getStream() << Expr::setlanguage(language);
Trace.getStream() << Expr::setlanguage(language);
@@ -229,7 +238,6 @@ int runCvc4(int argc, char* argv[]) {
Warning.getStream() << Expr::setlanguage(language);
}
-
// Parse and execute commands until we are done
Command* cmd;
if( options.interactive ) {
@@ -273,10 +281,10 @@ int runCvc4(int argc, char* argv[]) {
#endif
ReferenceStat< Result > s_statSatResult("sat/unsat", result);
- RegisterStatistic statSatResultReg(&s_statSatResult);
+ RegisterStatistic statSatResultReg(exprMgr, &s_statSatResult);
if(options.statistics) {
- StatisticsRegistry::flushStatistics(*options.err);
+ smt.getStatisticsRegistry()->flushStatistics(*options.err);
}
return returnValue;
diff --git a/src/main/main.h b/src/main/main.h
index 2c2773a92..7e0bf6b65 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -21,6 +21,7 @@
#include "util/options.h"
#include "util/exception.h"
+#include "util/stats.h"
#include "cvc4autoconfig.h"
#ifndef __CVC4__MAIN__MAIN_H
@@ -31,10 +32,13 @@ namespace CVC4 {
namespace main {
/** Full argv[0] */
-extern const char *progPath;
+extern const char* progPath;
/** Just the basename component of argv[0] */
-extern const char *progName;
+extern const char* progName;
+
+/** A reference to the StatisticsRegistry for use by the signal handlers */
+extern CVC4::StatisticsRegistry* pStatistics;
/**
* If true, will not spin on segfault even when CVC4_DEBUG is on.
diff --git a/src/main/util.cpp b/src/main/util.cpp
index eb360818b..bf42025a0 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -51,8 +51,8 @@ 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);
+ if(options.statistics && pStatistics != NULL) {
+ pStatistics->flushStatistics(cerr);
}
abort();
}
@@ -60,8 +60,8 @@ void timeout_handler(int sig, siginfo_t* info, void*) {
/** 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);
+ if(options.statistics && pStatistics != NULL) {
+ pStatistics->flushStatistics(cerr);
}
abort();
}
@@ -85,8 +85,8 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
if(segvNoSpin) {
fprintf(stderr, "No-spin requested, aborting...\n");
- if(options.statistics) {
- StatisticsRegistry::flushStatistics(cerr);
+ if(options.statistics && pStatistics != NULL) {
+ pStatistics->flushStatistics(cerr);
}
abort();
} else {
@@ -105,8 +105,8 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
} else if(addr < 10*1024) {
cerr << "Looks like a NULL pointer was dereferenced." << endl;
}
- if(options.statistics) {
- StatisticsRegistry::flushStatistics(cerr);
+ if(options.statistics && pStatistics != NULL) {
+ pStatistics->flushStatistics(cerr);
}
abort();
#endif /* CVC4_DEBUG */
@@ -118,8 +118,8 @@ void ill_handler(int sig, siginfo_t* info, void*) {
fprintf(stderr, "CVC4 executed an illegal instruction in DEBUG mode.\n");
if(segvNoSpin) {
fprintf(stderr, "No-spin requested, aborting...\n");
- if(options.statistics) {
- StatisticsRegistry::flushStatistics(cerr);
+ if(options.statistics && pStatistics != NULL) {
+ pStatistics->flushStatistics(cerr);
}
abort();
} else {
@@ -131,8 +131,8 @@ void ill_handler(int sig, siginfo_t* info, void*) {
}
#else /* CVC4_DEBUG */
fprintf(stderr, "CVC4 executed an illegal instruction.\n");
- if(options.statistics) {
- StatisticsRegistry::flushStatistics(cerr);
+ if(options.statistics && pStatistics != NULL) {
+ pStatistics->flushStatistics(cerr);
}
abort();
#endif /* CVC4_DEBUG */
@@ -155,8 +155,8 @@ void cvc4unexpected() {
}
if(segvNoSpin) {
fprintf(stderr, "No-spin requested.\n");
- if(options.statistics) {
- StatisticsRegistry::flushStatistics(cerr);
+ if(options.statistics && pStatistics != NULL) {
+ pStatistics->flushStatistics(cerr);
}
set_terminate(default_terminator);
} else {
@@ -168,8 +168,8 @@ void cvc4unexpected() {
}
#else /* CVC4_DEBUG */
fprintf(stderr, "CVC4 threw an \"unexpected\" exception.\n");
- if(options.statistics) {
- StatisticsRegistry::flushStatistics(cerr);
+ if(options.statistics && pStatistics != NULL) {
+ pStatistics->flushStatistics(cerr);
}
set_terminate(default_terminator);
#endif /* CVC4_DEBUG */
@@ -181,16 +181,16 @@ void cvc4terminate() {
"CVC4 was terminated by the C++ runtime.\n"
"Perhaps an exception was thrown during stack unwinding. "
"(Don't do that.)\n");
- if(options.statistics) {
- StatisticsRegistry::flushStatistics(cerr);
+ if(options.statistics && pStatistics != NULL) {
+ pStatistics->flushStatistics(cerr);
}
default_terminator();
#else /* CVC4_DEBUG */
fprintf(stderr,
"CVC4 was terminated by the C++ runtime.\n"
"Perhaps an exception was thrown during stack unwinding.\n");
- if(options.statistics) {
- StatisticsRegistry::flushStatistics(cerr);
+ if(options.statistics && pStatistics != NULL) {
+ pStatistics->flushStatistics(cerr);
}
default_terminator();
#endif /* CVC4_DEBUG */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback