diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-27 23:43:24 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-27 23:43:24 +0000 |
commit | 0eb82499822544f96877f317bbbcd4cb7c644614 (patch) | |
tree | 7abbd631cb9c5e065883f9eb8babccc62a9fbb00 /src/expr/node_value.cpp | |
parent | e56c41f47d43103a6e8bf744e12229ed6e5a8f19 (diff) |
A bag of unrelated fixes to bring trunk more in-line with recent
policy discussion (no dead code, no unimplemented unit tests...), and
other fixes:
* src/expr/node_builder.h: uncomment AndNodeBuilder, OrNodeBuilder,
PlusNodeBuilder, and MultNodeBuilder. (These had been dead code for
awhile.)
* src/expr/node_value.cpp: toString() is much more reasonable now,
printing S-exprs and using variable names (instead of printing raw
pointer values). Next, we'll want to define a pretty-printing
theory interface and perhaps hook this up to that.
* test/unit/expr/node_black.h: implement testIterator(),
testToString(), and testToStream().
* test/unit/expr/node_builder_black.h: implement testIterator() and
testAppend(), and add some code to avoid the warnings on clear() for
unused NodeBuilders.
* src/expr/node_builder.h: redefine "iterator" to be over Nodes rather
than over NodeValues. Doesn't make sense to expose the underlying
NodeValues. This shouldn't affect anyone, no one was using
NodeBuilder iterators.
* fix some comments in source code
Diffstat (limited to 'src/expr/node_value.cpp')
-rw-r--r-- | src/expr/node_value.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 63fe0c84a..b95f8ff0a 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -36,24 +36,24 @@ string NodeValue::toString() const { } void NodeValue::toStream(std::ostream& out) const { - out << "(" << Kind(d_kind); if(d_kind == kind::VARIABLE) { Node n(this); string s; if(n.hasAttribute(VarNameAttr(), s)) { - out << ":" << s; + out << s; } else { - out << ":" << this; + out << "var_" << d_id; } } else { + out << "(" << Kind(d_kind); for(const_nv_iterator i = nv_begin(); i != nv_end(); ++i) { if(i != nv_end()) { out << " "; } - out << *i; + Node(*i).toStream(out); } + out << ")"; } - out << ")"; } }/* CVC4 namespace */ |