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.

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 */