From 2b87789ee57a738cccd89dd9d2d81b065875dc29 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 2 Mar 2010 20:33:26 +0000 Subject: [PATCH] * NodeBuilder work: specifically, convenience builders. "a && b && c || d && e" (etc.) now work for Nodes a, b, c, d, e. Also refcounting fixes for NodeBuilder in certain cases * (various places) don't overload __gnu_cxx::hash<>, instead provide an explicit hash function to hash_maps and hash_sets. * add a new kind of assert, DtorAssert(), which doesn't throw exceptions (right now it operates like a usual C assert()). For use in destructors. * don't import NodeValue into CVC4 namespace (leave under CVC4::expr::). * fix some Make rule dependencies * reformat node.h as per code formatting policy * added Theory and NodeBuilder unit tests --- src/expr/Makefile.am | 2 +- src/expr/node.h | 1067 ++++++++++++++------------- src/expr/node_builder.h | 558 +++++++++----- src/expr/node_manager.h | 27 +- src/expr/node_value.cpp | 2 + src/expr/node_value.h | 29 +- src/parser/symbol_table.h | 22 +- src/prop/cnf_stream.h | 2 +- src/util/Assert.h | 6 + test/unit/expr/node_builder_black.h | 88 ++- test/unit/theory/theory_black.h | 89 +-- 11 files changed, 1084 insertions(+), 808 deletions(-) diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 1aa2e61fa..bd02cf452 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -31,7 +31,7 @@ EXTRA_DIST = \ kind_middle.h \ kind_epilogue.h -@srcdir@/kind.h: @srcdir@/mkkind kind_prologue.h kind_middle.h kind_epilogue.h @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds +@srcdir@/kind.h: mkkind kind_prologue.h kind_middle.h kind_epilogue.h builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds chmod +x @srcdir@/mkkind (@srcdir@/mkkind \ @srcdir@/kind_prologue.h \ diff --git a/src/expr/node.h b/src/expr/node.h index 5655d7e3a..e4e57fc62 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -36,8 +36,9 @@ namespace CVC4 { class Type; class NodeManager; -template - class NodeTemplate; + +template class NodeTemplate; + /** * The Node class encapsulates the NodeValue with reference counting. */ @@ -49,14 +50,14 @@ typedef NodeTemplate Node; typedef NodeTemplate TNode; namespace expr { - class NodeValue; + +class NodeValue; namespace attr { class AttributeManager; }/* CVC4::expr::attr namespace */ -}/* CVC4::expr namespace */ -using CVC4::expr::NodeValue; +}/* CVC4::expr namespace */ /** * Encapsulation of an NodeValue pointer. The reference count is @@ -64,390 +65,335 @@ using CVC4::expr::NodeValue; * @param ref_count if true reference are counted in the NodeValue */ template - class NodeTemplate { - - /** - * The NodeValue has access to the private constructors, so that the - * iterators can can create new nodes. - */ - friend class NodeValue; - - /** A convenient null-valued encapsulated pointer */ - static NodeTemplate s_null; - - /** The referenced NodeValue */ - NodeValue* d_nv; - - /** - * This constructor is reserved for use by the NodeTemplate package; one - * must construct an NodeTemplate using one of the build mechanisms of the - * NodeTemplate package. - * - * FIXME: there's a type-system escape here to cast away the const, - * since the refcount needs to be updated. But conceptually Nodes - * don't change their arguments, and it's nice to have - * const_iterators over them. - * - * This really does needs to be explicit to avoid hard to track errors with - * Nodes implicitly wrapping NodeValues - */ - explicit NodeTemplate(const NodeValue*); - - friend class NodeTemplate ; - friend class NodeTemplate ; - friend class NodeManager; - template - friend class NodeBuilder; - friend class ::CVC4::expr::attr::AttributeManager; - - /** - * 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. - * - * @param ev the expression value to assign - */ - void assignNodeValue(NodeValue* ev); - - public: - - /** Default constructor, makes a null expression. */ - NodeTemplate() : d_nv(&NodeValue::s_null) { } - - /** - * Conversion between nodes that are reference-counted and those that are - * not. - * @param node the node to make copy of - */ - NodeTemplate(const NodeTemplate& 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& node); - - /** - * Assignment operator for nodes, copies the relevant information from node - * to this node. - * @param node the node to copy - * @return reference to this node - */ - NodeTemplate& operator=(const NodeTemplate& node); - - /** - * Assignment operator for nodes, copies the relevant information from node - * to this node. - * @param node the node to copy - * @return reference to this node - */ - NodeTemplate& operator=(const NodeTemplate& node); - - /** - * Destructor. If ref_count is true it will decrement the reference count - * and, if zero, collect the NodeValue. - */ - ~NodeTemplate(); - - /** - * Return the null node. - * @return the null node - */ - static NodeTemplate null() { - return s_null; - } - - /** - * Returns true if this expression is a null expression. - * @return true if null - */ - bool isNull() const { - return d_nv == &NodeValue::s_null; - } - - /** - * Structural comparison operator for expressions. - * @param node the node to compare to - * @return true if expressions are equal, false otherwise - */ - template - bool operator==(const NodeTemplate& node) const { - return d_nv == node.d_nv; - } - - /** - * Structural comparison operator for expressions. - * @param node the node to compare to - * @return false if expressions are equal, true otherwise - */ - template - bool operator!=(const NodeTemplate& node) const { - return d_nv != node.d_nv; - } +class NodeTemplate { + + /** + * The NodeValue has access to the private constructors, so that the + * iterators can can create new nodes. + */ + friend class expr::NodeValue; + + /** A convenient null-valued encapsulated pointer */ + static NodeTemplate s_null; + + /** The referenced NodeValue */ + expr::NodeValue* d_nv; + + /** + * This constructor is reserved for use by the NodeTemplate package; one + * must construct an NodeTemplate using one of the build mechanisms of the + * NodeTemplate package. + * + * FIXME: there's a type-system escape here to cast away the const, + * since the refcount needs to be updated. But conceptually Nodes + * don't change their arguments, and it's nice to have + * const_iterators over them. + * + * This really does needs to be explicit to avoid hard to track errors with + * Nodes implicitly wrapping NodeValues + */ + explicit NodeTemplate(const expr::NodeValue*); + + friend class NodeTemplate ; + friend class NodeTemplate ; + friend class NodeManager; + + template + friend class NodeBuilder; + + friend class ::CVC4::expr::attr::AttributeManager; + + /** + * 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. + * + * @param ev the expression value to assign + */ + void assignNodeValue(expr::NodeValue* ev); + +public: + + /** Default constructor, makes a null expression. */ + NodeTemplate() : d_nv(&expr::NodeValue::s_null) { } + + /** + * Conversion between nodes that are reference-counted and those that are + * not. + * @param node the node to make copy of + */ + NodeTemplate(const NodeTemplate& 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& node); + + /** + * Assignment operator for nodes, copies the relevant information from node + * to this node. + * @param node the node to copy + * @return reference to this node + */ + NodeTemplate& operator=(const NodeTemplate& node); + + /** + * Assignment operator for nodes, copies the relevant information from node + * to this node. + * @param node the node to copy + * @return reference to this node + */ + NodeTemplate& operator=(const NodeTemplate& node); + + /** + * Destructor. If ref_count is true it will decrement the reference count + * and, if zero, collect the NodeValue. + */ + ~NodeTemplate() throw(); + + /** + * Return the null node. + * @return the null node + */ + static NodeTemplate null() { + return s_null; + } - /** - * We compare by expression ids so, keeping things deterministic and having - * that subexpressions have to be smaller than the enclosing expressions. - * @param node the node to compare to - * @return true if this expression is smaller - */ - template - inline bool operator<(const NodeTemplate& node) const { - return d_nv->d_id < node.d_nv->d_id; - } + /** + * Returns true if this expression is a null expression. + * @return true if null + */ + bool isNull() const { + return d_nv == &expr::NodeValue::s_null; + } - /** - * Returns the i-th child of this node. - * @param i the index of the child - * @return the node representing the i-th child - */ - NodeTemplate operator[](int i) const { - Assert(i >= 0 && unsigned(i) < d_nv->d_nchildren); - return NodeTemplate(d_nv->d_children[i]); - } + /** + * Structural comparison operator for expressions. + * @param node the node to compare to + * @return true if expressions are equal, false otherwise + */ + template + bool operator==(const NodeTemplate& node) const { + return d_nv == node.d_nv; + } - /** - * Returns true if this node is atomic (has no more Boolean structure) - * @return true if atomic - */ - bool isAtomic() const; - - /** - * Returns the hash value of this node. - * @return the hash value - */ - size_t hash() const { - return d_nv->getId(); - } + /** + * Structural comparison operator for expressions. + * @param node the node to compare to + * @return false if expressions are equal, true otherwise + */ + template + bool operator!=(const NodeTemplate& node) const { + return d_nv != node.d_nv; + } - /** - * Returns the unique id of this node - * @return the ud - */ - uint64_t getId() const { - return d_nv->getId(); - } + /** + * We compare by expression ids so, keeping things deterministic and having + * that subexpressions have to be smaller than the enclosing expressions. + * @param node the node to compare to + * @return true if this expression is smaller + */ + template + inline bool operator<(const NodeTemplate& node) const { + return d_nv->d_id < node.d_nv->d_id; + } - /** - * Returns a node representing the operator of this expression. - * If this is an APPLY, then the operator will be a functional term. - * Otherwise, it will be a node with kind BUILTIN - */ - inline NodeTemplate getOperator() const { - switch(getKind()) { - case kind::APPLY: - /* The operator is the first child. */ - return NodeTemplate (d_nv->d_children[0]); - - case kind::EQUAL: - case kind::ITE: - case kind::TUPLE: - case kind::NOT: - case kind::AND: - case kind::IFF: - case kind::IMPLIES: - case kind::OR: - case kind::XOR: - case kind::PLUS: - /* Should return a BUILTIN node. */ - Unimplemented("getOperator() on non-APPLY kind: " + getKind()); - break; - - case kind::FALSE: - case kind::TRUE: - case kind::SKOLEM: - case kind::VARIABLE: - IllegalArgument(*this,"getOperator() called on kind with no operator"); - break; - - default: - Unhandled(getKind()); - } - - NodeTemplate n; // NULL Node for default return - return n; - } + /** + * Returns the i-th child of this node. + * @param i the index of the child + * @return the node representing the i-th child + */ + NodeTemplate operator[](int i) const { + Assert(i >= 0 && unsigned(i) < d_nv->d_nchildren); + return NodeTemplate(d_nv->d_children[i]); + } - /** Returns true if the node has an operator (i.e., it's not a variable or a constant). */ - inline bool hasOperator() const { - switch(getKind()) { - case kind::APPLY: - case kind::EQUAL: - case kind::ITE: - case kind::TUPLE: - case kind::FALSE: - case kind::TRUE: - case kind::NOT: - case kind::AND: - case kind::IFF: - case kind::IMPLIES: - case kind::OR: - case kind::XOR: - case kind::PLUS: - return true; - - case kind::SKOLEM: - case kind::VARIABLE: - return false; - - default: - Unhandled(getKind()); - } + /** + * Returns true if this node is atomic (has no more Boolean structure) + * @return true if atomic + */ + bool isAtomic() const; + + /** + * Returns the hash value of this node. + * @return the hash value + */ + size_t hash() const { + return d_nv->getId(); + } - } + /** + * Returns the unique id of this node + * @return the ud + */ + uint64_t getId() const { + return d_nv->getId(); + } - /** - * Returns the type of this node. - * @return the type - */ - const Type* getType() const; - - /** - * Returns the kind of this node. - * @return the kind - */ - inline Kind getKind() const { - return Kind(d_nv->d_kind); - } + /** + * Returns a node representing the operator of this expression. + * If this is an APPLY, then the operator will be a functional term. + * Otherwise, it will be a node with kind BUILTIN + */ + NodeTemplate getOperator() const; + + /** Returns true if the node has an operator (i.e., it's not a variable or a constant). */ + bool hasOperator() const; + + /** + * Returns the type of this node. + * @return the type + */ + const Type* getType() const; + + /** + * Returns the kind of this node. + * @return the kind + */ + inline Kind getKind() const { + return Kind(d_nv->d_kind); + } - /** - * Returns the number of children this node has. - * @return the number of children - */ - inline size_t getNumChildren() const; - - /** - * Returns the value of the given attribute that this has been attached. - * @param attKind the kind of the attribute - * @return the value of the attribute - */ - template - 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 - 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 - * value has been set for this node, it will be returned. - * @param attKind the kind of the attribute - * @param value where to store the value if it exists - * @return true if this node has the requested attribute - */ - template - 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 - inline void setAttribute(const AttrKind& attKind, - const typename AttrKind::value_type& value); - - /** Iterator allowing for scanning through the children. */ - typedef typename NodeValue::iterator iterator; - /** Constant iterator allowing for scanning through the children. */ - typedef typename NodeValue::iterator const_iterator; - - /** - * Returns the iterator pointing to the first child. - * @return the iterator - */ - inline iterator begin() { - return d_nv->begin(); - } + /** + * Returns the number of children this node has. + * @return the number of children + */ + inline size_t getNumChildren() const; + + /** + * Returns the value of the given attribute that this has been attached. + * @param attKind the kind of the attribute + * @return the value of the attribute + */ + template + 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 + 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 + * value has been set for this node, it will be returned. + * @param attKind the kind of the attribute + * @param value where to store the value if it exists + * @return true if this node has the requested attribute + */ + template + 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 + inline void setAttribute(const AttrKind& attKind, + const typename AttrKind::value_type& value); + + /** Iterator allowing for scanning through the children. */ + typedef typename expr::NodeValue::iterator iterator; + /** Constant iterator allowing for scanning through the children. */ + typedef typename expr::NodeValue::iterator const_iterator; + + /** + * Returns the iterator pointing to the first child. + * @return the iterator + */ + inline iterator begin() { + return d_nv->begin(); + } - /** - * Returns the iterator pointing to the end of the children (one beyond the - * last one. - * @return the end of the children iterator. - */ - inline iterator end() { - return d_nv->end(); - } + /** + * Returns the iterator pointing to the end of the children (one beyond the + * last one. + * @return the end of the children iterator. + */ + inline iterator end() { + return d_nv->end(); + } - /** - * Returns the const_iterator pointing to the first child. - * @return the const_iterator - */ - inline const_iterator begin() const { - return d_nv->begin(); - } + /** + * Returns the const_iterator pointing to the first child. + * @return the const_iterator + */ + inline const_iterator begin() const { + return d_nv->begin(); + } - /** - * Returns the const_iterator pointing to the end of the children (one - * beyond the last one. - * @return the end of the children const_iterator. - */ - inline const_iterator end() const { - return d_nv->end(); - } + /** + * Returns the const_iterator pointing to the end of the children (one + * beyond the last one. + * @return the end of the children const_iterator. + */ + inline const_iterator end() const { + return d_nv->end(); + } - /** - * Converts this node into a string representation. - * @return the string representation of this node. - */ - inline std::string toString() const { - return d_nv->toString(); - } + /** + * Converts this node into a string representation. + * @return the string representation of this node. + */ + inline std::string toString() const { + return d_nv->toString(); + } - /** - * Converst this node into a string representation and sends it to the - * given stream - * @param out the sream to serialise this node to - */ - inline void toStream(std::ostream& out) const { - d_nv->toStream(out); - } + /** + * Converst this node into a string representation and sends it to the + * given stream + * @param out the sream to serialise this node to + */ + inline void toStream(std::ostream& out) const { + d_nv->toStream(out); + } - /** - * Very basic pretty printer for Node. - * @param o output stream to print to. - * @param indent number of spaces to indent the formula by. - */ - void printAst(std::ostream & o, int indent = 0) const; - - NodeTemplate eqNode(const NodeTemplate& right) const; - - NodeTemplate notNode() const; - NodeTemplate andNode(const NodeTemplate& right) const; - NodeTemplate orNode(const NodeTemplate& right) const; - NodeTemplate iteNode(const NodeTemplate& thenpart, - const NodeTemplate& elsepart) const; - NodeTemplate iffNode(const NodeTemplate& right) const; - NodeTemplate impNode(const NodeTemplate& right) const; - NodeTemplate xorNode(const NodeTemplate& right) const; - - private: - - /** - * Indents the given stream a given amount of spaces. - * @param out the stream to indent - * @param indent the numer of spaces - */ - static void indent(std::ostream& out, int indent) { - for(int i = 0; i < indent; i++) - out << ' '; - } + /** + * Very basic pretty printer for Node. + * @param o output stream to print to. + * @param indent number of spaces to indent the formula by. + */ + void printAst(std::ostream & o, int indent = 0) const; + + NodeTemplate eqNode(const NodeTemplate& right) const; + + NodeTemplate notNode() const; + NodeTemplate andNode(const NodeTemplate& right) const; + NodeTemplate orNode(const NodeTemplate& right) const; + NodeTemplate iteNode(const NodeTemplate& thenpart, + const NodeTemplate& elsepart) const; + NodeTemplate iffNode(const NodeTemplate& right) const; + NodeTemplate impNode(const NodeTemplate& right) const; + NodeTemplate xorNode(const NodeTemplate& right) const; + +private: + + /** + * Indents the given stream a given amount of spaces. + * @param out the stream to indent + * @param indent the numer of spaces + */ + static void indent(std::ostream& out, int indent) { + for(int i = 0; i < indent; i++) + out << ' '; + } - };/* class NodeTemplate */ +};/* class NodeTemplate */ /** * Serializes a given node to the given stream. @@ -464,239 +410,313 @@ inline std::ostream& operator<<(std::ostream& out, const Node& node) { #include -// for hashtables -namespace __gnu_cxx { -template<> - struct hash { - size_t operator()(const CVC4::Node& node) const { - return (size_t) node.hash(); - } - }; -}/* __gnu_cxx namespace */ - #include "expr/attribute.h" #include "expr/node_manager.h" namespace CVC4 { -template - inline size_t NodeTemplate::getNumChildren() const { - return d_nv->d_nchildren; +// for hash_maps, hash_sets.. +struct NodeHashFcn { + size_t operator()(const CVC4::Node& node) const { + return (size_t) node.hash(); } +}; template - template - inline typename AttrKind::value_type NodeTemplate:: - getAttribute(const AttrKind&) const { - Assert( NodeManager::currentNM() != NULL, +inline size_t NodeTemplate::getNumChildren() const { + return d_nv->d_nchildren; +} + +template +template +inline typename AttrKind::value_type NodeTemplate:: +getAttribute(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()->getAttribute(*this, AttrKind()); - } + return NodeManager::currentNM()->getAttribute(*this, AttrKind()); +} template - template - inline bool NodeTemplate:: - hasAttribute(const AttrKind&) const { - Assert( NodeManager::currentNM() != NULL, +template +inline bool NodeTemplate:: +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()); - } + return NodeManager::currentNM()->hasAttribute(*this, AttrKind()); +} template - template - inline bool NodeTemplate:: - hasAttribute(const AttrKind&, typename AttrKind::value_type& ret) const { - Assert( NodeManager::currentNM() != NULL, +template +inline bool NodeTemplate:: +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 ?" ); - return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret); - } + return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret); +} template - template - inline void NodeTemplate:: - setAttribute(const AttrKind&, const typename AttrKind::value_type& value) { - Assert( NodeManager::currentNM() != NULL, +template +inline void NodeTemplate:: +setAttribute(const AttrKind&, const typename AttrKind::value_type& value) { + Assert( NodeManager::currentNM() != NULL, "There is no current CVC4::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?" ); - NodeManager::currentNM()->setAttribute(*this, AttrKind(), value); - } + NodeManager::currentNM()->setAttribute(*this, AttrKind(), value); +} template - NodeTemplate NodeTemplate::s_null(&NodeValue::s_null); +NodeTemplate NodeTemplate::s_null(&expr::NodeValue::s_null); ////FIXME: This function is a major hack! Should be changed ASAP ////TODO: Should use positive definition, i.e. what kinds are atomic. template - bool NodeTemplate::isAtomic() const { - using namespace kind; - switch(getKind()) { - case NOT: - case XOR: - case ITE: - case IFF: - case IMPLIES: - case OR: - case AND: - return false; - default: - return true; - } +bool NodeTemplate::isAtomic() const { + using namespace kind; + switch(getKind()) { + case NOT: + case XOR: + case ITE: + case IFF: + case IMPLIES: + case OR: + case AND: + return false; + default: + return true; } +} // FIXME: escape from type system convenient but is there a better // way? Nodes conceptually don't change their expr values but of // course they do modify the refcount. But it's nice to be able to // support node_iterators over const NodeValue*. So.... hm. template - NodeTemplate::NodeTemplate(const NodeValue* ev) : - d_nv(const_cast (ev)) { - Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); - if(ref_count) - d_nv->inc(); +NodeTemplate::NodeTemplate(const expr::NodeValue* ev) : + d_nv(const_cast (ev)) { + Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); + if(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 - NodeTemplate::NodeTemplate(const NodeTemplate& e) { - Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!"); - d_nv = e.d_nv; - if(ref_count) - d_nv->inc(); +NodeTemplate::NodeTemplate(const NodeTemplate& e) { + Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!"); + d_nv = e.d_nv; + if(ref_count) { + d_nv->inc(); } +} template - NodeTemplate::NodeTemplate(const NodeTemplate& e) { - Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!"); - d_nv = e.d_nv; - if(ref_count) - d_nv->inc(); +NodeTemplate::NodeTemplate(const NodeTemplate& e) { + Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!"); + d_nv = e.d_nv; + if(ref_count) { + d_nv->inc(); } +} template - NodeTemplate::~NodeTemplate() { - Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); - if(ref_count) - d_nv->dec(); - Assert(ref_count || d_nv->d_rc > 0, - "Temporary node pointing to an expired node"); +NodeTemplate::~NodeTemplate() throw() { + DtorAssert(d_nv != NULL, "Expecting a non-NULL expression value!"); + if(ref_count) { + d_nv->dec(); } + DtorAssert(ref_count || d_nv->d_rc > 0, + "Temporary node pointing to an expired node"); +} template - void NodeTemplate::assignNodeValue(NodeValue* ev) { - d_nv = ev; - if(ref_count) - d_nv->inc(); +void NodeTemplate::assignNodeValue(expr::NodeValue* ev) { + d_nv = ev; + if(ref_count) { + d_nv->inc(); } +} template - NodeTemplate& NodeTemplate:: - operator=(const NodeTemplate& e) { - Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); - Assert(e.d_nv != NULL, "Expecting a non-NULL expression value on RHS!"); - if(EXPECT_TRUE( d_nv != e.d_nv )) { - if(ref_count) - d_nv->dec(); - d_nv = e.d_nv; - if(ref_count) - d_nv->inc(); +NodeTemplate& NodeTemplate:: +operator=(const NodeTemplate& e) { + Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); + Assert(e.d_nv != NULL, "Expecting a non-NULL expression value on RHS!"); + if(EXPECT_TRUE( d_nv != e.d_nv )) { + if(ref_count) { + d_nv->dec(); + } + d_nv = e.d_nv; + if(ref_count) { + d_nv->inc(); } - return *this; } + return *this; +} template - NodeTemplate& NodeTemplate:: - operator=(const NodeTemplate& e) { - Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); - Assert(e.d_nv != NULL, "Expecting a non-NULL expression value on RHS!"); - if(EXPECT_TRUE( d_nv != e.d_nv )) { - if(ref_count) - d_nv->dec(); - d_nv = e.d_nv; - if(ref_count) - d_nv->inc(); +NodeTemplate& NodeTemplate:: +operator=(const NodeTemplate& e) { + Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); + Assert(e.d_nv != NULL, "Expecting a non-NULL expression value on RHS!"); + if(EXPECT_TRUE( d_nv != e.d_nv )) { + if(ref_count) { + d_nv->dec(); + } + d_nv = e.d_nv; + if(ref_count) { + d_nv->inc(); } - return *this; } + return *this; +} template - NodeTemplate NodeTemplate::eqNode(const NodeTemplate< - ref_count>& right) const { - return NodeManager::currentNM()->mkNode(kind::EQUAL, *this, right); - } +NodeTemplate NodeTemplate::eqNode(const NodeTemplate< + ref_count>& right) const { + return NodeManager::currentNM()->mkNode(kind::EQUAL, *this, right); +} template - NodeTemplate NodeTemplate::notNode() const { - return NodeManager::currentNM()->mkNode(kind::NOT, *this); - } +NodeTemplate NodeTemplate::notNode() const { + return NodeManager::currentNM()->mkNode(kind::NOT, *this); +} template - NodeTemplate NodeTemplate::andNode(const NodeTemplate< - ref_count>& right) const { - return NodeManager::currentNM()->mkNode(kind::AND, *this, right); - } +NodeTemplate NodeTemplate::andNode(const NodeTemplate< + ref_count>& right) const { + return NodeManager::currentNM()->mkNode(kind::AND, *this, right); +} template - NodeTemplate NodeTemplate::orNode(const NodeTemplate< - ref_count>& right) const { - return NodeManager::currentNM()->mkNode(kind::OR, *this, right); - } +NodeTemplate NodeTemplate::orNode(const NodeTemplate< + ref_count>& right) const { + return NodeManager::currentNM()->mkNode(kind::OR, *this, right); +} template - NodeTemplate NodeTemplate::iteNode(const NodeTemplate< - ref_count>& thenpart, const NodeTemplate& elsepart) const { - return NodeManager::currentNM()->mkNode(kind::ITE, *this, thenpart, elsepart); - } +NodeTemplate NodeTemplate::iteNode(const NodeTemplate< + ref_count>& thenpart, const NodeTemplate& elsepart) const { + return NodeManager::currentNM()->mkNode(kind::ITE, *this, thenpart, elsepart); +} template - NodeTemplate NodeTemplate::iffNode(const NodeTemplate< - ref_count>& right) const { - return NodeManager::currentNM()->mkNode(kind::IFF, *this, right); - } +NodeTemplate NodeTemplate::iffNode(const NodeTemplate< + ref_count>& right) const { + return NodeManager::currentNM()->mkNode(kind::IFF, *this, right); +} template - NodeTemplate NodeTemplate::impNode(const NodeTemplate< - ref_count>& right) const { - return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right); - } +NodeTemplate NodeTemplate::impNode(const NodeTemplate< + ref_count>& right) const { + return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right); +} template - NodeTemplate NodeTemplate::xorNode(const NodeTemplate< - ref_count>& right) const { - return NodeManager::currentNM()->mkNode(kind::XOR, *this, right); - } +NodeTemplate NodeTemplate::xorNode(const NodeTemplate< + ref_count>& right) const { + return NodeManager::currentNM()->mkNode(kind::XOR, *this, right); +} template - void NodeTemplate::printAst(std::ostream& out, int ind) const { - indent(out, ind); - out << '('; - out << getKind(); - if(getKind() == kind::VARIABLE) { - out << ' ' << getId(); - - } else if(getNumChildren() >= 1) { - for(const_iterator child = begin(); child != end(); ++child) { - out << std::endl; - NodeTemplate((*child)).printAst(out, ind + 1); - } +void NodeTemplate::printAst(std::ostream& out, int ind) const { + indent(out, ind); + out << '('; + out << getKind(); + if(getKind() == kind::VARIABLE) { + out << ' ' << getId(); + + } else if(getNumChildren() >= 1) { + for(const_iterator child = begin(); child != end(); ++child) { out << std::endl; - indent(out, ind); + NodeTemplate((*child)).printAst(out, ind + 1); } - out << ')'; + out << std::endl; + indent(out, ind); } + out << ')'; +} -template - const Type* NodeTemplate::getType() 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()->getType(*this); +/** + * Returns a node representing the operator of this expression. + * If this is an APPLY, then the operator will be a functional term. + * Otherwise, it will be a node with kind BUILTIN + */ +template +NodeTemplate NodeTemplate::getOperator() const { + switch(Kind k = getKind()) { + case kind::APPLY: + /* The operator is the first child. */ + return NodeTemplate(d_nv->d_children[0]); + + case kind::EQUAL: + case kind::ITE: + case kind::TUPLE: + case kind::NOT: + case kind::AND: + case kind::IFF: + case kind::IMPLIES: + case kind::OR: + case kind::XOR: + case kind::PLUS: { + /* Returns a BUILTIN node. */ + /* TODO: construct a singleton at load-time? */ + /* TODO: maybe keep a table like the TheoryOfTable ? */ + NodeTemplate n = NodeManager::currentNM()->mkNode(k); + return NodeManager::currentNM()->mkNode(kind::BUILTIN, n); } + case kind::FALSE: + case kind::TRUE: + case kind::SKOLEM: + case kind::VARIABLE: + IllegalArgument(*this, "getOperator() called on kind with no operator"); + + default: + Unhandled(getKind()); + } +} + +/** + * Returns true if the node has an operator (i.e., it's not a variable or a constant). + */ +template +bool NodeTemplate::hasOperator() const { + switch(getKind()) { + case kind::APPLY: + case kind::EQUAL: + case kind::ITE: + case kind::TUPLE: + case kind::FALSE: + case kind::TRUE: + case kind::NOT: + case kind::AND: + case kind::IFF: + case kind::IMPLIES: + case kind::OR: + case kind::XOR: + case kind::PLUS: + return true; + + case kind::SKOLEM: + case kind::VARIABLE: + return false; + + default: + Unhandled(getKind()); + } +} +template +const Type* NodeTemplate::getType() 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()->getType(*this); +} /** * Pretty printer for use within gdb. This is not intended to be used @@ -721,7 +741,6 @@ static void __attribute__((used)) debugPrintTNode(const NodeTemplate& n) Warning().flush(); } - }/* CVC4 namespace */ #endif /* __CVC4__NODE_H */ diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index f5da56d96..4dc3c06d0 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -63,20 +63,20 @@ class NodeBuilder { // extract another bool d_used; - NodeValue *d_nv; - NodeValue d_inlineNv; - NodeValue *d_childrenStorage[nchild_thresh]; + expr::NodeValue *d_nv; + expr::NodeValue d_inlineNv; + expr::NodeValue *d_childrenStorage[nchild_thresh]; - bool nvIsAllocated() { + bool nvIsAllocated() const { return d_nv->d_nchildren > nchild_thresh; } template - bool nvIsAllocated(const NodeBuilder& nb) { + bool nvIsAllocated(const NodeBuilder& nb) const { return nb.d_nv->d_nchildren > N; } - bool evNeedsToBeAllocated() { + bool evNeedsToBeAllocated() const { return d_nv->d_nchildren == d_size; } @@ -93,17 +93,31 @@ class NodeBuilder { } // dealloc: only call this with d_used == false and nvIsAllocated() - inline void dealloc(); + inline void dealloc() throw(); void crop() { - Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); + Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); if(EXPECT_FALSE( nvIsAllocated() ) && EXPECT_TRUE( d_size > d_nv->d_nchildren )) { - d_nv = (NodeValue*) - std::realloc(d_nv, sizeof(NodeValue) + - ( sizeof(NodeValue*) * (d_size = d_nv->d_nchildren) )); + d_nv = (expr::NodeValue*) + std::realloc(d_nv, sizeof(expr::NodeValue) + + ( sizeof(expr::NodeValue*) * (d_size = d_nv->d_nchildren) )); } } + NodeBuilder& collapseTo(Kind k) { + Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); + AssertArgument(k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR, + k, "illegal collapsing kind"); + + if(getKind() != k) { + Node n = *this; + clear(); + d_nv->d_kind = k; + append(n); + } + return *this; + } + public: inline NodeBuilder(); @@ -112,67 +126,48 @@ public: template inline NodeBuilder(const NodeBuilder& nb); inline NodeBuilder(NodeManager* nm); inline NodeBuilder(NodeManager* nm, Kind k); - inline ~NodeBuilder(); + inline ~NodeBuilder() throw(); - typedef NodeValue::iterator iterator; - typedef NodeValue::iterator const_iterator; + typedef expr::NodeValue::iterator iterator; + typedef expr::NodeValue::iterator const_iterator; const_iterator begin() const { - Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); + Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); return d_nv->begin(); } const_iterator end() const { - Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); + Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); return d_nv->end(); } Kind getKind() const { - Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); + Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); return d_nv->getKind(); } unsigned getNumChildren() const { - Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); + Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); return d_nv->getNumChildren(); } Node operator[](int i) const { - Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); + Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); Assert(i >= 0 && i < d_nv->getNumChildren()); return Node(d_nv->d_children[i]); } + /** + * "Reset" this node builder (optionally setting a new kind for it), + * using the same memory as before. This should leave the + * NodeBuilder<> in the state it was after initial construction. + */ void clear(Kind k = kind::UNDEFINED_KIND); - // Compound expression constructors - /* - NodeBuilder& eqExpr(TNode right); - NodeBuilder& notExpr(); - NodeBuilder& andExpr(TNode right); - NodeBuilder& orExpr(TNode right); - NodeBuilder& iteExpr(TNode thenpart, TNode elsepart); - NodeBuilder& iffExpr(TNode right); - NodeBuilder& impExpr(TNode right); - NodeBuilder& xorExpr(TNode right); - */ - - /* TODO design: these modify NodeBuilder ?? */ - /* - NodeBuilder& operator!() { return notExpr(); } - NodeBuilder& operator&&(TNode right) { return andExpr(right); } - NodeBuilder& operator||(TNode right) { return orExpr(right); } - */ - - /* - NodeBuilder& operator&&=(TNode right) { return andExpr(right); } - NodeBuilder& operator||=(TNode right) { return orExpr(right); } - */ - // "Stream" expression constructor syntax NodeBuilder& operator<<(const Kind& k) { - Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); + Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); Assert(d_nv->getKind() == kind::UNDEFINED_KIND); d_nv->d_kind = k; return *this; @@ -180,21 +175,21 @@ public: NodeBuilder& operator<<(TNode n) { // FIXME: collapse if ! UNDEFINED_KIND - Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); + Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); return append(n); } // For pushing sequences of children NodeBuilder& append(const std::vector& children) { - Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); + Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); return append(children.begin(), children.end()); } NodeBuilder& append(TNode n) { - Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); + Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); Debug("prop") << "append: " << this << " " << n << "[" << n.d_nv << "]" << std::endl; allocateEvIfNecessaryForAppend(); - NodeValue* ev = n.d_nv; + expr::NodeValue* ev = n.d_nv; ev->inc(); d_nv->d_children[d_nv->d_nchildren++] = ev; return *this; @@ -202,209 +197,309 @@ public: template NodeBuilder& append(const Iterator& begin, const Iterator& end) { - Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); + Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); for(Iterator i = begin; i != end; ++i) { append(*i); } return *this; } - // not const operator Node(); + operator Node() const; inline void toStream(std::ostream& out) const { - Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); + Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); d_nv->toStream(out); } - AndNodeBuilder operator&&(Node); - OrNodeBuilder operator||(Node); - PlusNodeBuilder operator+ (Node); - PlusNodeBuilder operator- (Node); - MultNodeBuilder operator* (Node); + NodeBuilder& operator&=(TNode); + NodeBuilder& operator|=(TNode); + NodeBuilder& operator+=(TNode); + NodeBuilder& operator-=(TNode); + NodeBuilder& operator*=(TNode); friend class AndNodeBuilder; 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 template friend class NodeBuilder; };/* class NodeBuilder */ +// TODO: add templatized NodeTemplate to all above and +// below inlines for 'const [T]Node&' arguments? Technically a lot of +// time is spent in the TNode conversion and copy constructor, but +// this should be optimized into a simple pointer copy (?) +// TODO: double-check this. + class AndNodeBuilder { +public: NodeBuilder<> d_eb; -public: + inline AndNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { + d_eb.collapseTo(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); - } + inline AndNodeBuilder(TNode a, TNode b) : d_eb(kind::AND) { + d_eb << a << b; } - AndNodeBuilder& operator&&(Node); - OrNodeBuilder operator||(Node); + template + inline AndNodeBuilder& operator&&(const NodeTemplate&); - operator NodeBuilder<>() { return d_eb; } + template + inline OrNodeBuilder operator||(const NodeTemplate&); + + inline operator NodeBuilder<>() { return d_eb; } + inline operator Node() { return d_eb; } };/* class AndNodeBuilder */ class OrNodeBuilder { +public: NodeBuilder<> d_eb; -public: + inline OrNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { + d_eb.collapseTo(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); - } + inline OrNodeBuilder(TNode a, TNode b) : d_eb(kind::OR) { + d_eb << a << b; } - AndNodeBuilder operator&&(Node); - OrNodeBuilder& operator||(Node); + template + inline AndNodeBuilder operator&&(const NodeTemplate&); + + template + inline OrNodeBuilder& operator||(const NodeTemplate&); - operator NodeBuilder<>() { return d_eb; } + inline operator NodeBuilder<>() { return d_eb; } + inline operator Node() { return d_eb; } };/* class OrNodeBuilder */ class PlusNodeBuilder { +public: NodeBuilder<> d_eb; -public: + inline PlusNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { + d_eb.collapseTo(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); - } + inline PlusNodeBuilder(TNode a, TNode b) : d_eb(kind::PLUS) { + d_eb << a << b; } - PlusNodeBuilder& operator+(Node); - PlusNodeBuilder& operator-(Node); - MultNodeBuilder operator*(Node); + template + inline PlusNodeBuilder& operator+(const NodeTemplate&); + + template + inline PlusNodeBuilder& operator-(const NodeTemplate&); + + template + inline MultNodeBuilder operator*(const NodeTemplate&); - operator NodeBuilder<>() { return d_eb; } + inline operator NodeBuilder<>() { return d_eb; } + inline operator Node() { return d_eb; } };/* class PlusNodeBuilder */ class MultNodeBuilder { +public: NodeBuilder<> d_eb; -public: + inline MultNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { + d_eb.collapseTo(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); - } + inline MultNodeBuilder(TNode a, TNode b) : d_eb(kind::MULT) { + d_eb << a << b; } - PlusNodeBuilder operator+(Node); - PlusNodeBuilder operator-(Node); - MultNodeBuilder& operator*(Node); + template + inline PlusNodeBuilder operator+(const NodeTemplate&); - operator NodeBuilder<>() { return d_eb; } + template + inline PlusNodeBuilder operator-(const NodeTemplate&); + + template + inline MultNodeBuilder& operator*(const NodeTemplate&); + + inline operator NodeBuilder<>() { return d_eb; } + inline operator Node() { return d_eb; } };/* class MultNodeBuilder */ template -inline AndNodeBuilder NodeBuilder::operator&&(Node e) { - return AndNodeBuilder(*this) && e; +inline NodeBuilder& NodeBuilder::operator&=(TNode e) { + return collapseTo(kind::AND).append(e); } template -inline OrNodeBuilder NodeBuilder::operator||(Node e) { - return OrNodeBuilder(*this) || e; +inline NodeBuilder& NodeBuilder::operator|=(TNode e) { + return collapseTo(kind::OR).append(e); } template -inline PlusNodeBuilder NodeBuilder::operator+ (Node e) { - return PlusNodeBuilder(*this) + e; +inline NodeBuilder& NodeBuilder::operator+=(TNode e) { + return collapseTo(kind::PLUS).append(e); } template -inline PlusNodeBuilder NodeBuilder::operator- (Node e) { - return PlusNodeBuilder(*this) - e; +inline NodeBuilder& NodeBuilder::operator-=(TNode e) { + return collapseTo(kind::PLUS).append(NodeManager::currentNM()->mkNode(kind::UMINUS, e)); } template -inline MultNodeBuilder NodeBuilder::operator* (Node e) { - return MultNodeBuilder(*this) * e; +inline NodeBuilder& NodeBuilder::operator*=(TNode e) { + return collapseTo(kind::MULT).append(e); } -inline AndNodeBuilder& AndNodeBuilder::operator&&(Node e) { - d_eb.append(e); +template +inline AndNodeBuilder& AndNodeBuilder::operator&&(const NodeTemplate& n) { + d_eb.append(n); return *this; } -inline OrNodeBuilder AndNodeBuilder::operator||(Node e) { - Node n = d_eb; - d_eb.clear(); - d_eb.append(n); - return OrNodeBuilder(d_eb) || e; +template +inline OrNodeBuilder AndNodeBuilder::operator||(const NodeTemplate& n) { + return OrNodeBuilder(Node(d_eb), n); } -inline AndNodeBuilder OrNodeBuilder::operator&&(Node e) { - Node n = d_eb; - d_eb.clear(); +inline AndNodeBuilder& operator&&(AndNodeBuilder& a, const AndNodeBuilder& b) { + return a && Node(b.d_eb); +} +inline AndNodeBuilder& operator&&(AndNodeBuilder& a, const OrNodeBuilder& b) { + return a && Node(b.d_eb); +} +inline OrNodeBuilder operator||(AndNodeBuilder& a, const AndNodeBuilder& b) { + return a || Node(b.d_eb); +} +inline OrNodeBuilder operator||(AndNodeBuilder& a, const OrNodeBuilder& b) { + return a || Node(b.d_eb); +} + +template +inline AndNodeBuilder OrNodeBuilder::operator&&(const NodeTemplate& n) { + return AndNodeBuilder(Node(d_eb), n); +} + +template +inline OrNodeBuilder& OrNodeBuilder::operator||(const NodeTemplate& n) { d_eb.append(n); - return AndNodeBuilder(d_eb) && e; + return *this; } -inline OrNodeBuilder& OrNodeBuilder::operator||(Node e) { - d_eb.append(e); +inline AndNodeBuilder operator&&(OrNodeBuilder& a, const AndNodeBuilder& b) { + return a && Node(b.d_eb); +} +inline AndNodeBuilder operator&&(OrNodeBuilder& a, const OrNodeBuilder& b) { + return a && Node(b.d_eb); +} +inline OrNodeBuilder& operator||(OrNodeBuilder& a, const AndNodeBuilder& b) { + return a || Node(b.d_eb); +} +inline OrNodeBuilder& operator||(OrNodeBuilder& a, const OrNodeBuilder& b) { + return a || Node(b.d_eb); +} + +template +inline PlusNodeBuilder& PlusNodeBuilder::operator+(const NodeTemplate& n) { + d_eb.append(n); return *this; } -inline PlusNodeBuilder& PlusNodeBuilder::operator+(Node e) { - d_eb.append(e); +template +inline PlusNodeBuilder& PlusNodeBuilder::operator-(const NodeTemplate& n) { + d_eb.append(NodeManager::currentNM()->mkNode(kind::UMINUS, n)); return *this; } +template +inline MultNodeBuilder PlusNodeBuilder::operator*(const NodeTemplate& n) { + return MultNodeBuilder(Node(d_eb), n); +} + /* -inline PlusNodeBuilder& PlusNodeBuilder::operator-(Node e) { - d_eb.append(e.uMinusExpr()); +inline PlusNodeBuilder& PlusNodeBuilder::operator+(PlusNodeBuilder& b) { return *this + Node(d_eb); } +inline PlusNodeBuilder& PlusNodeBuilder::operator+(MultNodeBuilder& b) { return *this + Node(d_eb); } +inline PlusNodeBuilder& PlusNodeBuilder::operator-(PlusNodeBuilder& b) { return *this - Node(d_eb); } +inline PlusNodeBuilder& PlusNodeBuilder::operator-(MultNodeBuilder& b) { return *this - Node(d_eb); } +inline MultNodeBuilder PlusNodeBuilder::operator*(PlusNodeBuilder& b) { return *this * Node(d_eb); } +inline MultNodeBuilder PlusNodeBuilder::operator*(MultNodeBuilder& b) { return *this * Node(d_eb); } +*/ + +template +inline PlusNodeBuilder MultNodeBuilder::operator+(const NodeTemplate& n) { + return PlusNodeBuilder(Node(d_eb), n); +} + +template +inline PlusNodeBuilder MultNodeBuilder::operator-(const NodeTemplate& n) { + return PlusNodeBuilder(Node(d_eb), n); +} + +template +inline MultNodeBuilder& MultNodeBuilder::operator*(const NodeTemplate& n) { + d_eb.append(n); return *this; } + +/* +inline PlusNodeBuilder MultNodeBuilder::operator+(const PlusNodeBuilder& b) { return *this + Node(d_eb); } +inline PlusNodeBuilder MultNodeBuilder::operator+(const MultNodeBuilder& b) { return *this + Node(d_eb); } +inline PlusNodeBuilder MultNodeBuilder::operator-(const PlusNodeBuilder& b) { return *this - Node(d_eb); } +inline PlusNodeBuilder MultNodeBuilder::operator-(const MultNodeBuilder& b) { return *this - Node(d_eb); } +inline MultNodeBuilder& MultNodeBuilder::operator*(const PlusNodeBuilder& b) { return *this * Node(d_eb); } +inline MultNodeBuilder& MultNodeBuilder::operator*(const MultNodeBuilder& b) { return *this * Node(d_eb); } */ -inline MultNodeBuilder PlusNodeBuilder::operator*(Node e) { - Node n = d_eb; - d_eb.clear(); - d_eb.append(n); - return MultNodeBuilder(d_eb) * e; +template +inline AndNodeBuilder operator&&(const NodeTemplate& a, const NodeTemplate& b) { + return AndNodeBuilder(a, b); } -inline PlusNodeBuilder MultNodeBuilder::operator+(Node e) { - Node n = d_eb; - d_eb.clear(); - d_eb.append(n); - return MultNodeBuilder(d_eb) + e; +template +inline OrNodeBuilder operator||(const NodeTemplate& a, const NodeTemplate& b) { + return OrNodeBuilder(a, b); } -inline PlusNodeBuilder MultNodeBuilder::operator-(Node e) { - Node n = d_eb; - d_eb.clear(); - d_eb.append(n); - return MultNodeBuilder(d_eb) - e; +template +inline PlusNodeBuilder operator+(const NodeTemplate& a, const NodeTemplate& b) { + return PlusNodeBuilder(a, b); } -inline MultNodeBuilder& MultNodeBuilder::operator*(Node e) { - d_eb.append(e); - return *this; +template +inline PlusNodeBuilder operator-(const NodeTemplate& a, const NodeTemplate& b) { + return PlusNodeBuilder(a, NodeManager::currentNM()->mkNode(kind::UMINUS, b)); +} + +template +inline MultNodeBuilder operator*(const NodeTemplate& a, const NodeTemplate& b) { + return MultNodeBuilder(a, b); +} + +template +inline AndNodeBuilder operator&&(const NodeTemplate& a, const AndNodeBuilder& b) { + return a && Node(b.d_eb); +} + +template +inline AndNodeBuilder operator&&(const NodeTemplate& a, const OrNodeBuilder& b) { + return a && Node(b.d_eb); +} + +template +inline OrNodeBuilder operator||(const NodeTemplate& a, const AndNodeBuilder& b) { + return a || Node(b.d_eb); +} + +template +inline OrNodeBuilder operator||(const NodeTemplate& a, const OrNodeBuilder& b) { + return a || Node(b.d_eb); } }/* CVC4 namespace */ @@ -436,7 +531,6 @@ inline NodeBuilder::NodeBuilder(Kind k) : d_inlineNv(0), d_childrenStorage() { - //Message() << "kind " << k << std::endl; d_inlineNv.d_kind = k; } @@ -458,6 +552,11 @@ inline NodeBuilder::NodeBuilder(const NodeBuilder& } d_nv->d_kind = nb.d_nv->d_kind; d_nv->d_nchildren = nb.d_nv->d_nchildren; + for(expr::NodeValue::nv_iterator i = d_nv->nv_begin(); + i != d_nv->nv_end(); + ++i) { + (*i)->inc(); + } } template @@ -479,6 +578,11 @@ inline NodeBuilder::NodeBuilder(const NodeBuilder& nb) : } d_nv->d_kind = nb.d_nv->d_kind; d_nv->d_nchildren = nb.d_nv->d_nchildren; + for(expr::NodeValue::nv_iterator i = d_nv->nv_begin(); + i != d_nv->nv_end(); + ++i) { + (*i)->inc(); + } } template @@ -490,7 +594,7 @@ inline NodeBuilder::NodeBuilder(NodeManager* nm) : d_nv(&d_inlineNv), d_inlineNv(0), d_childrenStorage() { - d_inlineNv.d_kind = NodeValue::kindToDKind(kind::UNDEFINED_KIND); + d_inlineNv.d_kind = expr::NodeValue::kindToDKind(kind::UNDEFINED_KIND); } template @@ -503,12 +607,11 @@ inline NodeBuilder::NodeBuilder(NodeManager* nm, Kind k) : d_inlineNv(0), d_childrenStorage() { - //Message() << "kind " << k << std::endl; d_inlineNv.d_kind = k; } template -inline NodeBuilder::~NodeBuilder() { +inline NodeBuilder::~NodeBuilder() throw() { if(!d_used) { // Warning("NodeBuilder unused at destruction\n"); // Commented above, as it happens a lot, for example with exceptions @@ -536,12 +639,12 @@ void NodeBuilder::clear(Kind k) { template void NodeBuilder::realloc() { if(EXPECT_FALSE( nvIsAllocated() )) { - d_nv = (NodeValue*) + d_nv = (expr::NodeValue*) std::realloc(d_nv, - sizeof(NodeValue) + ( sizeof(NodeValue*) * (d_size *= 2) )); + sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * (d_size *= 2) )); } else { - d_nv = (NodeValue*) - std::malloc(sizeof(NodeValue) + ( sizeof(NodeValue*) * (d_size *= 2) )); + d_nv = (expr::NodeValue*) + std::malloc(sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * (d_size *= 2) )); d_nv->d_id = 0; d_nv->d_rc = 0; d_nv->d_kind = d_inlineNv.d_kind; @@ -557,13 +660,13 @@ void NodeBuilder::realloc(size_t toSize, bool copy) { Assert( d_size < toSize ); if(EXPECT_FALSE( nvIsAllocated() )) { - d_nv = (NodeValue*) - std::realloc(d_nv, sizeof(NodeValue) + - ( sizeof(NodeValue*) * (d_size = toSize) )); + d_nv = (expr::NodeValue*) + std::realloc(d_nv, sizeof(expr::NodeValue) + + ( sizeof(expr::NodeValue*) * (d_size = toSize) )); } else { - d_nv = (NodeValue*) - std::malloc(sizeof(NodeValue) + - ( sizeof(NodeValue*) * (d_size = toSize) )); + d_nv = (expr::NodeValue*) + std::malloc(sizeof(expr::NodeValue) + + ( sizeof(expr::NodeValue*) * (d_size = toSize) )); d_nv->d_id = 0; d_nv->d_rc = 0; d_nv->d_kind = d_inlineNv.d_kind; @@ -579,14 +682,14 @@ void NodeBuilder::realloc(size_t toSize, bool copy) { } template -inline void NodeBuilder::dealloc() { +inline void NodeBuilder::dealloc() throw() { /* Prefer asserts to if() because usually these conditions have been * checked already, so we don't want to do a double-check in * production; these are just sanity checks for debug builds */ - Assert(!d_used, - "Internal error: NodeBuilder: dealloc() called with d_used"); + DtorAssert(!d_used, + "Internal error: NodeBuilder: dealloc() called with d_used"); - for(NodeValue::nv_iterator i = d_nv->nv_begin(); + for(expr::NodeValue::nv_iterator i = d_nv->nv_begin(); i != d_nv->nv_end(); ++i) { (*i)->dec(); @@ -596,20 +699,110 @@ inline void NodeBuilder::dealloc() { } } +template +NodeBuilder::operator Node() const {// const version + Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); + Assert(d_nv->getKind() != kind::UNDEFINED_KIND, + "Can't make an expression of an undefined kind!"); + + if(d_nv->d_kind == kind::VARIABLE) { + Assert(d_nv->d_nchildren == 0); + expr::NodeValue *nv = (expr::NodeValue*) + std::malloc(sizeof(expr::NodeValue) + + (sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));// FIXME :: WTF?? + nv->d_nchildren = 0; + nv->d_kind = kind::VARIABLE; + nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading + nv->d_rc = 0; + //d_used = true; // const version + //d_nv = NULL; // const version + return Node(nv); + } + + // implementation differs depending on whether the expression value + // was malloc'ed or not + + if(EXPECT_FALSE( nvIsAllocated() )) { + // Lookup the expression value in the pool we already have (with insert) + expr::NodeValue* nv = d_nm->poolLookup(d_nv); + // If something else is there, we reuse it + if(nv != NULL) { + // expression already exists in node manager + //dealloc(); // const version + //d_used = true; // const version + return Node(nv); + } + // Otherwise copy children out + nv = (expr::NodeValue*) + std::malloc(sizeof(expr::NodeValue) + + ( sizeof(expr::NodeValue*) * d_nv->d_nchildren )); + nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading + nv->d_rc = 0; + nv->d_kind = d_nv->d_kind; + nv->d_nchildren = d_nv->d_nchildren; + std::copy(d_nv->d_children, + d_nv->d_children + d_nv->d_nchildren, + nv->d_children); + // inc child refcounts + for(expr::NodeValue::nv_iterator i = nv->nv_begin(); + i != nv->nv_end(); + ++i) { + (*i)->inc(); + } + d_nm->poolInsert(nv); + return Node(nv); + } + + // Lookup the expression value in the pool we already have + expr::NodeValue* ev = d_nm->poolLookup(d_nv); + //DANGER d_nv should be ptr-to-const in the above line b/c it points to d_inlineNv + if(ev != NULL) { + // expression already exists in node manager + //d_used = true; // const version + Debug("prop") << "result: " << Node(ev) << std::endl; + return Node(ev); + } + + // otherwise create the canonical expression value for this node + ev = (expr::NodeValue*) + std::malloc(sizeof(expr::NodeValue) + + ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren )); + ev->d_nchildren = d_inlineNv.d_nchildren; + ev->d_kind = d_inlineNv.d_kind; + ev->d_id = expr::NodeValue::next_id++;// FIXME multithreading + ev->d_rc = 0; + std::copy(d_inlineNv.d_children, + d_inlineNv.d_children + d_inlineNv.d_nchildren, + ev->d_children); + //d_used = true; + //d_nv = NULL; + //d_inlineNv.d_nchildren = 0;// inhibit decr'ing refcounts of children in dtor + // inc child refcounts + for(expr::NodeValue::nv_iterator i = ev->nv_begin(); + i != ev->nv_end(); + ++i) { + (*i)->inc(); + } + + // Make the new expression + d_nm->poolInsert(ev); + return Node(ev); +} + template NodeBuilder::operator Node() {// not const - Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); + Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); Assert(d_nv->getKind() != kind::UNDEFINED_KIND, "Can't make an expression of an undefined kind!"); if(d_nv->d_kind == kind::VARIABLE) { Assert(d_nv->d_nchildren == 0); - NodeValue *nv = (NodeValue*) - std::malloc(sizeof(NodeValue) + - (sizeof(NodeValue*) * d_inlineNv.d_nchildren ));// FIXME :: WTF?? + expr::NodeValue *nv = (expr::NodeValue*) + std::malloc(sizeof(expr::NodeValue) + + (sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));// FIXME :: WTF?? nv->d_nchildren = 0; nv->d_kind = kind::VARIABLE; - nv->d_id = NodeValue::next_id++;// FIXME multithreading + nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading nv->d_rc = 0; d_used = true; d_nv = NULL; @@ -622,7 +815,7 @@ NodeBuilder::operator Node() {// not const if(EXPECT_FALSE( nvIsAllocated() )) { // Lookup the expression value in the pool we already have (with insert) - NodeValue* nv = d_nm->poolLookup(d_nv); + expr::NodeValue* nv = d_nm->poolLookup(d_nv); // If something else is there, we reuse it if(nv != NULL) { // expression already exists in node manager @@ -631,19 +824,18 @@ NodeBuilder::operator Node() {// not const Debug("prop") << "result: " << Node(nv) << std::endl; return Node(nv); } - // Otherwise crop and set the expression value to the allocate one + // Otherwise crop and set the expression value to the allocated one crop(); nv = d_nv; + nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading d_nv = NULL; d_used = true; d_nm->poolInsert(nv); - Node n(nv); - Debug("prop") << "result: " << n << std::endl; - return n; + return Node(nv); } // Lookup the expression value in the pool we already have - NodeValue* ev = d_nm->poolLookup(&d_inlineNv); + expr::NodeValue* ev = d_nm->poolLookup(&d_inlineNv); if(ev != NULL) { // expression already exists in node manager d_used = true; @@ -652,12 +844,12 @@ NodeBuilder::operator Node() {// not const } // otherwise create the canonical expression value for this node - ev = (NodeValue*) - std::malloc(sizeof(NodeValue) + - ( sizeof(NodeValue*) * d_inlineNv.d_nchildren )); + ev = (expr::NodeValue*) + std::malloc(sizeof(expr::NodeValue) + + ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren )); ev->d_nchildren = d_inlineNv.d_nchildren; ev->d_kind = d_inlineNv.d_kind; - ev->d_id = NodeValue::next_id++;// FIXME multithreading + ev->d_id = expr::NodeValue::next_id++;// FIXME multithreading ev->d_rc = 0; std::copy(d_inlineNv.d_children, d_inlineNv.d_children + d_inlineNv.d_nchildren, @@ -668,9 +860,7 @@ NodeBuilder::operator Node() {// not const // Make the new expression d_nm->poolInsert(ev); - Node n(ev); - Debug("prop") << "result: " << n << std::endl; - return n; + return Node(ev); } template diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 00fcf52c4..62bcc7516 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -29,16 +29,6 @@ #include "expr/kind.h" #include "expr/expr.h" -namespace __gnu_cxx { - template<> - struct hash { - size_t operator()(const CVC4::NodeValue* nv) const { - return (size_t)nv->hash(); - } - }; -}/* __gnu_cxx namespace */ - - namespace CVC4 { class Type; @@ -61,20 +51,21 @@ class NodeManager { template friend class CVC4::NodeBuilder; - typedef __gnu_cxx::hash_set, NodeValue::NodeValueEq> NodeValueSet; + typedef __gnu_cxx::hash_set NodeValueSet; NodeValueSet d_nodeValueSet; expr::attr::AttributeManager d_attrManager; - NodeValue* poolLookup(NodeValue* nv) const; - void poolInsert(NodeValue* nv); + expr::NodeValue* poolLookup(expr::NodeValue* nv) const; + void poolInsert(expr::NodeValue* nv); friend class NodeManagerScope; public: NodeManager() { - poolInsert( &NodeValue::s_null ); + poolInsert( &expr::NodeValue::s_null ); } static NodeManager* currentNM() { return s_current; } @@ -152,7 +143,7 @@ public: Debug("current") << "node manager scope: " << NodeManager::s_current << "\n"; } - ~NodeManagerScope() { + ~NodeManagerScope() throw() { NodeManager::s_current = d_oldNodeManager; Debug("current") << "node manager scope: returning to " << NodeManager::s_current << "\n"; } @@ -224,9 +215,9 @@ inline const Type* NodeManager::getType(TNode n) { return getAttribute(n, CVC4::expr::TypeAttr()); } -inline void NodeManager::poolInsert(NodeValue* nv) { - Assert(d_nodeValueSet.find(nv) == d_nodeValueSet.end(), "NodeValue already in" - "the pool!"); +inline void NodeManager::poolInsert(expr::NodeValue* nv) { + Assert(d_nodeValueSet.find(nv) == d_nodeValueSet.end(), + "NodeValue already in the pool!"); d_nodeValueSet.insert(nv); } diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index b95f8ff0a..5c5765011 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -24,6 +24,7 @@ using namespace std; namespace CVC4 { +namespace expr { size_t NodeValue::next_id = 1; @@ -56,4 +57,5 @@ void NodeValue::toStream(std::ostream& out) const { } } +}/* CVC4::expr namespace */ }/* CVC4 namespace */ diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 0ad7ba559..523c5387b 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -98,7 +98,7 @@ class NodeValue { NodeValue(int); /** Destructor decrements the ref counts of its children */ - ~NodeValue(); + ~NodeValue() throw(); typedef NodeValue** nv_iterator; typedef NodeValue const* const* const_nv_iterator; @@ -165,17 +165,26 @@ public: } inline bool compareTo(const NodeValue* nv) const { - if(d_kind != nv->d_kind) + if(d_kind != nv->d_kind) { return false; - if(d_nchildren != nv->d_nchildren) + } + + if(d_nchildren != nv->d_nchildren) { return false; + } + const_nv_iterator i = nv_begin(); const_nv_iterator j = nv->nv_begin(); const_nv_iterator i_end = nv_end(); + while(i != i_end) { - if ((*i) != (*j)) return false; - ++i; ++j; + if((*i) != (*j)) { + return false; + } + ++i; + ++j; } + return true; } @@ -196,6 +205,7 @@ public: static inline unsigned kindToDKind(Kind k) { return ((unsigned) k) & kindMask; } + static inline Kind dKindToKind(unsigned d) { return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d); } @@ -215,7 +225,7 @@ inline NodeValue::NodeValue(int) : d_nchildren(0) { } -inline NodeValue::~NodeValue() { +inline NodeValue::~NodeValue() throw() { for(nv_iterator i = nv_begin(); i != nv_end(); ++i) { (*i)->dec(); } @@ -254,6 +264,13 @@ inline NodeValue::const_nv_iterator NodeValue::nv_end() const { return d_children + d_nchildren; } +// for hash_maps, hash_sets, ... +struct NodeValueHashFcn { + size_t operator()(const CVC4::expr::NodeValue* nv) const { + return (size_t)nv->hash(); + } +};/* struct NodeValueHashFcn */ + }/* CVC4::expr namespace */ }/* CVC4 namespace */ diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h index bfa38ec28..5838790a8 100644 --- a/src/parser/symbol_table.h +++ b/src/parser/symbol_table.h @@ -23,18 +23,15 @@ #include -namespace __gnu_cxx { -template<> - struct hash { - size_t operator()(const std::string& str) const { - return hash()(str.c_str()); - } - }; -}/* __gnu_cxx namespace */ - namespace CVC4 { namespace parser { +struct StringHashFcn { + size_t operator()(const std::string& str) const { + return __gnu_cxx::hash()(str.c_str()); + } +}; + /** * Generic symbol table for looking up variables by name. */ @@ -44,12 +41,9 @@ class SymbolTable { private: /** The name to expression bindings */ - typedef __gnu_cxx::hash_map + typedef __gnu_cxx::hash_map LookupTable; -/* - typedef __gnu_cxx::hash_map > - LookupTable; -*/ + /** The table iterator */ typedef typename LookupTable::iterator table_iterator; /** The table iterator */ diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index da3f7b1ed..9af15ba31 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -46,7 +46,7 @@ private: SatSolver *d_satSolver; /** Cache of what literal have been registered to a node. */ - __gnu_cxx::hash_map d_translationCache; + __gnu_cxx::hash_map d_translationCache; protected: diff --git a/src/util/Assert.h b/src/util/Assert.h index 8f03ecd45..3b42f2887 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -24,6 +24,8 @@ #include "cvc4_config.h" #include "config.h" +#include + namespace CVC4 { class CVC4_PUBLIC AssertionException : public Exception { @@ -196,6 +198,8 @@ public: throw AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ } \ } while(0) +#define DtorAlwaysAssert(cond, msg...) \ + assert(EXPECT_TRUE( cond )) #define Unreachable(msg...) \ throw UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define Unhandled(msg...) \ @@ -215,9 +219,11 @@ public: #ifdef CVC4_ASSERTIONS # define Assert(cond, msg...) AlwaysAssert(cond, ## msg) +# define DtorAssert(cond, msg...) assert(EXPECT_TRUE( cond )) # define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ## msg) #else /* ! CVC4_ASSERTIONS */ # define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/ +# define DtorAssert(cond, msg...) /*EXPECT_TRUE( cond )*/ # define AssertArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/ #endif /* CVC4_ASSERTIONS */ diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 8aff0faf0..871e93dca 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -15,7 +15,6 @@ #include -//Used in some of the tests #include #include #include @@ -65,7 +64,7 @@ public: /** * Tests just constructors. No modification is done to the node. */ - void testNodeConstructors(){ + void testNodeConstructors() { //inline NodeBuilder(); //inline NodeBuilder(Kind k); @@ -151,14 +150,14 @@ public: } - void testDestructor(){ + void testDestructor() { //inline ~NodeBuilder(); NodeBuilder* nb = new NodeBuilder(); delete nb; //Not sure what to test other than survival } - void testBeginEnd(){ + void testBeginEnd() { /* Test begin and ends without resizing */ NodeBuilder ws; TS_ASSERT_EQUALS(ws.begin(), ws.end()); @@ -203,12 +202,12 @@ public: TS_ASSERT_EQUALS(smaller_citer, smaller.end()); } - void testIterator(){ + void testIterator() { NodeBuilder<> b; Node x = d_nm->mkVar(); Node y = d_nm->mkVar(); Node z = d_nm->mkVar(); - b << x << y << z << kind::AND; + b << x << y << z << AND; { NodeBuilder<>::iterator i = b.begin(); @@ -228,7 +227,7 @@ public: } } - void testGetKind(){ + void testGetKind() { /* Kind getKind() const; */ NodeBuilder<> noKind; TS_ASSERT_EQUALS(noKind.getKind(), UNDEFINED_KIND); @@ -244,15 +243,13 @@ public: TS_ASSERT_THROWS_ANYTHING(noKind.getKind();); #endif - NodeBuilder<> spec(specKind); TS_ASSERT_EQUALS(spec.getKind(), specKind); push_back(spec, K); TS_ASSERT_EQUALS(spec.getKind(), specKind); - } - void testGetNumChildren(){ + void testGetNumChildren() { /* unsigned getNumChildren() const; */ NodeBuilder<> noKind; @@ -282,7 +279,7 @@ public: #endif } - void testOperatorSquare(){ + void testOperatorSquare() { /* Node operator[](int i) const { Assert(i >= 0 && i < d_ev->getNumChildren()); @@ -332,7 +329,7 @@ public: #endif } - void testClear(){ + void testClear() { /* void clear(Kind k = UNDEFINED_KIND); */ NodeBuilder<> nb; @@ -378,7 +375,7 @@ public: } - void testStreamInsertionKind(){ + void testStreamInsertionKind() { /* NodeBuilder& operator<<(const Kind& k); */ #ifdef CVC4_DEBUG @@ -420,7 +417,7 @@ public: specKind); } - void testStreamInsertionNode(){ + void testStreamInsertionNode() { /* NodeBuilder& operator<<(const Node& n); */ NodeBuilder nb(specKind); TS_ASSERT_EQUALS(nb.getKind(), specKind); @@ -449,7 +446,7 @@ public: } - void testAppend(){ + void testAppend() { Node x = d_nm->mkVar(); Node y = d_nm->mkVar(); Node z = d_nm->mkVar(); @@ -499,7 +496,7 @@ public: TS_ASSERT(b[8] == m); } - void testOperatorNodeCast(){ + void testOperatorNodeCast() { /* operator Node();*/ NodeBuilder implicit(specKind); NodeBuilder explic(specKind); @@ -521,7 +518,7 @@ public: #endif } - void testToStream(){ + void testToStream() { /* inline void toStream(std::ostream& out) const { d_ev->toStream(out); } @@ -571,4 +568,61 @@ public: TS_ASSERT_EQUALS(astr, bstr); TS_ASSERT_DIFFERS(astr, cstr); } + + void testConvenienceBuilders() { + Node a = d_nm->mkVar(); + Node b = d_nm->mkVar(); + Node c = d_nm->mkVar(); + Node d = d_nm->mkVar(); + Node e = d_nm->mkVar(); + Node f = d_nm->mkVar(); + + Node m = a && b; + Node n = a && b || c; + Node o = d + e - b; + Node p = a && o || c; + + Node x = d + e + o - m; + Node y = f - a - c + e; + + Node q = a && b && c; + + Node r = e && d && b && a || x && y || f || q && a; + + TS_ASSERT_EQUALS(m, d_nm->mkNode(AND, a, b)); + TS_ASSERT_EQUALS(n, d_nm->mkNode(OR, m, c)); + TS_ASSERT_EQUALS(o, d_nm->mkNode(PLUS, d, e, d_nm->mkNode(UMINUS, b))); + TS_ASSERT_EQUALS(p, d_nm->mkNode(OR, d_nm->mkNode(AND, a, o), c)); + + TS_ASSERT_EQUALS(x, d_nm->mkNode(PLUS, d, e, o, d_nm->mkNode(UMINUS, m))); + TS_ASSERT_EQUALS(y, d_nm->mkNode(PLUS, + f, + d_nm->mkNode(UMINUS, a), + d_nm->mkNode(UMINUS, c), + e)); + + TS_ASSERT_EQUALS(q, d_nm->mkNode(AND, a, b, c)); + + TS_ASSERT_EQUALS(r, d_nm->mkNode(OR, + d_nm->mkNode(AND, e, d, b, a), + d_nm->mkNode(AND, x, y), + f, + d_nm->mkNode(AND, q, a))); + + Node assoc1 = (a && b) && c; + Node assoc2 = a && (b && c); + + TS_ASSERT_EQUALS(assoc1, d_nm->mkNode(AND, a, b, c)); + TS_ASSERT_EQUALS(assoc2, d_nm->mkNode(AND, a, d_nm->mkNode(AND, b, c))); + + Node prec1 = (a && b) || c; + Node prec2 = a || (b && c); + Node prec3 = a && (b || c); + Node prec4 = (a || b) && c; + + TS_ASSERT_EQUALS(prec1, d_nm->mkNode(OR, d_nm->mkNode(AND, a, b), c)); + TS_ASSERT_EQUALS(prec2, d_nm->mkNode(OR, a, d_nm->mkNode(AND, b, c))); + TS_ASSERT_EQUALS(prec3, d_nm->mkNode(AND, a, d_nm->mkNode(OR, b, c))); + TS_ASSERT_EQUALS(prec4, d_nm->mkNode(AND, d_nm->mkNode(OR, a, b), c)); + } }; diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index ee914090e..17fefd07b 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -29,17 +29,17 @@ using namespace CVC4::context; using namespace std; - /** * Very basic OutputChannel for testing simple Theory Behaviour. * Stores a call sequence for the output channel */ -enum OutputChannelCallType{CONFLICT, PROPOGATE, LEMMA, EXPLANATION}; +enum OutputChannelCallType{CONFLICT, PROPAGATE, LEMMA, EXPLANATION}; class TestOutputChannel : public OutputChannel { private: - void push(OutputChannelCallType call, TNode n){ - d_callHistory.push_back(make_pair(call,n)); + void push(OutputChannelCallType call, TNode n) { + d_callHistory.push_back(make_pair(call, n)); } + public: vector< pair > d_callHistory; @@ -49,71 +49,78 @@ public: void safePoint() throw(Interrupted) {} - void conflict(TNode n, bool safe = false) throw(Interrupted){ + void conflict(TNode n, bool safe = false) throw(Interrupted) { push(CONFLICT, n); } - void propagate(TNode n, bool safe = false) throw(Interrupted){ - push(PROPOGATE, n); + void propagate(TNode n, bool safe = false) throw(Interrupted) { + push(PROPAGATE, n); } - void lemma(TNode n, bool safe = false) throw(Interrupted){ + void lemma(TNode n, bool safe = false) throw(Interrupted) { push(LEMMA, n); } - void explanation(TNode n, bool safe = false) throw(Interrupted){ + void explanation(TNode n, bool safe = false) throw(Interrupted) { push(EXPLANATION, n); } - void clear(){ + void clear() { d_callHistory.clear(); } - Node getIthNode(int i){ + + Node getIthNode(int i) { Node tmp = (d_callHistory[i]).second; return tmp; } - OutputChannelCallType getIthCallType(int i){ + OutputChannelCallType getIthCallType(int i) { return (d_callHistory[i]).first; } - unsigned getNumCalls(){ + unsigned getNumCalls() { return d_callHistory.size(); } }; class DummyTheory : public TheoryImpl { public: - vector d_registerSequence; + set d_registered; vector d_getSequence; DummyTheory(context::Context* ctxt, OutputChannel& out) : TheoryImpl(ctxt, out) {} - void registerTerm(TNode n){ - d_registerSequence.push_back(n); - } + void registerTerm(TNode n) { + // check that we registerTerm() a term only once + TS_ASSERT(d_registered.find(n) == d_registered.end()); + for(TNode::iterator i = n.begin(); i != n.end(); ++i) { + // check that registerTerm() is called in reverse topological order + TS_ASSERT(d_registered.find(*i) != d_registered.end()); + } + + d_registered.insert(n); + } - Node getWrapper(){ + Node getWrapper() { Node n = get(); d_getSequence.push_back(n); return n; } - bool doneWrapper(){ + bool doneWrapper() { return done(); } - void check(Effort e){ - while(!done()){ + void check(Effort e) { + while(!done()) { getWrapper(); } } - void preRegisterTerm(TNode n ){} - void propagate(Effort level = FULL_EFFORT){} - void explain(TNode n, Effort level = FULL_EFFORT){} - + void preRegisterTerm(TNode n) {} + void propagate(Effort level) {} + void explain(TNode n, Effort level) {} }; class TheoryBlack : public CxxTest::TestSuite { @@ -132,7 +139,7 @@ class TheoryBlack : public CxxTest::TestSuite { public: - TheoryBlack() { } + TheoryBlack() {} void setUp() { d_nm = new NodeManager(); @@ -187,15 +194,13 @@ public: TS_ASSERT( Theory::quickCheckOrMore(s)); TS_ASSERT( Theory::quickCheckOrMore(f)); - TS_ASSERT(!Theory::standardEffortOrMore(m)); TS_ASSERT(!Theory::standardEffortOrMore(q)); TS_ASSERT( Theory::standardEffortOrMore(s)); TS_ASSERT( Theory::standardEffortOrMore(f)); - } - void testDone(){ + void testDone() { TS_ASSERT(d_dummy->doneWrapper()); d_dummy->assertFact(atom0); @@ -208,7 +213,7 @@ public: TS_ASSERT(d_dummy->doneWrapper()); } - void testRegisterSequence(){ + void testRegisterTerm() { TS_ASSERT(d_dummy->doneWrapper()); Node x = d_nm->mkVar(); @@ -218,7 +223,6 @@ public: Node f_x_eq_x = f_x.eqNode(x); Node x_eq_f_f_x = x.eqNode(f_f_x); - d_dummy->assertFact(f_x_eq_x); d_dummy->assertFact(x_eq_f_f_x); @@ -226,11 +230,13 @@ public: TS_ASSERT_EQUALS(got, f_x_eq_x); - TS_ASSERT_EQUALS(4, d_dummy-> d_registerSequence.size()); - TS_ASSERT_EQUALS(x, d_dummy-> d_registerSequence[0]); - TS_ASSERT_EQUALS(f, d_dummy-> d_registerSequence[1]); - TS_ASSERT_EQUALS(f_x, d_dummy-> d_registerSequence[2]); - TS_ASSERT_EQUALS(f_x_eq_x, d_dummy-> d_registerSequence[3]); + TS_ASSERT_EQUALS(4, d_dummy->d_registered.size()); + TS_ASSERT(d_dummy->d_registered.find(x) != d_dummy->d_registered.end()); + TS_ASSERT(d_dummy->d_registered.find(f) != d_dummy->d_registered.end()); + TS_ASSERT(d_dummy->d_registered.find(f_x) != d_dummy->d_registered.end()); + TS_ASSERT(d_dummy->d_registered.find(f_x_eq_x) != d_dummy->d_registered.end()); + TS_ASSERT(d_dummy->d_registered.find(f_f_x) == d_dummy->d_registered.end()); + TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) == d_dummy->d_registered.end()); TS_ASSERT(!d_dummy->doneWrapper()); @@ -238,15 +244,14 @@ public: TS_ASSERT_EQUALS(got, x_eq_f_f_x); - TS_ASSERT_EQUALS(6, d_dummy-> d_registerSequence.size()); - TS_ASSERT_EQUALS(f_f_x, d_dummy-> d_registerSequence[4]); - TS_ASSERT_EQUALS(x_eq_f_f_x, d_dummy-> d_registerSequence[5]); + TS_ASSERT_EQUALS(6, d_dummy->d_registered.size()); + TS_ASSERT(d_dummy->d_registered.find(f_f_x) != d_dummy->d_registered.end()); + TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) != d_dummy->d_registered.end()); TS_ASSERT(d_dummy->doneWrapper()); } - - void testOutputChannelAccessors(){ + void testOutputChannelAccessors() { /* void setOutputChannel(OutputChannel& out) */ /* OutputChannel& getOutputChannel() */ @@ -261,7 +266,5 @@ public: const OutputChannel& oc = d_dummy->getOutputChannel(); TS_ASSERT_EQUALS(&oc, &theOtherChannel); - } - }; -- 2.30.2