From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 14 Apr 2020 18:38:20 +0000 (-0500)
Subject: Remove early type check option (#4234)
X-Git-Tag: cvc5-1.0.0~3378
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ec83ced90e3c4db2b2b31458628a1957fc684484;p=cvc5.git

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 b6594a933..fb1d0fa6a 100644
--- 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 efac34902..feec9b782 100644
--- 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 d70765d69..b64758fd2 100644
--- 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"