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 | |
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')
-rw-r--r-- | src/expr/node_builder.h | 123 | ||||
-rw-r--r-- | src/expr/node_value.cpp | 10 | ||||
-rw-r--r-- | src/expr/node_value.h | 8 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 1 | ||||
-rw-r--r-- | src/theory/arith/kinds | 2 | ||||
-rw-r--r-- | src/theory/theoryof_table_epilogue.h | 3 | ||||
-rw-r--r-- | src/theory/theoryof_table_middle.h | 3 | ||||
-rw-r--r-- | src/theory/theoryof_table_prologue.h | 3 |
8 files changed, 93 insertions, 60 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<true> iterator; + typedef NodeValue::iterator<true> 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<true>(); } + 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<true>(); } 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 <unsigned nchild_thresh> +inline AndNodeBuilder NodeBuilder<nchild_thresh>::operator&&(Node e) { return AndNodeBuilder(*this) && e; } -inline OrNodeBuilder NodeBuilder::operator||(Node e) { +template <unsigned nchild_thresh> +inline OrNodeBuilder NodeBuilder<nchild_thresh>::operator||(Node e) { return OrNodeBuilder(*this) || e; } -inline PlusNodeBuilder NodeBuilder::operator+ (Node e) { +template <unsigned nchild_thresh> +inline PlusNodeBuilder NodeBuilder<nchild_thresh>::operator+ (Node e) { return PlusNodeBuilder(*this) + e; } -inline PlusNodeBuilder NodeBuilder::operator- (Node e) { +template <unsigned nchild_thresh> +inline PlusNodeBuilder NodeBuilder<nchild_thresh>::operator- (Node e) { return PlusNodeBuilder(*this) - e; } -inline MultNodeBuilder NodeBuilder::operator* (Node e) { +template <unsigned nchild_thresh> +inline MultNodeBuilder NodeBuilder<nchild_thresh>::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<nchild_thresh>::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 <bool ref_count> class NodeTemplate; template <unsigned> class NodeBuilder; +class AndNodeBuilder; +class OrNodeBuilder; +class PlusNodeBuilder; +class MultNodeBuilder; class NodeManager; namespace expr { @@ -76,6 +80,10 @@ class NodeValue { template <bool> friend class CVC4::NodeTemplate; template <unsigned> 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" |