Changing --no-early-type-checking to --no-type-checking

Disabling type checking when --no-checking is given (Fixes: #221)

3 files changed, 12 insertions, 9 deletions

diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 57aa84a57..5ddeced5d 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -128,7 +128,7 @@ static struct option cmdlineOptions[] = {
   { "no-interactive", no_argument   , NULL, NO_INTERACTIVE },
   { "produce-models", no_argument   , NULL, PRODUCE_MODELS},
   { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS},
-  { "no-early-type-checking", no_argument, NULL, NO_EARLY_TYPE_CHECKING},
+  { "no-type-checking", no_argument, NULL, NO_EARLY_TYPE_CHECKING},
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
 
diff --git a/src/main/main.cpp b/src/main/main.cpp
index fd7c1b303..8f790c211 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -123,15 +123,18 @@ int runCvc4(int argc, char* argv[]) {
   const bool inputFromStdin =
     firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]);
 
-  // if we're reading from stdin, default to interactive mode
-  // [chris 10/20/10] The expected behavior of interactive is
-  // different from the expected behavior of file input from
-  // stdin, due to EOL escapes in interactive mode
-
+  // if we're reading from stdin on a TTY, default to interactive mode
   if(!options.interactiveSetByUser) {
     options.interactive = inputFromStdin && isatty(fileno(stdin));
   }
 
+  /* Early type checking can be turned off by --no-type-checking OR
+     --no-checking. We're assuming that earlyTypeChecking is not
+     explicitly set by the user. */
+  if(options.earlyTypeChecking) {
+    options.earlyTypeChecking = options.semanticChecks;
+  }
+
   // Create the expression manager
   ExprManager exprMgr(options.earlyTypeChecking);
 
diff --git a/src/main/usage.h b/src/main/usage.h
index ed35e76e8..7affc254c 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -38,7 +38,8 @@ CVC4 options:\n\
    --show-config          show CVC4 static configuration\n\
    --segv-nospin          don't spin on segfault waiting for gdb\n\
    --no-checking          disable semantic checks in the parser\n\
-   --strict-parsing       fail on inputs that are not strictly conformant (SMT2 only)\n\
+   --no-type-checking     disable type checking [default in non-debug builds]\n\
+   --strict-parsing       fail on non-conformant inputs (SMT2 only)\n\
    --verbose | -v         increase verbosity (repeatable)\n\
    --quiet | -q           decrease verbosity (repeatable)\n\
    --trace | -t           tracing for something (e.g. --trace pushpop)\n\
@@ -51,8 +52,7 @@ CVC4 options:\n\
    --no-interactive       do not run interactively\n\
    --produce-models       support the get-value command\n\
    --produce-assignments  support the get-assignment command\n\
-   --lazy-definition-expansion expand define-fun lazily\n\
-   --no-early-type-checking don't typecheck at Expr creation [non-DEBUG builds never do]\n";
+   --lazy-definition-expansion expand define-fun lazily\n";
 
 }/* CVC4::main namespace */
 }/* CVC4 namespace */