* 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

14 files changed, 135 insertions, 67 deletions

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 4c8bc578a..095e81868 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -664,7 +664,7 @@ private:
   inline void debugCheckType(const TNode n) const {
     // force an immediate type check, if we are in debug mode
     // and the current node isn't a variable or constant
-    if( IS_DEBUG_BUILD && d_nm->d_earlyTypeChecking ) {
+    if( d_nm->d_earlyTypeChecking ) {
       kind::MetaKind mk = n.getMetaKind();
       if( mk != kind::metakind::VARIABLE 
           && mk != kind::metakind::CONSTANT ) {
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\
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index d7b1e6d99..f503efae2 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -57,15 +57,15 @@ public:
   }
 };
 
-PropEngine::PropEngine(const Options* opts, DecisionEngine* de,
-                       TheoryEngine* te, Context* context) :
+PropEngine::PropEngine(DecisionEngine* de, TheoryEngine* te, 
+                       Context* context, const Options& opts) :
   d_inCheckSat(false),
-  d_options(opts),
+  // d_options(opts),
   d_decisionEngine(de),
   d_theoryEngine(te),
   d_context(context) {
   Debug("prop") << "Constructing the PropEngine" << endl;
-  d_satSolver = new SatSolver(this, d_theoryEngine, d_context, d_options);
+  d_satSolver = new SatSolver(this, d_theoryEngine, d_context, opts);
   d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver);
   d_satSolver->setCnfStream(d_cnfStream);
 }
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 1dada2e69..1c7c506ee 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -26,11 +26,11 @@
 #include "expr/node.h"
 #include "util/result.h"
 #include "util/decision_engine.h"
+#include "smt/options.h"
 
 namespace CVC4 {
 
 class TheoryEngine;
-class Options;
 
 namespace prop {
 
@@ -50,7 +50,7 @@ class PropEngine {
   bool d_inCheckSat;
 
   /** The global options */
-  const Options *d_options;
+  //const Options d_options;
 
   /** The decision engine we will be using */
   DecisionEngine *d_decisionEngine;
@@ -76,7 +76,7 @@ public:
   /**
    * Create a PropEngine with a particular decision and theory engine.
    */
-  PropEngine(const Options*, DecisionEngine*, TheoryEngine*, context::Context*);
+  PropEngine(DecisionEngine*, TheoryEngine*, context::Context*, const Options&);
 
   /**
    * Destructor.
diff --git a/src/prop/sat.h b/src/prop/sat.h
index a335b733b..17bf447f8 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -125,7 +125,7 @@ class SatSolver : public SatInputInterface {
   context::Context* d_context;
 
   /** Remember the options */
-  Options* d_options;
+  // Options* d_options;
 
   /* Pointer to the concrete SAT solver. Including this via the
      preprocessor saves us a level of indirection vs, e.g., defining a
@@ -203,7 +203,7 @@ public:
   SatSolver(PropEngine* propEngine,
                    TheoryEngine* theoryEngine,
                    context::Context* context,
-                   const Options* options);
+                   const Options& options);
 
   ~SatSolver();
 
@@ -233,7 +233,7 @@ public:
 #ifdef __CVC4_USE_MINISAT
 
 inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
-                     context::Context* context, const Options* options) :
+                     context::Context* context, const Options& options) :
   d_propEngine(propEngine),
   d_cnfStream(NULL),
   d_theoryEngine(theoryEngine),
@@ -243,7 +243,7 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
   // Create the solver
   d_minisat = new Minisat::SimpSolver(this, d_context);
   // Setup the verbosity
-  d_minisat->verbosity = (options->verbosity > 0) ? 1 : -1;
+  d_minisat->verbosity = (options.verbosity > 0) ? 1 : -1;
 
   // No random choices
   if(Debug.isOn("no_rnd_decisions")){
diff --git a/src/smt/options.h b/src/smt/options.h
index 7ddaf5d4d..73c38545f 100644
--- a/src/smt/options.h
+++ b/src/smt/options.h
@@ -89,6 +89,9 @@ struct CVC4_PUBLIC Options {
   /** Whether we support SmtEngine::getAssignment() for this run. */
   bool produceAssignments;
 
+  /** Whether we do typechecking at all. */
+  bool typeChecking;
+
   /** Whether we do typechecking at Expr creation time. */
   bool earlyTypeChecking;
 
@@ -109,6 +112,7 @@ struct CVC4_PUBLIC Options {
     interactiveSetByUser(false),
     produceModels(false),
     produceAssignments(false),
+    typeChecking(true),
     earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT) {
   }
 };/* struct Options */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2f2fba848..d76a002e7 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -111,21 +111,20 @@ public:
 
 using namespace CVC4::smt;
 
-SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() :
-  d_context(em->getContext()),
-  d_exprManager(em),
-  d_nodeManager(em->getNodeManager()),
-  d_options(opts),
-  /* These next few are initialized below, after we have a NodeManager
-   * in scope. */
-  d_decisionEngine(NULL),
-  d_theoryEngine(NULL),
-  d_propEngine(NULL),
-  d_definedFunctions(NULL),
-  d_assertionList(NULL),
-  d_assignments(NULL),
-  d_haveAdditions(false),
-  d_status() {
+SmtEngine::SmtEngine(ExprManager* em) throw() :
+  d_exprManager(em) {
+  Options opts;
+  init(opts);
+}
+
+SmtEngine::SmtEngine(ExprManager* em, const Options& opts) throw() :
+  d_exprManager(em){
+  init(opts);
+}
+
+void SmtEngine::init(const Options& opts) throw() {
+  d_context = d_exprManager->getContext();
+  d_nodeManager = d_exprManager->getNodeManager();
 
   NodeManagerScope nms(d_nodeManager);
 
@@ -133,15 +132,26 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() :
   // We have mutual dependancy here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
   d_theoryEngine = new TheoryEngine(d_context, opts);
-  d_propEngine = new PropEngine(opts, d_decisionEngine,
-                                d_theoryEngine, d_context);
+  d_propEngine = new PropEngine(d_decisionEngine, d_theoryEngine, 
+                                d_context, opts);
   d_theoryEngine->setPropEngine(d_propEngine);
 
   d_definedFunctions = new(true) DefinedFunctionMap(d_context);
 
-  if(d_options->interactive) {
+  d_assertionList = NULL;
+  d_interactive = opts.interactive;
+  if(d_interactive) {
     d_assertionList = new(true) AssertionList(d_context);
   }
+
+  d_assignments = NULL;
+  d_haveAdditions = false;
+
+  d_typeChecking = opts.typeChecking;
+  d_lazyDefinitionExpansion = opts.lazyDefinitionExpansion;
+  d_produceModels = opts.produceModels;
+  d_produceAssignments = opts.produceAssignments;
+
 }
 
 void SmtEngine::shutdown() {
@@ -299,7 +309,7 @@ void SmtEngine::defineFunction(Expr func,
                                Expr formula) {
   Debug("smt") << "SMT defineFunction(" << func << ")" << endl;
   NodeManagerScope nms(d_nodeManager);
-  Type formulaType = formula.getType(true);// type check body
+  Type formulaType = formula.getType(d_typeChecking);// type check body
   Type funcType = func.getType();
   Type rangeType = funcType.isFunction() ?
     FunctionType(funcType).getRangeType() : funcType;
@@ -388,7 +398,7 @@ Node SmtEnginePrivate::expandDefinitions(SmtEngine& smt, TNode n)
 
 Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode n)
   throw(NoSuchFunctionException, AssertionException) {
-  if(!smt.d_options->lazyDefinitionExpansion) {
+  if(!smt.d_lazyDefinitionExpansion) {
     Node node = expandDefinitions(smt, n);
     Debug("expand") << "have: " << n << endl
                     << "made: " << node << endl;
@@ -416,7 +426,7 @@ void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n)
 }
 
 void SmtEngine::ensureBoolean(const BoolExpr& e) {
-  Type type = e.getType(true);
+  Type type = e.getType(d_typeChecking);
   Type boolType = d_exprManager->booleanType();
   if(type != boolType) {
     stringstream ss;
@@ -468,7 +478,9 @@ Result SmtEngine::assertFormula(const BoolExpr& e) {
 Expr SmtEngine::simplify(const Expr& e) {
   Assert(e.getExprManager() == d_exprManager);
   NodeManagerScope nms(d_nodeManager);
-  e.getType(true);// ensure expr is type-checked at this point
+  if( d_typeChecking ) {
+    e.getType(true);// ensure expr is type-checked at this point
+  }
   Debug("smt") << "SMT simplify(" << e << ")" << endl;
   Unimplemented();
 }
@@ -476,14 +488,14 @@ Expr SmtEngine::simplify(const Expr& e) {
 Expr SmtEngine::getValue(const Expr& e)
   throw(ModalException, AssertionException) {
   Assert(e.getExprManager() == d_exprManager);
-  Type type = e.getType(true);// ensure expr is type-checked at this point
+  Type type = e.getType(d_typeChecking);// ensure expr is type-checked at this point
   Debug("smt") << "SMT getValue(" << e << ")" << endl;
-  if(!d_options->interactive) {
+  if(!d_interactive) {
     const char* msg =
       "Cannot get value when not in interactive mode.";
     throw ModalException(msg);
   }
-  if(!d_options->produceModels) {
+  if(!d_produceModels) {
     const char* msg =
       "Cannot get value when produce-models options is off.";
     throw ModalException(msg);
@@ -510,13 +522,13 @@ Expr SmtEngine::getValue(const Expr& e)
   Node resultNode = d_theoryEngine->getValue(n);
 
   // type-check the result we got
-  Assert(resultNode.isNull() || resultNode.getType(true) == eNode.getType());
+  Assert(resultNode.isNull() || resultNode.getType() == eNode.getType());
   return Expr(d_exprManager, new Node(resultNode));
 }
 
 bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Type type = e.getType(true);
+  Type type = e.getType(d_typeChecking);
   // must be Boolean
   CheckArgument( type.isBoolean(), e,
                  "expected Boolean-typed variable or function application "
@@ -530,7 +542,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
                    n.getMetaKind() == kind::metakind::VARIABLE ), e,
                  "expected variable or defined-function application "
                  "in addToAssignment(),\ngot %s", e.toString().c_str() );
-  if(!d_options->produceAssignments) {
+  if(!d_produceAssignments) {
     return false;
   }
   if(d_assignments == NULL) {
@@ -543,7 +555,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
 
 SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
   Debug("smt") << "SMT getAssignment()" << endl;
-  if(!d_options->produceAssignments) {
+  if(!d_produceAssignments) {
     const char* msg =
       "Cannot get the current assignment when "
       "produce-assignments option is off.";
@@ -576,7 +588,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
     Node resultNode = d_theoryEngine->getValue(n);
 
     // type-check the result we got
-    Assert(resultNode.isNull() || resultNode.getType(true) == boolType);
+    Assert(resultNode.isNull() || resultNode.getType() == boolType);
 
     vector<SExpr> v;
     if((*i).getKind() == kind::APPLY) {
@@ -595,7 +607,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
 vector<Expr> SmtEngine::getAssertions()
   throw(ModalException, AssertionException) {
   Debug("smt") << "SMT getAssertions()" << endl;
-  if(!d_options->interactive) {
+  if(!d_interactive) {
     const char* msg =
       "Cannot query the current assertion list when not in interactive mode.";
     throw ModalException(msg);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index a3116dfa9..0831a0447 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -34,6 +34,7 @@
 #include "util/hash.h"
 #include "smt/modal_exception.h"
 #include "smt/no_such_function_exception.h"
+#include "smt/options.h"
 #include "smt/bad_option_exception.h"
 
 // In terms of abstraction, this is below (and provides services to)
@@ -47,7 +48,6 @@ typedef NodeTemplate<true> Node;
 typedef NodeTemplate<false> TNode;
 class NodeHashFunction;
 class Command;
-class Options;
 class TheoryEngine;
 class DecisionEngine;
 
@@ -99,7 +99,7 @@ class CVC4_PUBLIC SmtEngine {
   /** Out internal expression/node manager */
   NodeManager* d_nodeManager;
   /** User-level options */
-  const Options* d_options;
+  //const Options d_options;
   /** The decision engine */
   DecisionEngine* d_decisionEngine;
   /** The decision engine */
@@ -126,11 +126,39 @@ class CVC4_PUBLIC SmtEngine {
    */
   bool d_haveAdditions;
 
+  /** 
+   * Whether or not to type check input expressions.
+   */
+  bool d_typeChecking;
+
+  /**
+   * Whether we're being used in an interactive setting.
+   */
+  bool d_interactive;
+
+  /**
+   * Whether we expand function definitions lazily.
+   */
+  bool d_lazyDefinitionExpansion;
+
+  /**
+   * Whether getValue() is enabled.
+   */
+  bool d_produceModels;
+
+  /**
+   * Whether getAssignment() is enabled.
+   */
+  bool d_produceAssignments;
+
   /**
    * Most recent result of last checkSat/query or (set-info :status).
    */
   Result d_status;
 
+  /** Called by the constructors to setup fields. */
+  void init(const Options& opts) throw();
+
   /**
    * This is called by the destructor, just before destroying the
    * PropEngine, TheoryEngine, and DecisionEngine (in that order).  It
@@ -163,9 +191,14 @@ class CVC4_PUBLIC SmtEngine {
 public:
 
   /**
+   * Construct an SmtEngine with the given expression manager.
+   */
+  SmtEngine(ExprManager* em) throw();
+
+  /**
    * Construct an SmtEngine with the given expression manager and user options.
    */
-  SmtEngine(ExprManager* em, const Options* opts) throw();
+  SmtEngine(ExprManager* em, const Options& opts) throw();
 
   /**
    * Destruct the SMT engine.
@@ -273,6 +306,13 @@ public:
    */
   void pop();
 
+  /** Enable type checking. Forces a type check on any Expr parameter
+      to an SmtEngine method. */
+  void enableTypeChecking() { d_typeChecking = true; }
+
+  /** Disable type checking. */
+  void disableTypeChecking() { d_typeChecking = false; }
+
 };/* class SmtEngine */
 
 }/* CVC4 namespace */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 4113466d7..2fcfc9626 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -126,7 +126,7 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
   }
 }
 
-TheoryEngine::TheoryEngine(context::Context* ctxt, const Options* opts) :
+TheoryEngine::TheoryEngine(context::Context* ctxt, const Options& opts) :
   d_propEngine(NULL),
   d_theoryOut(this, ctxt),
   d_hasShutDown(false),
@@ -137,7 +137,7 @@ TheoryEngine::TheoryEngine(context::Context* ctxt, const Options* opts) :
 
   d_builtin = new theory::builtin::TheoryBuiltin(0, ctxt, d_theoryOut);
   d_bool = new theory::booleans::TheoryBool(1, ctxt, d_theoryOut);
-  switch(opts->uf_implementation) {
+  switch(opts.uf_implementation) {
   case Options::TIM:
     d_uf = new theory::uf::tim::TheoryUFTim(2, ctxt, d_theoryOut);
     break;
@@ -145,7 +145,7 @@ TheoryEngine::TheoryEngine(context::Context* ctxt, const Options* opts) :
     d_uf = new theory::uf::morgan::TheoryUFMorgan(2, ctxt, d_theoryOut);
     break;
   default:
-    Unhandled(opts->uf_implementation);
+    Unhandled(opts.uf_implementation);
   }
   d_arith = new theory::arith::TheoryArith(3, ctxt, d_theoryOut);
   d_arrays = new theory::arrays::TheoryArrays(4, ctxt, d_theoryOut);
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index ca39001fe..0bca372ca 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -22,10 +22,11 @@
 #define __CVC4__THEORY_ENGINE_H
 
 #include "expr/node.h"
-#include "theory/theory.h"
-#include "theory/theoryof_table.h"
 #include "prop/prop_engine.h"
+#include "smt/options.h"
 #include "theory/shared_term_manager.h"
+#include "theory/theory.h"
+#include "theory/theoryof_table.h"
 #include "util/stats.h"
 
 namespace CVC4 {
@@ -206,7 +207,7 @@ public:
   /**
    * Construct a theory engine.
    */
-  TheoryEngine(context::Context* ctxt, const Options* opts);
+  TheoryEngine(context::Context* ctxt, const Options& opts);
 
   /**
    * Destroy a theory engine.
diff --git a/test/unit/theory/shared_term_manager_black.h b/test/unit/theory/shared_term_manager_black.h
index 3e7a9f523..5007f43ed 100644
--- a/test/unit/theory/shared_term_manager_black.h
+++ b/test/unit/theory/shared_term_manager_black.h
@@ -61,7 +61,7 @@ public:
     d_nm = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nm);
 
-    d_theoryEngine = new TheoryEngine(d_ctxt, &d_options);
+    d_theoryEngine = new TheoryEngine(d_ctxt, d_options);
   }
 
   void tearDown() {
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 12c38d0d7..00766ec90 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -248,7 +248,7 @@ public:
     d_bv = new FakeTheory(d_ctxt, *d_nullChannel, "BV");
 
     // create the TheoryEngine
-    d_theoryEngine = new TheoryEngine(d_ctxt, &d_options);
+    d_theoryEngine = new TheoryEngine(d_ctxt, d_options);
 
     // insert our fake versions into the TheoryEngine's theoryOf table
     d_theoryEngine->d_theoryOfTable.