diff options
author | Tim King <taking@cs.nyu.edu> | 2010-02-26 18:58:17 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-02-26 18:58:17 +0000 |
commit | 3311e8276fb6221d9e100be2b1eec88d8f119fef (patch) | |
tree | ef0ceebcd85b1153a25af7438c4bae96fe5aecb8 /src/expr/node.h | |
parent | 12cc3d32407cabbc8c3ed3d980199a020b61a883 (diff) |
TheoryUFWhite tests are added. There are also accompanying bug fixes. These currently do not pass. (See bug 39.) I modified node.h/cpp to get gdb debug printing working again
Diffstat (limited to 'src/expr/node.h')
-rw-r--r-- | src/expr/node.h | 36 |
1 files changed, 31 insertions, 5 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index 06f368583..25f0b7453 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -65,8 +65,8 @@ template<bool ref_count> class NodeTemplate { /** - * The NodeValue has access to the private constructors, so that the iterators - * can can create new nodes. + * The NodeValue has access to the private constructors, so that the + * iterators can can create new nodes. */ friend class NodeValue; @@ -100,8 +100,8 @@ template<bool ref_count> /** * Assigns the expression value and does reference counting. No assumptions - * are made on the expression, and should only be used if we know what we are - * doing. + * are made on the expression, and should only be used if we know what we + * are doing. * * @param ev the expression value to assign */ @@ -575,7 +575,7 @@ template<bool ref_count> if(ref_count) d_nv->dec(); Assert(ref_count || d_nv->d_rc > 0, - "Temporary node pointing to an expired node"); + "Temporary node pointing to an expired node"); } template<bool ref_count> @@ -675,6 +675,32 @@ template<bool ref_count> return NodeManager::currentNM()->getType(*this); } + + +/** + * Pretty printer for use within gdb. This is not intended to be used + * outside of gdb. This writes to the Warning() stream and immediately + * flushes the stream. + * + * Note that this function cannot be a template, since the compiler + * won't instantiate it. Even if we explicitly instantiate. (Odd?) + * So we implement twice. + * + * Tim's Note: I moved this into the node.h file because this allows gdb + * to find the symbol, and use it, which is the first standard this code needs + * to meet. A cleaner solution is welcomed. + */ +static void CVC4_PUBLIC debugPrintNode(const NodeTemplate<true>& n) { + n.printAst(Warning(), 0); + Warning().flush(); +} + +static void CVC4_PUBLIC debugPrintTNode(const NodeTemplate<false>& n) { + n.printAst(Warning(), 0); + Warning().flush(); +} + + }/* CVC4 namespace */ #endif /* __CVC4__NODE_H */ |