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/node_manager.cpp | |
| 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/node_manager.cpp')
| -rw-r--r-- | src/expr/node_manager.cpp | 11 |
1 files changed, 9 insertions, 2 deletions
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. */ |