* Option --no-type-checking now disables type checks in SmtEngine

* Adding options --lazy-type-checking and --eager-type-checking
  to control type checking in NodeBuilder, which can now be enabled
  in production mode and disabled in debug mode
* Option --no-checking implies --no-type-checking
* Adding constructor SmtEngine(ExprManager* em) that uses default options

3 files changed, 24 insertions, 13 deletions

diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 5ddeced5d..25badb7e5 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -76,7 +76,9 @@ enum OptionValue {
   NO_INTERACTIVE,
   PRODUCE_MODELS,
   PRODUCE_ASSIGNMENTS,
-  NO_EARLY_TYPE_CHECKING
+  NO_TYPE_CHECKING,
+  LAZY_TYPE_CHECKING,
+  EAGER_TYPE_CHECKING,
 };/* enum OptionValue */
 
 /**
@@ -128,7 +130,9 @@ 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-type-checking", no_argument, NULL, NO_EARLY_TYPE_CHECKING},
+  { "no-type-checking", no_argument, NULL, NO_TYPE_CHECKING},
+  { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING},
+  { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING},
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
 
@@ -229,6 +233,8 @@ throw(OptionException) {
 
     case NO_CHECKING:
       opts->semanticChecks = false;
+      opts->typeChecking = false;
+      opts->earlyTypeChecking = false;
       break;
 
     case USE_MMAP:
@@ -302,10 +308,20 @@ throw(OptionException) {
       opts->produceAssignments = true;
       break;
 
-    case NO_EARLY_TYPE_CHECKING:
+    case NO_TYPE_CHECKING:
+      opts->typeChecking = false;
+      opts->earlyTypeChecking = false;
+      break;
+
+    case LAZY_TYPE_CHECKING:
       opts->earlyTypeChecking = false;
       break;
 
+    case EAGER_TYPE_CHECKING:
+      opts->typeChecking = true;
+      opts->earlyTypeChecking = true;
+      break;
+
     case SHOW_CONFIG:
       fputs(Configuration::about().c_str(), stdout);
       printf("\n");
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 8f790c211..8ed938351 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -128,18 +128,11 @@ int runCvc4(int argc, char* argv[]) {
     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);
 
   // Create the SmtEngine
-  SmtEngine smt(&exprMgr, &options);
+  SmtEngine smt(&exprMgr, options);
 
   // Auto-detect input language by filename extension
   const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
diff --git a/src/main/usage.h b/src/main/usage.h
index 7affc254c..5ad96aea6 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -37,8 +37,10 @@ CVC4 options:\n\
    --mmap                 memory map file input\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\
-   --no-type-checking     disable type checking [default in non-debug builds]\n\
+   --lazy-type-checking   type check expressions only when necessary (default)\n\
+   --eager-type-checking  type check expressions immediately on creation\n\
+   --no-type-checking     never type check expressions\n\
+   --no-checking          disable ALL semantic checks, including type checks \n\
    --strict-parsing       fail on non-conformant inputs (SMT2 only)\n\
    --verbose | -v         increase verbosity (repeatable)\n\
    --quiet | -q           decrease verbosity (repeatable)\n\