From 0eb82499822544f96877f317bbbcd4cb7c644614 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sat, 27 Feb 2010 23:43:24 +0000 Subject: [PATCH] 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 --- src/expr/node_builder.h | 123 ++++++++++++++++----------- src/expr/node_value.cpp | 10 +-- src/expr/node_value.h | 8 ++ src/smt/smt_engine.h | 1 + src/theory/arith/kinds | 2 + src/theory/theoryof_table_epilogue.h | 3 +- src/theory/theoryof_table_middle.h | 3 +- src/theory/theoryof_table_prologue.h | 3 +- test/unit/expr/node_black.h | 53 +++++++++--- test/unit/expr/node_builder_black.h | 118 ++++++++++++++++--------- 10 files changed, 214 insertions(+), 110 deletions(-) diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index c1b2a87d2..f5da56d96 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -114,24 +114,17 @@ public: inline NodeBuilder(NodeManager* nm, Kind k); inline ~NodeBuilder(); - typedef NodeValue::nv_iterator iterator; - typedef NodeValue::const_nv_iterator const_iterator; + typedef NodeValue::iterator iterator; + typedef NodeValue::iterator const_iterator; - iterator begin() { - Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); - return d_nv->nv_begin(); - } - iterator end() { - Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); - return d_nv->nv_end(); - } const_iterator begin() const { Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); - return d_nv->nv_begin(); + return d_nv->begin(); } + const_iterator end() const { Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); - return d_nv->nv_end(); + return d_nv->end(); } Kind getKind() const { @@ -186,6 +179,7 @@ public: } NodeBuilder& operator<<(TNode n) { + // FIXME: collapse if ! UNDEFINED_KIND Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); return append(n); } @@ -223,7 +217,6 @@ public: d_nv->toStream(out); } - /* AndNodeBuilder operator&&(Node); OrNodeBuilder operator||(Node); PlusNodeBuilder operator+ (Node); @@ -234,7 +227,6 @@ public: friend class OrNodeBuilder; friend class PlusNodeBuilder; friend class MultNodeBuilder; - */ //Yet 1 more example of how terrifying C++ is as a language //This is needed for copy constructors of different sizes to access private fields @@ -242,54 +234,59 @@ public: };/* class NodeBuilder */ -#if 0 class AndNodeBuilder { - NodeBuilder d_eb; + NodeBuilder<> d_eb; public: - AndNodeBuilder(const NodeBuilder& eb) : d_eb(eb) { - if(d_eb.d_kind != AND) { - d_eb.collapse(); - d_eb.d_kind = AND; + AndNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { + if(d_eb.d_nv->d_kind != kind::AND) { + Node n = d_eb; + d_eb.clear(); + d_eb.d_nv->d_kind = kind::AND; + d_eb.append(n); } } AndNodeBuilder& operator&&(Node); OrNodeBuilder operator||(Node); - operator NodeBuilder() { return d_eb; } + operator NodeBuilder<>() { return d_eb; } };/* class AndNodeBuilder */ class OrNodeBuilder { - NodeBuilder d_eb; + NodeBuilder<> d_eb; public: - OrNodeBuilder(const NodeBuilder& eb) : d_eb(eb) { - if(d_eb.d_kind != OR) { - d_eb.collapse(); - d_eb.d_kind = OR; + OrNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { + if(d_eb.d_nv->d_kind != kind::OR) { + Node n = d_eb; + d_eb.clear(); + d_eb.d_nv->d_kind = kind::OR; + d_eb.append(n); } } AndNodeBuilder operator&&(Node); OrNodeBuilder& operator||(Node); - operator NodeBuilder() { return d_eb; } + operator NodeBuilder<>() { return d_eb; } };/* class OrNodeBuilder */ class PlusNodeBuilder { - NodeBuilder d_eb; + NodeBuilder<> d_eb; public: - PlusNodeBuilder(const NodeBuilder& eb) : d_eb(eb) { - if(d_eb.d_kind != PLUS) { - d_eb.collapse(); - d_eb.d_kind = PLUS; + PlusNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { + if(d_eb.d_nv->d_kind != kind::PLUS) { + Node n = d_eb; + d_eb.clear(); + d_eb.d_nv->d_kind = kind::PLUS; + d_eb.append(n); } } @@ -297,19 +294,21 @@ public: PlusNodeBuilder& operator-(Node); MultNodeBuilder operator*(Node); - operator NodeBuilder() { return d_eb; } + operator NodeBuilder<>() { return d_eb; } };/* class PlusNodeBuilder */ class MultNodeBuilder { - NodeBuilder d_eb; + NodeBuilder<> d_eb; public: - MultNodeBuilder(const NodeBuilder& eb) : d_eb(eb) { - if(d_eb.d_kind != MULT) { - d_eb.collapse(); - d_eb.d_kind = MULT; + MultNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { + if(d_eb.d_nv->d_kind != kind::MULT) { + Node n = d_eb; + d_eb.clear(); + d_eb.d_nv->d_kind = kind::MULT; + d_eb.append(n); } } @@ -317,27 +316,32 @@ public: PlusNodeBuilder operator-(Node); MultNodeBuilder& operator*(Node); - operator NodeBuilder() { return d_eb; } + operator NodeBuilder<>() { return d_eb; } };/* class MultNodeBuilder */ -inline AndNodeBuilder NodeBuilder::operator&&(Node e) { +template +inline AndNodeBuilder NodeBuilder::operator&&(Node e) { return AndNodeBuilder(*this) && e; } -inline OrNodeBuilder NodeBuilder::operator||(Node e) { +template +inline OrNodeBuilder NodeBuilder::operator||(Node e) { return OrNodeBuilder(*this) || e; } -inline PlusNodeBuilder NodeBuilder::operator+ (Node e) { +template +inline PlusNodeBuilder NodeBuilder::operator+ (Node e) { return PlusNodeBuilder(*this) + e; } -inline PlusNodeBuilder NodeBuilder::operator- (Node e) { +template +inline PlusNodeBuilder NodeBuilder::operator- (Node e) { return PlusNodeBuilder(*this) - e; } -inline MultNodeBuilder NodeBuilder::operator* (Node e) { +template +inline MultNodeBuilder NodeBuilder::operator* (Node e) { return MultNodeBuilder(*this) * e; } @@ -347,11 +351,17 @@ inline AndNodeBuilder& AndNodeBuilder::operator&&(Node e) { } inline OrNodeBuilder AndNodeBuilder::operator||(Node e) { - return OrNodeBuilder(d_eb.collapse()) || e; + Node n = d_eb; + d_eb.clear(); + d_eb.append(n); + return OrNodeBuilder(d_eb) || e; } inline AndNodeBuilder OrNodeBuilder::operator&&(Node e) { - return AndNodeBuilder(d_eb.collapse()) && e; + Node n = d_eb; + d_eb.clear(); + d_eb.append(n); + return AndNodeBuilder(d_eb) && e; } inline OrNodeBuilder& OrNodeBuilder::operator||(Node e) { @@ -364,21 +374,32 @@ inline PlusNodeBuilder& PlusNodeBuilder::operator+(Node e) { return *this; } +/* inline PlusNodeBuilder& PlusNodeBuilder::operator-(Node e) { d_eb.append(e.uMinusExpr()); return *this; } +*/ inline MultNodeBuilder PlusNodeBuilder::operator*(Node e) { - return MultNodeBuilder(d_eb.collapse()) * e; + Node n = d_eb; + d_eb.clear(); + d_eb.append(n); + return MultNodeBuilder(d_eb) * e; } inline PlusNodeBuilder MultNodeBuilder::operator+(Node e) { - return MultNodeBuilder(d_eb.collapse()) + e; + Node n = d_eb; + d_eb.clear(); + d_eb.append(n); + return MultNodeBuilder(d_eb) + e; } inline PlusNodeBuilder MultNodeBuilder::operator-(Node e) { - return MultNodeBuilder(d_eb.collapse()) - e; + Node n = d_eb; + d_eb.clear(); + d_eb.append(n); + return MultNodeBuilder(d_eb) - e; } inline MultNodeBuilder& MultNodeBuilder::operator*(Node e) { @@ -386,8 +407,6 @@ inline MultNodeBuilder& MultNodeBuilder::operator*(Node e) { return *this; } -#endif /* 0 */ - }/* CVC4 namespace */ #include "expr/node.h" @@ -567,7 +586,7 @@ inline void NodeBuilder::dealloc() { Assert(!d_used, "Internal error: NodeBuilder: dealloc() called with d_used"); - for(iterator i = d_nv->nv_begin(); + for(NodeValue::nv_iterator i = d_nv->nv_begin(); i != d_nv->nv_end(); ++i) { (*i)->dec(); 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 */ diff --git a/src/expr/node_value.h b/src/expr/node_value.h index e8435df26..0ad7ba559 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -33,6 +33,10 @@ namespace CVC4 { template class NodeTemplate; template class NodeBuilder; +class AndNodeBuilder; +class OrNodeBuilder; +class PlusNodeBuilder; +class MultNodeBuilder; class NodeManager; namespace expr { @@ -76,6 +80,10 @@ class NodeValue { template friend class CVC4::NodeTemplate; template friend class CVC4::NodeBuilder; + friend class CVC4::AndNodeBuilder; + friend class CVC4::OrNodeBuilder; + friend class CVC4::PlusNodeBuilder; + friend class CVC4::MultNodeBuilder; friend class CVC4::NodeManager; void inc(); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 594676416..7495e4100 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -24,6 +24,7 @@ #include "util/result.h" #include "util/model.h" +// FIXME private header in public code #include "expr/node.h" // In terms of abstraction, this is below (and provides services to) diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 994416838..fd784ccce 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -1 +1,3 @@ PLUS +MULT +UMINUS diff --git a/src/theory/theoryof_table_epilogue.h b/src/theory/theoryof_table_epilogue.h index 7483248ec..11f75183a 100644 --- a/src/theory/theoryof_table_epilogue.h +++ b/src/theory/theoryof_table_epilogue.h @@ -10,7 +10,8 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** The theoryOf table. + ** The epilogue section for the automatically-generated theoryOf table. + ** See the mktheoryof script. **/ };/* class TheoryOfTable */ diff --git a/src/theory/theoryof_table_middle.h b/src/theory/theoryof_table_middle.h index 17a945d01..f3ad433a3 100644 --- a/src/theory/theoryof_table_middle.h +++ b/src/theory/theoryof_table_middle.h @@ -10,7 +10,8 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** The theoryOf table. + ** The middle section for the automatically-generated theoryOf table. + ** See the mktheoryof script. **/ namespace CVC4 { diff --git a/src/theory/theoryof_table_prologue.h b/src/theory/theoryof_table_prologue.h index 47fd2d9b2..6e83d6d2c 100644 --- a/src/theory/theoryof_table_prologue.h +++ b/src/theory/theoryof_table_prologue.h @@ -10,7 +10,8 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** The theoryOf table. + ** The prologue section for the automatically-generated theoryOf table. + ** See the mktheoryof script. **/ #include "cvc4_private.h" diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 90358a622..c11d5cf86 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -17,6 +17,7 @@ //Used in some of the tests #include +#include #include "expr/expr_manager.h" #include "expr/node_value.h" @@ -449,24 +450,52 @@ public: } void testIterator(){ - /*typedef NodeValue::node_iterator iterator; */ - /*typedef NodeValue::node_iterator const_iterator; */ - - /*inline iterator begin(); */ - /*inline iterator end(); */ - /*inline const_iterator begin() const; */ - /*inline const_iterator end() const; */ + NodeBuilder<> b; + Node x = d_nodeManager->mkVar(); + Node y = d_nodeManager->mkVar(); + Node z = d_nodeManager->mkVar(); + Node n = b << x << y << z << kind::AND; + + { // iterator + Node::iterator i = n.begin(); + TS_ASSERT(*i++ == x); + TS_ASSERT(*i++ == y); + TS_ASSERT(*i++ == z); + TS_ASSERT(i == n.end()); + } - TS_WARN( "TODO: This test still needs to be written!" ); + { // same for const iterator + const Node& c = n; + Node::const_iterator i = c.begin(); + TS_ASSERT(*i++ == x); + TS_ASSERT(*i++ == y); + TS_ASSERT(*i++ == z); + TS_ASSERT(i == n.end()); + } } void testToString(){ - /*inline std::string toString() const; */ - TS_WARN( "TODO: This test still needs to be written!" ); + Node w = d_nodeManager->mkVar(NULL, "w"); + Node x = d_nodeManager->mkVar(NULL, "x"); + Node y = d_nodeManager->mkVar(NULL, "y"); + Node z = d_nodeManager->mkVar(NULL, "z"); + Node m = NodeBuilder<>() << w << x << kind::OR; + Node n = NodeBuilder<>() << m << y << z << kind::AND; + + TS_ASSERT(n.toString() == "(AND (OR w x) y z)"); } void testToStream(){ - /*inline void toStream(std::ostream&) const;*/ - TS_WARN( "TODO: This test still needs to be written!" ); + NodeBuilder<> b; + Node w = d_nodeManager->mkVar(NULL, "w"); + Node x = d_nodeManager->mkVar(NULL, "x"); + Node y = d_nodeManager->mkVar(NULL, "y"); + Node z = d_nodeManager->mkVar(NULL, "z"); + Node m = NodeBuilder<>() << x << y << kind::OR; + Node n = NodeBuilder<>() << w << m << z << kind::AND; + + stringstream sstr; + n.toStream(sstr); + TS_ASSERT(sstr.str() == "(AND w (OR x y) z)"); } }; diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 5dc327a67..e956806b8 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -24,6 +24,7 @@ #include "expr/node_manager.h" #include "expr/node.h" #include "expr/kind.h" +#include "util/Assert.h" using namespace CVC4; using namespace CVC4::kind; @@ -203,7 +204,28 @@ public: } void testIterator(){ - TS_WARN( "TODO: This test still needs to be written!" ); + NodeBuilder<> b; + Node x = d_nm->mkVar(); + Node y = d_nm->mkVar(); + Node z = d_nm->mkVar(); + b << x << y << z << kind::AND; + + { + NodeBuilder<>::iterator i = b.begin(); + TS_ASSERT(*i++ == x); + TS_ASSERT(*i++ == y); + TS_ASSERT(*i++ == z); + TS_ASSERT(i == b.end()); + } + + { + const NodeBuilder<>& c = b; + NodeBuilder<>::const_iterator i = c.begin(); + TS_ASSERT(*i++ == x); + TS_ASSERT(*i++ == y); + TS_ASSERT(*i++ == z); + TS_ASSERT(i == b.end()); + } } void testGetKind(){ @@ -241,6 +263,8 @@ public: push_back(noKind, K); TS_ASSERT_EQUALS(noKind.getNumChildren(), K+K); + noKind << AND;// avoid exception on marking it used + Node n = noKind;// avoid warning on clear() noKind.clear(); TS_ASSERT_EQUALS(noKind.getNumChildren(), 0); push_back(noKind, K); @@ -250,10 +274,9 @@ public: push_back(noKind, K); TS_ASSERT_EQUALS(noKind.getNumChildren(), K+K); - noKind << specKind; - Node n = noKind; - TS_ASSERT_THROWS_ANYTHING(noKind.getNumChildren();); + n = noKind; + TS_ASSERT_THROWS_ANYTHING( noKind.getNumChildren() ); } void testOperatorSquare(){ @@ -319,6 +342,7 @@ public: TS_ASSERT_EQUALS(nb.getNumChildren(), K); TS_ASSERT_DIFFERS(nb.begin(), nb.end()); + Node n = nb;// avoid warning on clear() nb.clear(); TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND); @@ -332,6 +356,7 @@ public: TS_ASSERT_EQUALS(nb.getNumChildren(), K); TS_ASSERT_DIFFERS(nb.begin(), nb.end()); + n = nb;// avoid warning on clear() nb.clear(specKind); TS_ASSERT_EQUALS(nb.getKind(), specKind); @@ -339,10 +364,9 @@ public: TS_ASSERT_EQUALS(nb.begin(), nb.end()); push_back(nb, K); - Node n = nb; + n = nb;// avoid warning on clear() nb.clear(); - TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND); TS_ASSERT_EQUALS(nb.getNumChildren(), 0); TS_ASSERT_EQUALS(nb.begin(), nb.end()); @@ -366,9 +390,9 @@ public: TS_ASSERT_EQUALS(modified.getKind(), specKind); NodeBuilder<> nb(specKind); - Node n = nb; + Node n = nb;// avoid warning on clear() nb.clear(PLUS); - TS_ASSERT_THROWS_ANYTHING(nb << PLUS;); + TS_ASSERT_THROWS_ANYTHING( nb << PLUS; ); NodeBuilder<> testRef; TS_ASSERT_EQUALS((testRef << specKind).getKind(), specKind); @@ -414,30 +438,53 @@ public: } void testAppend(){ - /* - NodeBuilder& append(const Node& n) { - Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); - Debug("prop") << "append: " << this << " " << n << "[" << n.d_ev << "]" << std::endl; - allocateEvIfNecessaryForAppend(); - NodeValue* ev = n.d_ev; - ev->inc(); - d_ev->d_children[d_ev->d_nchildren++] = ev; - return *this; - } - */ - /* - - template - NodeBuilder& append(const Iterator& begin, const Iterator& end) { - Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); - for(Iterator i = begin; i != end; ++i) { - append(*i); - } - return *this; - } - - */ - TS_WARN( "TODO: This test still needs to be written!" ); + Node x = d_nm->mkVar(); + Node y = d_nm->mkVar(); + Node z = d_nm->mkVar(); + Node m = d_nm->mkNode(AND, y, z, x); + Node n = d_nm->mkNode(OR, d_nm->mkNode(NOT, x), y, z); + Node o = d_nm->mkNode(XOR, y, x, z); + Node p = d_nm->mkNode(PLUS, z, d_nm->mkNode(UMINUS, x), z); + Node q = d_nm->mkNode(AND, x, z, d_nm->mkNode(NOT, y)); + + NodeBuilder<> b; + + // test append(TNode) + b.append(n).append(o).append(q); + + TS_ASSERT(b.getNumChildren() == 3); + TS_ASSERT(b[0] == n); + TS_ASSERT(b[1] == o); + TS_ASSERT(b[2] == q); + + vector v; + v.push_back(m); + v.push_back(p); + v.push_back(q); + // test append(vector) + b.append(v); + + TS_ASSERT(b.getNumChildren() == 6); + TS_ASSERT(b[0] == n); + TS_ASSERT(b[1] == o); + TS_ASSERT(b[2] == q); + TS_ASSERT(b[3] == m); + TS_ASSERT(b[4] == p); + TS_ASSERT(b[5] == q); + + // test append(iterator, iterator) + b.append(v.rbegin(), v.rend()); + + TS_ASSERT(b.getNumChildren() == 9); + TS_ASSERT(b[0] == n); + TS_ASSERT(b[1] == o); + TS_ASSERT(b[2] == q); + TS_ASSERT(b[3] == m); + TS_ASSERT(b[4] == p); + TS_ASSERT(b[5] == q); + TS_ASSERT(b[6] == q); + TS_ASSERT(b[7] == p); + TS_ASSERT(b[8] == m); } void testOperatorNodeCast(){ @@ -476,12 +523,10 @@ public: push_back(b,K/2); push_back(c,K/2); - a.toStream(astream); b.toStream(bstream); c.toStream(cstream); - astr = astream.str(); bstr = bstream.str(); cstr = cstream.str(); @@ -489,7 +534,7 @@ public: TS_ASSERT_EQUALS(astr, bstr); TS_ASSERT_DIFFERS(astr, cstr); - + Node n = a; n = b; n = c;// avoid warning on clear() a.clear(specKind); b.clear(specKind); c.clear(specKind); @@ -497,17 +542,14 @@ public: bstream.flush(); cstream.flush(); - push_back(a,2*K); push_back(b,2*K); push_back(c,2*K+1); - a.toStream(astream); b.toStream(bstream); c.toStream(cstream); - astr = astream.str(); bstr = bstream.str(); cstr = cstream.str(); -- 2.30.2