From ec83ced90e3c4db2b2b31458628a1957fc684484 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 14 Apr 2020 13:38:20 -0500 Subject: [PATCH] Remove early type check option (#4234) Required to decouple options from NodeManager. This option is now always enabled in debug, and disabled in production. --- src/expr/node_builder.h | 12 +++++------- src/expr/node_manager.cpp | 11 +++++++++-- src/options/expr_options.toml | 9 --------- 3 files changed, 14 insertions(+), 18 deletions(-) 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::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" -- 2.30.2