diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-29 18:33:33 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-29 18:33:33 +0000 |
| commit | 704b56f3f5bdba6601dd687c8e649e36de50a6e7 (patch) | |
| tree | d8c0f8cd427d3c29c7ad0f9bffc509b1d8651583 /src/expr | |
| parent | d7da09eaa58b0a6f12a80686cc565666d9e1dad2 (diff) | |
Adding configuration_private.h to allow inlining of configuration checks
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/node_manager.h | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index b7c7f871e..dcfb14b7a 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -37,6 +37,7 @@ #include "expr/metakind.h" #include "expr/node_value.h" #include "context/context.h" +#include "util/configuration_private.h" namespace CVC4 { @@ -788,7 +789,7 @@ inline TypeNode NodeManager::mkSort(const std::string& name) { template <unsigned nchild_thresh> inline Node NodeManager::doMkNode(NodeBuilder<nchild_thresh>& nb) { Node n = nb.constructNode(); - if( Configuration::isDebugBuild() ) { + if( IS_DEBUG_BUILD ) { // force an immediate type check getType(n,true); } @@ -798,7 +799,7 @@ inline Node NodeManager::doMkNode(NodeBuilder<nchild_thresh>& nb) { template <unsigned nchild_thresh> inline Node* NodeManager::doMkNodePtr(NodeBuilder<nchild_thresh>& nb) { Node* np = nb.constructNodePtr(); - if( Configuration::isDebugBuild() ) { + if( IS_DEBUG_BUILD ) { // force an immediate type check getType(*np,true); } |