diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-25 07:48:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-25 07:48:03 +0000 |
commit | 826f583ee14b922f39666dc827a5624fff753724 (patch) | |
tree | 03e7f1ad98b003dae5f6406bb990a715041d239c /src/expr/node.h | |
parent | f716b67e7bedd90c4dd43617158c0f55c1811334 (diff) |
* src/expr/node.h: add a copy constructor. Apparently GCC doesn't
recognize an instantiation of the join conversion/copy ctor with
ref_count = ref_count_1 as a copy constructor. Problems with
reference counts ensue.
* src/theory/theory.h, src/theory/theory.cpp: Theory base
implementation work. Changed from continuation-style theory calls
to having an data member for the output channel. registerTerm() and
preRegisterTerm() work.
* src/theory/output_channel.h, src/theory/theory.h,
src/theory/theory.cpp, src/theory/uf/theory_uf.h,
src/theory/uf/theory_uf.cpp: merged ExplainOutputChannel into
OutputChannel.
* test/unit/expr/node_black.h: remove testPlusNode(),
testUMinusNode(), testMultNode().
* src/expr/attribute.h: new facilities ManagedAttribute<> and
CDAttribute<>, and add new template parameters to Attribute<>. Make
CDAttribute<>s work with context manager.
* src/expr/attribute.h, src/expr/node_manager.h: VarNameAttr and
TypeAttr are now "owned" (defined) by the NodeManager. The
AttributeManager knows nothing of specific attributes, it just as
all the code for dealing generically with attributes.
* test/unit/expr/node_white.h: test new attribute facilities.
* src/expr/soft_node.h: removed: We now have TNode, so SoftNode goes
away.
* src/theory/Makefile.am: fixed improper linking of theories
* src/theory/theory_engine.h: some implementation work (mainly stubs
for now, just to make sure TheoryUF can be instantiated properly,
etc.)
* src/expr/node_value.cpp, src/expr/node_value.h: move a number of
function implementations to the header and make them inline
* src/expr/node_manager.cpp, src/expr/node_manager.h: move a number of
function implementations to the header and make them inline
* src/theory/theoryof_table_prologue.h,
src/theory/theoryof_table_epilogue.h, src/theory/mktheoryof,
src/theory/Makefile.am: make the theoryOf() table from kinds and
implement TheoryEngine::theoryOf().
* src/theory/arith/Makefile, src/theory/bool/Makefile: generated these
stub Makefiles (with contrib/addsourcedir) as per policy
* src/theory/arith, src/theory/bool [directory properties]: add .deps
to svn:ignore.
* contrib/configure-in-place: permit configuring "in-place" in the
source directory.
* contrib/get-authors, contrib/dimacs_to_smt.pl,
contrib/update-copyright.pl, contrib/get-authors,
contrib/addsourcedir, src/expr/mkkind: copyright notice
* src/expr/node_manager.h, src/expr/node_builder.h,
src/prop/prop_engine.h, src/prop/prop_engine.cpp,
src/theory/theory_engine.h, src/smt/smt_engine.h, src/smt/smt_engine.cpp,
src/theory/output_channel.h: turn "const Node&"-typed formal
parameters into "TNode"
* src/theory/bool, src/theory/booleans: "bool" directory renamed "booleans"
to avoid keyword clash on containing namespace
* src/theory/booleans/theory_def.h, src/theory/uf/theory_def.h,
src/theory/arith/theory_def.h: "define" a theory simply (for automatic
theoryOf() generator).
* src/Makefile.am: build theory subdirectory before prop, smt, etc. so that
src/theory/theoryof_table.h header gets generated before it's needed
* src/expr/node_prologue.h, src/expr/node_middle.h: move "Kind" into a
separate CVC4::kind namespace to avoid its contents from cluttering
the CVC4 root namespace. Import the symbol "Kind" into the CVC4 namespace
but not the enum values.
* src/expr/node_manager.h, src/expr/node.h, src/expr/node_value.h,
src/expr/node_value.cpp, src/expr/expr.cpp, src/theory/uf/theory_uf.cpp,
src/prop/cnf_stream.cpp, src/parser/smt/smt_parser.g,
src/parser/cvc/cvc_parser.g, src/parser/antlr_parser.cpp,
test/unit/expr/node_white.h, test/unit/expr/node_black.h,
test/unit/expr/kind_black.h, test/unit/expr/node_builder_black.h:
update for having moved Kind into CVC4::kind.
* src/parser/parser.cpp: added file-does-not-exist check (was failing
silently).
Diffstat (limited to 'src/expr/node.h')
-rw-r--r-- | src/expr/node.h | 95 |
1 files changed, 70 insertions, 25 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index 03f3e9da3..19e50c5c2 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -28,6 +28,8 @@ #include "expr/type.h" #include "util/Assert.h" +#include "util/output.h" + namespace CVC4 { class Type; @@ -107,14 +109,22 @@ template<bool ref_count> NodeTemplate() : d_nv(&NodeValue::s_null) { } /** - * Copy constructor for nodes that can accept the nodes that are reference - * counted or not. + * Conversion between nodes that are reference-counted and those that are + * not. * @param node the node to make copy of */ template<bool ref_count_1> NodeTemplate(const NodeTemplate<ref_count_1>& node); /** + * Copy constructor. Note that GCC does NOT recognize an instantiation of + * the above template as a copy constructor and problems ensue. So we + * provide an explicit one here. + * @param node the node to make copy of + */ + NodeTemplate(const NodeTemplate<ref_count>& node); + + /** * Assignment operator for nodes, copies the relevant information from node * to this node. * @param node the node to copy @@ -233,9 +243,24 @@ template<bool ref_count> * @param attKind the kind of the attribute * @return the value of the attribute */ - template<class AttrKind> + template <class AttrKind> inline typename AttrKind::value_type getAttribute(const AttrKind& attKind) const; + // Note that there are two, distinct hasAttribute() declarations for + // a reason (rather than using a pointer-valued argument with a + // default value): they permit more optimized code in the underlying + // hasAttribute() implementations. + + /** + * Returns true if this node has been associated an attribute of given kind. + * Additionaly, if a pointer to the value_kind is give, and the attribute + * value has been set for this node, it will be returned. + * @param attKind the kind of the attribute + * @return true if this node has the requested attribute + */ + template <class AttrKind> + inline bool hasAttribute(const AttrKind& attKind) const; + /** * Returns true if this node has been associated an attribute of given kind. * Additionaly, if a pointer to the value_kind is give, and the attribute @@ -244,8 +269,17 @@ template<bool ref_count> * @param value where to store the value if it exists * @return true if this node has the requested attribute */ - template<class AttrKind> - inline bool hasAttribute(const AttrKind& attKind, typename AttrKind::value_type* value = NULL) const; + template <class AttrKind> + inline bool hasAttribute(const AttrKind& attKind, typename AttrKind::value_type& value) const; + + /** + * Sets the given attribute of this node to the given value. + * @param attKind the kind of the atribute + * @param value the value to set the attribute to + */ + template <class AttrKind> + inline void setAttribute(const AttrKind& attKind, + const typename AttrKind::value_type& value); /** Iterator allowing for scanning through the children. */ typedef typename NodeValue::iterator<ref_count> iterator; @@ -325,15 +359,6 @@ template<bool ref_count> NodeTemplate uMinusNode() const; NodeTemplate multNode(const NodeTemplate& right) const; - /** - * Sets the given attribute of this node to the given value. - * @param attKind the kind of the atribute - * @param value the value to set the attribute to - */ - template<class AttrKind> - inline void setAttribute(const AttrKind& attKind, - const typename AttrKind::value_type& value); - private: /** @@ -343,7 +368,6 @@ template<bool ref_count> */ void debugPrint(); - /** * Indents the given stream a given amount of spaces. * @param out the stream to indent @@ -404,7 +428,17 @@ template<bool ref_count> template<bool ref_count> template<class AttrKind> inline bool NodeTemplate<ref_count>:: - hasAttribute(const AttrKind&, typename AttrKind::value_type* ret) const { + hasAttribute(const AttrKind&) const { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->hasAttribute(*this, AttrKind()); + } + +template<bool ref_count> + template<class AttrKind> + inline bool NodeTemplate<ref_count>:: + hasAttribute(const AttrKind&, typename AttrKind::value_type& ret) const { Assert( NodeManager::currentNM() != NULL, "There is no current CVC4::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?" ); @@ -428,6 +462,7 @@ template<bool ref_count> ////TODO: Should use positive definition, i.e. what kinds are atomic. template<bool ref_count> bool NodeTemplate<ref_count>::isAtomic() const { + using namespace kind; switch(getKind()) { case NOT: case XOR: @@ -454,6 +489,8 @@ template<bool ref_count> d_nv->inc(); } +// the code for these two "conversion/copy constructors" is identical, but +// apparently we need both. see comment in the class. template<bool ref_count> template<bool ref_count_1> NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<ref_count_1>& e) { @@ -464,6 +501,14 @@ template<bool ref_count> } template<bool ref_count> + NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<ref_count>& e) { + Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!"); + d_nv = e.d_nv; + if(ref_count) + d_nv->inc(); + } + +template<bool ref_count> NodeTemplate<ref_count>::~NodeTemplate() { Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); if(ref_count) @@ -498,48 +543,48 @@ template<bool ref_count> template<bool ref_count> NodeTemplate<ref_count> NodeTemplate<ref_count>::eqNode(const NodeTemplate< ref_count>& right) const { - return NodeManager::currentNM()->mkNode(EQUAL, *this, right); + return NodeManager::currentNM()->mkNode(kind::EQUAL, *this, right); } template<bool ref_count> NodeTemplate<ref_count> NodeTemplate<ref_count>::notNode() const { - return NodeManager::currentNM()->mkNode(NOT, *this); + return NodeManager::currentNM()->mkNode(kind::NOT, *this); } template<bool ref_count> NodeTemplate<ref_count> NodeTemplate<ref_count>::andNode(const NodeTemplate< ref_count>& right) const { - return NodeManager::currentNM()->mkNode(AND, *this, right); + return NodeManager::currentNM()->mkNode(kind::AND, *this, right); } template<bool ref_count> NodeTemplate<ref_count> NodeTemplate<ref_count>::orNode(const NodeTemplate< ref_count>& right) const { - return NodeManager::currentNM()->mkNode(OR, *this, right); + return NodeManager::currentNM()->mkNode(kind::OR, *this, right); } template<bool ref_count> NodeTemplate<ref_count> NodeTemplate<ref_count>::iteNode(const NodeTemplate< ref_count>& thenpart, const NodeTemplate<ref_count>& elsepart) const { - return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart); + return NodeManager::currentNM()->mkNode(kind::ITE, *this, thenpart, elsepart); } template<bool ref_count> NodeTemplate<ref_count> NodeTemplate<ref_count>::iffNode(const NodeTemplate< ref_count>& right) const { - return NodeManager::currentNM()->mkNode(IFF, *this, right); + return NodeManager::currentNM()->mkNode(kind::IFF, *this, right); } template<bool ref_count> NodeTemplate<ref_count> NodeTemplate<ref_count>::impNode(const NodeTemplate< ref_count>& right) const { - return NodeManager::currentNM()->mkNode(IMPLIES, *this, right); + return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right); } template<bool ref_count> NodeTemplate<ref_count> NodeTemplate<ref_count>::xorNode(const NodeTemplate< ref_count>& right) const { - return NodeManager::currentNM()->mkNode(XOR, *this, right); + return NodeManager::currentNM()->mkNode(kind::XOR, *this, right); } template<bool ref_count> @@ -547,7 +592,7 @@ template<bool ref_count> indent(out, ind); out << '('; out << getKind(); - if(getKind() == VARIABLE) { + if(getKind() == kind::VARIABLE) { out << ' ' << getId(); } else if(getNumChildren() >= 1) { |