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.

diff --git a/configure.ac b/configure.ac
index 93f8f2ee5473f72959cad304b3ec1675132fabc5..e80c80e24cb921042b8fc1bb63173688efb6f335 100644 (file)
--- 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 2be116baa37a4199926cdd1a2e67594500b56ae7..2de6e2051be10e7d41ab167fe712f485906c64a5 100644 (file)
--- 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 a09da850dbef1a3b5213c816e7de3f4db5a187da..b24e91803b00cd235c764c5e110dff3df9ca0702 100644 (file)
--- 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 a575426fd181b1c63d55c1b74a32327916c9adc3..037dde559af2e2f79c1c13197d6043642cf46d41 100644 (file)
--- 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 c8ca6a1793560f04b3baf823bdb9322a3a5bef2b..4c600759f3df3d2866af314affdda466f3e67338 100644 (file)
--- 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 63f1cb99e2b8719788e637291f5dc31583cc03d7..d095d98d33aadd9ad0aefa5950fd4daaa30499f5 100644 (file)
--- 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 79bdd788ea47257f444808c4d62ee4fc26ea4835..ea96606cb89595197ed45b9521860d49a393ef42 100644 (file)
--- 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 */