Remove early type check option (#4234)

Required to decouple options from NodeManager.

This option is now always enabled in debug, and disabled in production.

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index b6594a933a1c9f64a3e85674eb974ada0d43ae2a..fb1d0fa6ac6f5e84aa40065f0f6d4027d78131ca 100644 (file)
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -1311,13 +1311,11 @@ inline void NodeBuilder<nchild_thresh>::maybeCheckType(const TNode n) const
 {
   /* force an immediate type check, if early type checking is
      enabled and the current node isn't a variable or constant */
-  if( d_nm->getOptions()[options::earlyTypeChecking] ) {
-    kind::MetaKind mk = n.getMetaKind();
-    if( mk != kind::metakind::VARIABLE
-        && mk != kind::metakind::NULLARY_OPERATOR
-        && mk != kind::metakind::CONSTANT ) {
-      d_nm->getType(n, true);
-    }
+  kind::MetaKind mk = n.getMetaKind();
+  if (mk != kind::metakind::VARIABLE && mk != kind::metakind::NULLARY_OPERATOR
+      && mk != kind::metakind::CONSTANT)
+  {
+    d_nm->getType(n, true);
   }
 }
 #endif /* CVC4_DEBUG */

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index efac349027dcd28d2423e8db8341e6b309916d23..feec9b78256efcae137606d4ed462e35b1c1e5fb 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -420,8 +420,15 @@ TypeNode NodeManager::getType(TNode n, bool check)
 
 
   Debug("getType") << this << " getting type for " << &n << " " << n << ", check=" << check << ", needsCheck = " << needsCheck << ", hasType = " << hasType << endl;
-  
-  if(needsCheck && !(*d_options)[options::earlyTypeChecking]) {
+
+#ifdef CVC4_DEBUG
+  // already did type check eagerly upon creation in node builder
+  bool doTypeCheck = false;
+#else
+  bool doTypeCheck = true;
+#endif
+  if (needsCheck && doTypeCheck)
+  {
     /* Iterate and compute the children bottom up. This avoids stack
        overflows in computeType() when the Node graph is really deep,
        which should only affect us when we're type checking lazily. */

diff --git a/src/options/expr_options.toml b/src/options/expr_options.toml
index d70765d69ef0dcb91e1f4b8f6f015cf79c1653b4..b64758fd2caea589f3778397fbf355ba525e74a1 100644 (file)
--- a/src/options/expr_options.toml
+++ b/src/options/expr_options.toml
@@ -35,15 +35,6 @@ header = "options/expr_options.h"
   read_only  = true
   help       = "print types with variables when printing exprs"
 
-[[option]]
-  name       = "earlyTypeChecking"
-  category   = "regular"
-  long       = "eager-type-checking"
-  type       = "bool"
-  default    = "USE_EARLY_TYPE_CHECKING_BY_DEFAULT"
-  read_only  = true
-  help       = "type check expressions immediately on creation (debug builds only)"
-
 [[option]]
   name       = "typeChecking"
   category   = "regular"