From 65d24277bfb9f76b612fa51770d5d63e1d34b528 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Tue, 4 May 2010 21:57:57 +0000 Subject: [PATCH] Disabling semantic checks in competition mode. Adding function debugTagIsOn to safely test for tracing in any compilation mode. Removing irrelevant command-line options from usage message in muzzled mode. --- configure.ac | 2 +- src/context/context.cpp | 6 +++--- src/main/getopt.cpp | 22 +++++++--------------- src/main/main.cpp | 37 +++++++++++++++++++------------------ src/main/usage.h | 21 +++++++++++++-------- src/util/options.h | 2 -- src/util/output.h | 8 ++++++++ 7 files changed, 51 insertions(+), 47 deletions(-) diff --git a/configure.ac b/configure.ac index 93f8f2ee5..e80c80e24 100644 --- a/configure.ac +++ b/configure.ac @@ -229,7 +229,7 @@ case "$with_build" in if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi ;; competition) # maximally optimized, no assertions, no tracing, muzzled - CVC4CPPFLAGS= + CVC4CPPFLAGS='-DCVC4_COMPETITION_MODE' CVC4CXXFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs' CVC4CFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs' CVC4LDFLAGS= diff --git a/src/context/context.cpp b/src/context/context.cpp index 2be116baa..2de6e2051 100644 --- a/src/context/context.cpp +++ b/src/context/context.cpp @@ -227,7 +227,7 @@ ContextObj* ContextObj::restoreAndContinue() throw(AssertionException) { void ContextObj::destroy() throw(AssertionException) { - if( DebugOut.isOn("context") ) { + if( debugTagIsOn("context") ) { /* Context can be big and complicated, so we only want to process this output * if we're really going to use it. (Same goes below.) */ @@ -246,7 +246,7 @@ void ContextObj::destroy() throw(AssertionException) { if(d_pContextObjRestore == NULL) { break; } - if( DebugOut.isOn("context") ) { + if( debugTagIsOn("context") ) { Debug("context") << "in destroy " << this << ", restore object is " << d_pContextObjRestore << " at level " << d_pContextObjRestore->getLevel() << ":" << std::endl @@ -254,7 +254,7 @@ void ContextObj::destroy() throw(AssertionException) { } restoreAndContinue(); } - if( DebugOut.isOn("context") ) { + if( debugTagIsOn("context") ) { Debug("context") << "after destroy " << this << ":" << std::endl << *getContext() << std::endl; } diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index a09da850d..b24e91803 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -91,21 +91,20 @@ enum OptionValue { */ static struct option cmdlineOptions[] = { // name, has_arg, *flag, val - { "help" , no_argument , NULL, 'h' }, - { "version" , no_argument , NULL, 'V' }, - { "about" , no_argument , NULL, 'V' }, { "verbose" , no_argument , NULL, 'v' }, { "quiet" , no_argument , NULL, 'q' }, - { "lang" , required_argument, NULL, 'L' }, { "debug" , required_argument, NULL, 'd' }, { "trace" , required_argument, NULL, 't' }, - { "smtcomp" , no_argument , NULL, SMTCOMP }, { "stats" , no_argument , NULL, STATS }, + { "no-checking", no_argument , NULL, NO_CHECKING }, + { "show-config", no_argument , NULL, SHOW_CONFIG }, { "segv-nospin", no_argument , NULL, SEGV_NOSPIN }, + { "help" , no_argument , NULL, 'h' }, + { "version" , no_argument , NULL, 'V' }, + { "about" , no_argument , NULL, 'V' }, + { "lang" , required_argument, NULL, 'L' }, { "parse-only" , no_argument , NULL, PARSE_ONLY }, - { "no-checking", no_argument , NULL, NO_CHECKING }, - { "mmap", no_argument , NULL, USE_MMAP }, - { "show-config", no_argument , NULL, SHOW_CONFIG } + { "mmap", no_argument , NULL, USE_MMAP } };/* if you add things to the above, please remember to update usage.h! */ /** Full argv[0] */ @@ -199,13 +198,6 @@ throw(OptionException) { segvNoSpin = true; break; - case SMTCOMP: - // silences CVC4 (except "sat" or "unsat" or "unknown", forces smtlib input) - opts->smtcomp_mode = true; - opts->verbosity = -1; - opts->lang = parser::LANG_SMTLIB; - break; - case PARSE_ONLY: opts->parseOnly = true; break; diff --git a/src/main/main.cpp b/src/main/main.cpp index a575426fd..037dde559 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -27,10 +27,11 @@ #include "expr/expr_manager.h" #include "smt/smt_engine.h" #include "expr/command.h" -#include "util/result.h" #include "util/Assert.h" +#include "util/configuration.h" #include "util/output.h" #include "util/options.h" +#include "util/result.h" using namespace std; using namespace CVC4; @@ -54,28 +55,28 @@ int main(int argc, char* argv[]) { try { return runCvc4(argc, argv); } catch(OptionException& e) { - if(options.smtcomp_mode) { - cout << "unknown" << endl; - } +#ifdef CVC4_COMPETITION_MODE + cout << "unknown" << endl; +#endif cerr << "CVC4 Error:" << endl << e << endl; printf(usage, options.binary_name.c_str()); exit(1); } catch(Exception& e) { - if(options.smtcomp_mode) { - cout << "unknown" << endl; - } +#ifdef CVC4_COMPETITION_MODE + cout << "unknown" << endl; +#endif cerr << "CVC4 Error:" << endl << e << endl; exit(1); } catch(bad_alloc) { - if(options.smtcomp_mode) { - cout << "unknown" << endl; - } +#ifdef CVC4_COMPETITION_MODE + cout << "unknown" << endl; +#endif cerr << "CVC4 ran out of memory." << endl; exit(1); } catch(...) { - if(options.smtcomp_mode) { - cout << "unknown" << endl; - } +#ifdef CVC4_COMPETITION_MODE + cout << "unknown" << endl; +#endif cerr << "CVC4 threw an exception of unknown type." << endl; exit(1); } @@ -90,9 +91,9 @@ int runCvc4(int argc, char* argv[]) { int firstArgIndex = parseOptions(argc, argv, &options); // If in competition mode, set output stream option to flush immediately - if(options.smtcomp_mode) { - cout << unitbuf; - } +#ifdef CVC4_COMPETITION_MODE + cout << unitbuf; +#endif /* NOTE: ANTLR3 doesn't support input from stdin */ if(firstArgIndex >= argc) { @@ -128,7 +129,7 @@ int runCvc4(int argc, char* argv[]) { } // Determine which messages to show based on smtcomp_mode and verbosity - if(options.smtcomp_mode) { + if(Configuration::isMuzzledBuild()) { Debug.setStream(CVC4::null_os); Trace.setStream(CVC4::null_os); Notice.setStream(CVC4::null_os); @@ -160,7 +161,7 @@ int runCvc4(int argc, char* argv[]) { // } Parser parser(&exprMgr, input); - if(!options.semanticChecks) { + if(!options.semanticChecks || Configuration::isMuzzledBuild()) { parser.disableChecks(); } diff --git a/src/main/usage.h b/src/main/usage.h index c8ca6a179..4c600759f 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -30,18 +30,23 @@ CVC4 options:\n\ --lang | -L force input language (default is `auto'; see --lang help)\n\ --version | -V identify this CVC4 binary\n\ --help | -h this command line reference\n\ + --parse-only exit after parsing input\n\ + --mmap memory map file input\n\ + --show-config show CVC4 static configuration\n" +#ifdef CVC4_DEBUG +"\ + --segv-nospin don't spin on segfault waiting for gdb\n" +#endif +#ifndef CVC4_MUZZLE +"\ + --no-checking disable semantic checks in the parser\n\ --verbose | -v increase verbosity (repeatable)\n\ --quiet | -q decrease verbosity (repeatable)\n\ --trace | -t tracing for something (e.g. --trace pushpop)\n\ --debug | -d debugging for something (e.g. --debug arith), implies -t\n\ - --smtcomp competition mode (very quiet)\n\ - --stats give statistics on exit\n\ - --segv-nospin (debug builds only) don't spin on segfault waiting for gdb\n\ - --parse-only exit after parsing input\n\ - --no-checking disable semantic checks in the parser\n\ - --mmap memory map file input\n\ - --show-config show CVC4 static configuration\n\ -"; + --stats give statistics on exit\n" +#endif +; }/* CVC4::main namespace */ }/* CVC4 namespace */ diff --git a/src/util/options.h b/src/util/options.h index 63f1cb99e..d095d98d3 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -29,7 +29,6 @@ struct CVC4_PUBLIC Options { std::string binary_name; - bool smtcomp_mode; bool statistics; std::ostream *out; @@ -55,7 +54,6 @@ struct CVC4_PUBLIC Options { bool memoryMap; Options() : binary_name(), - smtcomp_mode(false), statistics(false), out(0), err(0), diff --git a/src/util/output.h b/src/util/output.h index 79bdd788e..ea96606cb 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -343,6 +343,14 @@ public: extern NullDebugC debugNullCvc4Stream CVC4_PUBLIC; extern NullC nullCvc4Stream CVC4_PUBLIC; +inline bool debugTagIsOn(std::string tag) { +#ifdef CVC4_DEBUG + return DebugOut.isOn(tag); +#else + return false; +#endif +} + }/* CVC4 namespace */ #endif /* __CVC4__OUTPUT_H */ -- 2.30.2