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 \
class Type;
class NodeManager;
-template<bool ref_count>
- class NodeTemplate;
+
+template<bool ref_count> class NodeTemplate;
+
/**
* The Node class encapsulates the NodeValue with reference counting.
*/
typedef NodeTemplate<false> 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
* @param ref_count if true reference are counted in the NodeValue
*/
template<bool ref_count>
- 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<true> ;
- friend class NodeTemplate<false> ;
- friend class NodeManager;
- template<unsigned>
- 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<!ref_count>& 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<!ref_count>& 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 ref_count_1>
- bool operator==(const NodeTemplate<ref_count_1>& 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 ref_count_1>
- bool operator!=(const NodeTemplate<ref_count_1>& 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<true> ;
+ friend class NodeTemplate<false> ;
+ friend class NodeManager;
+
+ template<unsigned>
+ 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<!ref_count>& 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<!ref_count>& 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 <bool ref_count_1>
- inline bool operator<(const NodeTemplate<ref_count_1>& 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 ref_count_1>
+ bool operator==(const NodeTemplate<ref_count_1>& 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 ref_count_1>
+ bool operator!=(const NodeTemplate<ref_count_1>& 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 <bool ref_count_1>
+ inline bool operator<(const NodeTemplate<ref_count_1>& 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<true> getOperator() const {
- switch(getKind()) {
- case kind::APPLY:
- /* The operator is the first child. */
- return NodeTemplate<true> (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<true> 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<true> 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 <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
- * 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 <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;
- /** Constant iterator allowing for scanning through the children. */
- typedef typename NodeValue::iterator<ref_count> const_iterator;
-
- /**
- * Returns the iterator pointing to the first child.
- * @return the iterator
- */
- inline iterator begin() {
- return d_nv->begin<ref_count>();
- }
+ /**
+ * 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 <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
+ * 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 <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 expr::NodeValue::iterator<ref_count> iterator;
+ /** Constant iterator allowing for scanning through the children. */
+ typedef typename expr::NodeValue::iterator<ref_count> const_iterator;
+
+ /**
+ * Returns the iterator pointing to the first child.
+ * @return the iterator
+ */
+ inline iterator begin() {
+ return d_nv->begin<ref_count>();
+ }
- /**
- * 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<ref_count>();
- }
+ /**
+ * 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<ref_count>();
+ }
- /**
- * Returns the const_iterator pointing to the first child.
- * @return the const_iterator
- */
- inline const_iterator begin() const {
- return d_nv->begin<ref_count>();
- }
+ /**
+ * Returns the const_iterator pointing to the first child.
+ * @return the const_iterator
+ */
+ inline const_iterator begin() const {
+ return d_nv->begin<ref_count>();
+ }
- /**
- * 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<ref_count>();
- }
+ /**
+ * 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<ref_count>();
+ }
- /**
- * 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<true> eqNode(const NodeTemplate& right) const;
-
- NodeTemplate<true> notNode() const;
- NodeTemplate<true> andNode(const NodeTemplate& right) const;
- NodeTemplate<true> orNode(const NodeTemplate& right) const;
- NodeTemplate<true> iteNode(const NodeTemplate& thenpart,
- const NodeTemplate& elsepart) const;
- NodeTemplate<true> iffNode(const NodeTemplate& right) const;
- NodeTemplate<true> impNode(const NodeTemplate& right) const;
- NodeTemplate<true> 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<true> eqNode(const NodeTemplate& right) const;
+
+ NodeTemplate<true> notNode() const;
+ NodeTemplate<true> andNode(const NodeTemplate& right) const;
+ NodeTemplate<true> orNode(const NodeTemplate& right) const;
+ NodeTemplate<true> iteNode(const NodeTemplate& thenpart,
+ const NodeTemplate& elsepart) const;
+ NodeTemplate<true> iffNode(const NodeTemplate& right) const;
+ NodeTemplate<true> impNode(const NodeTemplate& right) const;
+ NodeTemplate<true> 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.
#include <ext/hash_map>
-// for hashtables
-namespace __gnu_cxx {
-template<>
- struct hash<CVC4::Node> {
- 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<bool ref_count>
- inline size_t NodeTemplate<ref_count>::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<bool ref_count>
- template<class AttrKind>
- inline typename AttrKind::value_type NodeTemplate<ref_count>::
- getAttribute(const AttrKind&) const {
- Assert( NodeManager::currentNM() != NULL,
+inline size_t NodeTemplate<ref_count>::getNumChildren() const {
+ return d_nv->d_nchildren;
+}
+
+template<bool ref_count>
+template<class AttrKind>
+inline typename AttrKind::value_type NodeTemplate<ref_count>::
+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<bool ref_count>
- template<class AttrKind>
- inline bool NodeTemplate<ref_count>::
- hasAttribute(const AttrKind&) const {
- Assert( NodeManager::currentNM() != NULL,
+template<class AttrKind>
+inline bool NodeTemplate<ref_count>::
+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<bool ref_count>
- template<class AttrKind>
- inline bool NodeTemplate<ref_count>::
- hasAttribute(const AttrKind&, typename AttrKind::value_type& ret) const {
- Assert( NodeManager::currentNM() != NULL,
+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 ?" );
- return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret);
- }
+ return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret);
+}
template<bool ref_count>
- template<class AttrKind>
- inline void NodeTemplate<ref_count>::
- setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
- Assert( NodeManager::currentNM() != NULL,
+template<class AttrKind>
+inline void NodeTemplate<ref_count>::
+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<bool ref_count>
- NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&NodeValue::s_null);
+NodeTemplate<ref_count> NodeTemplate<ref_count>::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 ref_count>
- bool NodeTemplate<ref_count>::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<ref_count>::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<bool ref_count>
- NodeTemplate<ref_count>::NodeTemplate(const NodeValue* ev) :
- d_nv(const_cast<NodeValue*> (ev)) {
- Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
- if(ref_count)
- d_nv->inc();
+NodeTemplate<ref_count>::NodeTemplate(const expr::NodeValue* ev) :
+ d_nv(const_cast<expr::NodeValue*> (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<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();
+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(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<ref_count>::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<bool ref_count>
- NodeTemplate<ref_count>::~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<ref_count>::~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<bool ref_count>
- void NodeTemplate<ref_count>::assignNodeValue(NodeValue* ev) {
- d_nv = ev;
- if(ref_count)
- d_nv->inc();
+void NodeTemplate<ref_count>::assignNodeValue(expr::NodeValue* ev) {
+ d_nv = ev;
+ if(ref_count) {
+ d_nv->inc();
}
+}
template<bool ref_count>
- NodeTemplate<ref_count>& NodeTemplate<ref_count>::
- 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<ref_count>& NodeTemplate<ref_count>::
+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<bool ref_count>
- NodeTemplate<ref_count>& NodeTemplate<ref_count>::
- operator=(const NodeTemplate<!ref_count>& 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<ref_count>& NodeTemplate<ref_count>::
+operator=(const NodeTemplate<!ref_count>& 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<bool ref_count>
- NodeTemplate<true> NodeTemplate<ref_count>::eqNode(const NodeTemplate<
- ref_count>& right) const {
- return NodeManager::currentNM()->mkNode(kind::EQUAL, *this, right);
- }
+NodeTemplate<true> NodeTemplate<ref_count>::eqNode(const NodeTemplate<
+ ref_count>& right) const {
+ return NodeManager::currentNM()->mkNode(kind::EQUAL, *this, right);
+}
template<bool ref_count>
- NodeTemplate<true> NodeTemplate<ref_count>::notNode() const {
- return NodeManager::currentNM()->mkNode(kind::NOT, *this);
- }
+NodeTemplate<true> NodeTemplate<ref_count>::notNode() const {
+ return NodeManager::currentNM()->mkNode(kind::NOT, *this);
+}
template<bool ref_count>
- NodeTemplate<true> NodeTemplate<ref_count>::andNode(const NodeTemplate<
- ref_count>& right) const {
- return NodeManager::currentNM()->mkNode(kind::AND, *this, right);
- }
+NodeTemplate<true> NodeTemplate<ref_count>::andNode(const NodeTemplate<
+ ref_count>& right) const {
+ return NodeManager::currentNM()->mkNode(kind::AND, *this, right);
+}
template<bool ref_count>
- NodeTemplate<true> NodeTemplate<ref_count>::orNode(const NodeTemplate<
- ref_count>& right) const {
- return NodeManager::currentNM()->mkNode(kind::OR, *this, right);
- }
+NodeTemplate<true> NodeTemplate<ref_count>::orNode(const NodeTemplate<
+ ref_count>& right) const {
+ return NodeManager::currentNM()->mkNode(kind::OR, *this, right);
+}
template<bool ref_count>
- NodeTemplate<true> NodeTemplate<ref_count>::iteNode(const NodeTemplate<
- ref_count>& thenpart, const NodeTemplate<ref_count>& elsepart) const {
- return NodeManager::currentNM()->mkNode(kind::ITE, *this, thenpart, elsepart);
- }
+NodeTemplate<true> NodeTemplate<ref_count>::iteNode(const NodeTemplate<
+ ref_count>& thenpart, const NodeTemplate<ref_count>& elsepart) const {
+ return NodeManager::currentNM()->mkNode(kind::ITE, *this, thenpart, elsepart);
+}
template<bool ref_count>
- NodeTemplate<true> NodeTemplate<ref_count>::iffNode(const NodeTemplate<
- ref_count>& right) const {
- return NodeManager::currentNM()->mkNode(kind::IFF, *this, right);
- }
+NodeTemplate<true> NodeTemplate<ref_count>::iffNode(const NodeTemplate<
+ ref_count>& right) const {
+ return NodeManager::currentNM()->mkNode(kind::IFF, *this, right);
+}
template<bool ref_count>
- NodeTemplate<true> NodeTemplate<ref_count>::impNode(const NodeTemplate<
- ref_count>& right) const {
- return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right);
- }
+NodeTemplate<true> NodeTemplate<ref_count>::impNode(const NodeTemplate<
+ ref_count>& right) const {
+ return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right);
+}
template<bool ref_count>
- NodeTemplate<true> NodeTemplate<ref_count>::xorNode(const NodeTemplate<
- ref_count>& right) const {
- return NodeManager::currentNM()->mkNode(kind::XOR, *this, right);
- }
+NodeTemplate<true> NodeTemplate<ref_count>::xorNode(const NodeTemplate<
+ ref_count>& right) const {
+ return NodeManager::currentNM()->mkNode(kind::XOR, *this, right);
+}
template<bool ref_count>
- void NodeTemplate<ref_count>::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<ref_count>::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<bool ref_count>
- const Type* NodeTemplate<ref_count>::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 <bool ref_count>
+NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const {
+ switch(Kind k = getKind()) {
+ case kind::APPLY:
+ /* The operator is the first child. */
+ return NodeTemplate<true>(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<true> 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 ref_count>
+bool NodeTemplate<ref_count>::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<bool ref_count>
+const Type* NodeTemplate<ref_count>::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
Warning().flush();
}
-
}/* CVC4 namespace */
#endif /* __CVC4__NODE_H */
// 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 <unsigned N>
- bool nvIsAllocated(const NodeBuilder<N>& nb) {
+ bool nvIsAllocated(const NodeBuilder<N>& nb) const {
return nb.d_nv->d_nchildren > N;
}
- bool evNeedsToBeAllocated() {
+ bool evNeedsToBeAllocated() const {
return d_nv->d_nchildren == d_size;
}
}
// 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();
template <unsigned N> inline NodeBuilder(const NodeBuilder<N>& nb);
inline NodeBuilder(NodeManager* nm);
inline NodeBuilder(NodeManager* nm, Kind k);
- inline ~NodeBuilder();
+ inline ~NodeBuilder() throw();
- typedef NodeValue::iterator<true> iterator;
- typedef NodeValue::iterator<true> const_iterator;
+ typedef expr::NodeValue::iterator<true> iterator;
+ typedef expr::NodeValue::iterator<true> 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<true>();
}
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<true>();
}
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;
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<Node>& 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;
template <class Iterator>
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 <unsigned N> friend class NodeBuilder;
};/* class NodeBuilder */
+// TODO: add templatized NodeTemplate<ref_count> 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 <bool rc>
+ inline AndNodeBuilder& operator&&(const NodeTemplate<rc>&);
- operator NodeBuilder<>() { return d_eb; }
+ template <bool rc>
+ inline OrNodeBuilder operator||(const NodeTemplate<rc>&);
+
+ 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 <bool rc>
+ inline AndNodeBuilder operator&&(const NodeTemplate<rc>&);
+
+ template <bool rc>
+ inline OrNodeBuilder& operator||(const NodeTemplate<rc>&);
- 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 <bool rc>
+ inline PlusNodeBuilder& operator+(const NodeTemplate<rc>&);
+
+ template <bool rc>
+ inline PlusNodeBuilder& operator-(const NodeTemplate<rc>&);
+
+ template <bool rc>
+ inline MultNodeBuilder operator*(const NodeTemplate<rc>&);
- 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 <bool rc>
+ inline PlusNodeBuilder operator+(const NodeTemplate<rc>&);
- operator NodeBuilder<>() { return d_eb; }
+ template <bool rc>
+ inline PlusNodeBuilder operator-(const NodeTemplate<rc>&);
+
+ template <bool rc>
+ inline MultNodeBuilder& operator*(const NodeTemplate<rc>&);
+
+ inline operator NodeBuilder<>() { return d_eb; }
+ inline operator Node() { return d_eb; }
};/* class MultNodeBuilder */
template <unsigned nchild_thresh>
-inline AndNodeBuilder NodeBuilder<nchild_thresh>::operator&&(Node e) {
- return AndNodeBuilder(*this) && e;
+inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator&=(TNode e) {
+ return collapseTo(kind::AND).append(e);
}
template <unsigned nchild_thresh>
-inline OrNodeBuilder NodeBuilder<nchild_thresh>::operator||(Node e) {
- return OrNodeBuilder(*this) || e;
+inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator|=(TNode e) {
+ return collapseTo(kind::OR).append(e);
}
template <unsigned nchild_thresh>
-inline PlusNodeBuilder NodeBuilder<nchild_thresh>::operator+ (Node e) {
- return PlusNodeBuilder(*this) + e;
+inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator+=(TNode e) {
+ return collapseTo(kind::PLUS).append(e);
}
template <unsigned nchild_thresh>
-inline PlusNodeBuilder NodeBuilder<nchild_thresh>::operator- (Node e) {
- return PlusNodeBuilder(*this) - e;
+inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator-=(TNode e) {
+ return collapseTo(kind::PLUS).append(NodeManager::currentNM()->mkNode(kind::UMINUS, e));
}
template <unsigned nchild_thresh>
-inline MultNodeBuilder NodeBuilder<nchild_thresh>::operator* (Node e) {
- return MultNodeBuilder(*this) * e;
+inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator*=(TNode e) {
+ return collapseTo(kind::MULT).append(e);
}
-inline AndNodeBuilder& AndNodeBuilder::operator&&(Node e) {
- d_eb.append(e);
+template <bool rc>
+inline AndNodeBuilder& AndNodeBuilder::operator&&(const NodeTemplate<rc>& 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 <bool rc>
+inline OrNodeBuilder AndNodeBuilder::operator||(const NodeTemplate<rc>& 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 <bool rc>
+inline AndNodeBuilder OrNodeBuilder::operator&&(const NodeTemplate<rc>& n) {
+ return AndNodeBuilder(Node(d_eb), n);
+}
+
+template <bool rc>
+inline OrNodeBuilder& OrNodeBuilder::operator||(const NodeTemplate<rc>& 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 <bool rc>
+inline PlusNodeBuilder& PlusNodeBuilder::operator+(const NodeTemplate<rc>& n) {
+ d_eb.append(n);
return *this;
}
-inline PlusNodeBuilder& PlusNodeBuilder::operator+(Node e) {
- d_eb.append(e);
+template <bool rc>
+inline PlusNodeBuilder& PlusNodeBuilder::operator-(const NodeTemplate<rc>& n) {
+ d_eb.append(NodeManager::currentNM()->mkNode(kind::UMINUS, n));
return *this;
}
+template <bool rc>
+inline MultNodeBuilder PlusNodeBuilder::operator*(const NodeTemplate<rc>& 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 <bool rc>
+inline PlusNodeBuilder MultNodeBuilder::operator+(const NodeTemplate<rc>& n) {
+ return PlusNodeBuilder(Node(d_eb), n);
+}
+
+template <bool rc>
+inline PlusNodeBuilder MultNodeBuilder::operator-(const NodeTemplate<rc>& n) {
+ return PlusNodeBuilder(Node(d_eb), n);
+}
+
+template <bool rc>
+inline MultNodeBuilder& MultNodeBuilder::operator*(const NodeTemplate<rc>& 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 <bool rc1, bool rc2>
+inline AndNodeBuilder operator&&(const NodeTemplate<rc1>& a, const NodeTemplate<rc2>& 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 <bool rc1, bool rc2>
+inline OrNodeBuilder operator||(const NodeTemplate<rc1>& a, const NodeTemplate<rc2>& 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 <bool rc1, bool rc2>
+inline PlusNodeBuilder operator+(const NodeTemplate<rc1>& a, const NodeTemplate<rc2>& b) {
+ return PlusNodeBuilder(a, b);
}
-inline MultNodeBuilder& MultNodeBuilder::operator*(Node e) {
- d_eb.append(e);
- return *this;
+template <bool rc1, bool rc2>
+inline PlusNodeBuilder operator-(const NodeTemplate<rc1>& a, const NodeTemplate<rc2>& b) {
+ return PlusNodeBuilder(a, NodeManager::currentNM()->mkNode(kind::UMINUS, b));
+}
+
+template <bool rc1, bool rc2>
+inline MultNodeBuilder operator*(const NodeTemplate<rc1>& a, const NodeTemplate<rc2>& b) {
+ return MultNodeBuilder(a, b);
+}
+
+template <bool rc>
+inline AndNodeBuilder operator&&(const NodeTemplate<rc>& a, const AndNodeBuilder& b) {
+ return a && Node(b.d_eb);
+}
+
+template <bool rc>
+inline AndNodeBuilder operator&&(const NodeTemplate<rc>& a, const OrNodeBuilder& b) {
+ return a && Node(b.d_eb);
+}
+
+template <bool rc>
+inline OrNodeBuilder operator||(const NodeTemplate<rc>& a, const AndNodeBuilder& b) {
+ return a || Node(b.d_eb);
+}
+
+template <bool rc>
+inline OrNodeBuilder operator||(const NodeTemplate<rc>& a, const OrNodeBuilder& b) {
+ return a || Node(b.d_eb);
}
}/* CVC4 namespace */
d_inlineNv(0),
d_childrenStorage() {
- //Message() << "kind " << k << std::endl;
d_inlineNv.d_kind = k;
}
}
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 <unsigned nchild_thresh>
}
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 <unsigned nchild_thresh>
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 <unsigned nchild_thresh>
d_inlineNv(0),
d_childrenStorage() {
- //Message() << "kind " << k << std::endl;
d_inlineNv.d_kind = k;
}
template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>::~NodeBuilder() {
+inline NodeBuilder<nchild_thresh>::~NodeBuilder() throw() {
if(!d_used) {
// Warning("NodeBuilder unused at destruction\n");
// Commented above, as it happens a lot, for example with exceptions
template <unsigned nchild_thresh>
void NodeBuilder<nchild_thresh>::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;
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;
}
template <unsigned nchild_thresh>
-inline void NodeBuilder<nchild_thresh>::dealloc() {
+inline void NodeBuilder<nchild_thresh>::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();
}
}
+template <unsigned nchild_thresh>
+NodeBuilder<nchild_thresh>::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 <unsigned nchild_thresh>
NodeBuilder<nchild_thresh>::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;
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
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;
}
// 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,
// Make the new expression
d_nm->poolInsert(ev);
- Node n(ev);
- Debug("prop") << "result: " << n << std::endl;
- return n;
+ return Node(ev);
}
template <unsigned nchild_thresh>
#include "expr/kind.h"
#include "expr/expr.h"
-namespace __gnu_cxx {
- template<>
- struct hash<CVC4::NodeValue*> {
- size_t operator()(const CVC4::NodeValue* nv) const {
- return (size_t)nv->hash();
- }
- };
-}/* __gnu_cxx namespace */
-
-
namespace CVC4 {
class Type;
template <unsigned> friend class CVC4::NodeBuilder;
- typedef __gnu_cxx::hash_set<NodeValue*, __gnu_cxx::hash<NodeValue*>, NodeValue::NodeValueEq> NodeValueSet;
+ typedef __gnu_cxx::hash_set<expr::NodeValue*, expr::NodeValueHashFcn,
+ expr::NodeValue::NodeValueEq> 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; }
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";
}
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);
}
using namespace std;
namespace CVC4 {
+namespace expr {
size_t NodeValue::next_id = 1;
}
}
+}/* CVC4::expr namespace */
}/* CVC4 namespace */
NodeValue(int);
/** Destructor decrements the ref counts of its children */
- ~NodeValue();
+ ~NodeValue() throw();
typedef NodeValue** nv_iterator;
typedef NodeValue const* const* const_nv_iterator;
}
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;
}
static inline unsigned kindToDKind(Kind k) {
return ((unsigned) k) & kindMask;
}
+
static inline Kind dKindToKind(unsigned d) {
return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d);
}
d_nchildren(0) {
}
-inline NodeValue::~NodeValue() {
+inline NodeValue::~NodeValue() throw() {
for(nv_iterator i = nv_begin(); i != nv_end(); ++i) {
(*i)->dec();
}
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 */
#include <ext/hash_map>
-namespace __gnu_cxx {
-template<>
- struct hash<std::string> {
- size_t operator()(const std::string& str) const {
- return hash<const char*>()(str.c_str());
- }
- };
-}/* __gnu_cxx namespace */
-
namespace CVC4 {
namespace parser {
+struct StringHashFcn {
+ size_t operator()(const std::string& str) const {
+ return __gnu_cxx::hash<const char*>()(str.c_str());
+ }
+};
+
/**
* Generic symbol table for looking up variables by name.
*/
private:
/** The name to expression bindings */
- typedef __gnu_cxx::hash_map<std::string, ObjectType>
+ typedef __gnu_cxx::hash_map<std::string, ObjectType, StringHashFcn>
LookupTable;
-/*
- typedef __gnu_cxx::hash_map<std::string, std::stack<ObjectType> >
- LookupTable;
-*/
+
/** The table iterator */
typedef typename LookupTable::iterator table_iterator;
/** The table iterator */
SatSolver *d_satSolver;
/** Cache of what literal have been registered to a node. */
- __gnu_cxx::hash_map<Node, SatLiteral> d_translationCache;
+ __gnu_cxx::hash_map<Node, SatLiteral, NodeHashFcn> d_translationCache;
protected:
#include "cvc4_config.h"
#include "config.h"
+#include <cassert>
+
namespace CVC4 {
class CVC4_PUBLIC AssertionException : public Exception {
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...) \
#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 */
#include <cxxtest/TestSuite.h>
-//Used in some of the tests
#include <vector>
#include <limits.h>
#include <sstream>
/**
* Tests just constructors. No modification is done to the node.
*/
- void testNodeConstructors(){
+ void testNodeConstructors() {
//inline NodeBuilder();
//inline NodeBuilder(Kind k);
}
- void testDestructor(){
+ void testDestructor() {
//inline ~NodeBuilder();
NodeBuilder<K>* nb = new NodeBuilder<K>();
delete nb;
//Not sure what to test other than survival
}
- void testBeginEnd(){
+ void testBeginEnd() {
/* Test begin and ends without resizing */
NodeBuilder<K> ws;
TS_ASSERT_EQUALS(ws.begin(), ws.end());
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();
}
}
- void testGetKind(){
+ void testGetKind() {
/* Kind getKind() const; */
NodeBuilder<> noKind;
TS_ASSERT_EQUALS(noKind.getKind(), UNDEFINED_KIND);
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;
#endif
}
- void testOperatorSquare(){
+ void testOperatorSquare() {
/*
Node operator[](int i) const {
Assert(i >= 0 && i < d_ev->getNumChildren());
#endif
}
- void testClear(){
+ void testClear() {
/* void clear(Kind k = UNDEFINED_KIND); */
NodeBuilder<> nb;
}
- void testStreamInsertionKind(){
+ void testStreamInsertionKind() {
/* NodeBuilder& operator<<(const Kind& k); */
#ifdef CVC4_DEBUG
specKind);
}
- void testStreamInsertionNode(){
+ void testStreamInsertionNode() {
/* NodeBuilder& operator<<(const Node& n); */
NodeBuilder<K> nb(specKind);
TS_ASSERT_EQUALS(nb.getKind(), specKind);
}
- void testAppend(){
+ void testAppend() {
Node x = d_nm->mkVar();
Node y = d_nm->mkVar();
Node z = d_nm->mkVar();
TS_ASSERT(b[8] == m);
}
- void testOperatorNodeCast(){
+ void testOperatorNodeCast() {
/* operator Node();*/
NodeBuilder<K> implicit(specKind);
NodeBuilder<K> explic(specKind);
#endif
}
- void testToStream(){
+ void testToStream() {
/* inline void toStream(std::ostream& out) const {
d_ev->toStream(out);
}
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));
+ }
};
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<OutputChannelCallType, Node> > d_callHistory;
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<DummyTheory> {
public:
- vector<Node> d_registerSequence;
+ set<Node> d_registered;
vector<Node> d_getSequence;
DummyTheory(context::Context* ctxt, OutputChannel& out) :
TheoryImpl<DummyTheory>(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 {
public:
- TheoryBlack() { }
+ TheoryBlack() {}
void setUp() {
d_nm = new NodeManager();
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);
TS_ASSERT(d_dummy->doneWrapper());
}
- void testRegisterSequence(){
+ void testRegisterTerm() {
TS_ASSERT(d_dummy->doneWrapper());
Node x = d_nm->mkVar();
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);
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());
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() */
const OutputChannel& oc = d_dummy->getOutputChannel();
TS_ASSERT_EQUALS(&oc, &theOtherChannel);
-
}
-
};
projects / cvc5.git / commitdiff