diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-14 13:38:20 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-04-14 13:38:20 -0500 |
| commit | ec83ced90e3c4db2b2b31458628a1957fc684484 (patch) | |
| tree | 1487dc7e625b627ecd470de23e8e9f6bef85bb91 /src/expr | |
| parent | 3dfb48b80034a9eb628db641c9cec172e53fa910 (diff) | |
Remove early type check option (#4234)
Required to decouple options from NodeManager.
This option is now always enabled in debug, and disabled in production.
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/node_builder.h | 12 | ||||
| -rw-r--r-- | src/expr/node_manager.cpp | 11 |
2 files changed, 14 insertions, 9 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<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. */ |