diff options
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/getopt.cpp | 22 | ||||
-rw-r--r-- | src/main/main.cpp | 37 | ||||
-rw-r--r-- | src/main/usage.h | 21 |
3 files changed, 39 insertions, 41 deletions
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 */ |