1 /********************* */
4 ** Original author: mdeters
5 ** Major contributors: dejan
6 ** Minor contributors (to current version): taking, cconway
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Reference-counted encapsulation of a pointer to node information
16 ** Reference-counted encapsulation of a pointer to node information.
19 #include "cvc4_private.h"
21 // circular dependency
22 #include "expr/node_value.h"
24 #ifndef __CVC4__NODE_H
25 #define __CVC4__NODE_H
35 #include "expr/type.h"
36 #include "expr/kind.h"
37 #include "expr/metakind.h"
38 #include "expr/expr.h"
39 #include "util/Assert.h"
40 #include "util/configuration.h"
41 #include "util/output.h"
42 #include "util/exception.h"
43 #include "util/language.h"
44 #include "util/utility.h"
45 #include "util/hash.h"
55 }/* CVC4::expr::pickle namespace */
56 }/* CVC4::expr namespace */
58 template <bool ref_count
>
62 * Exception thrown during the type-checking phase, it can be
63 * thrown by node.getType().
65 class TypeCheckingExceptionPrivate
: public Exception
{
69 /** The node responsible for the failure */
70 NodeTemplate
<true>* d_node
;
74 TypeCheckingExceptionPrivate() throw() : Exception() {}
79 * Construct the exception with the problematic node and the message
80 * @param node the problematic node
81 * @param message the message explaining the failure
83 TypeCheckingExceptionPrivate(NodeTemplate
<false> node
, std::string message
) throw();
86 ~TypeCheckingExceptionPrivate() throw ();
89 * Get the Node that caused the type-checking to fail.
92 NodeTemplate
<true> getNode() const throw();
95 * Returns the message corresponding to the type-checking failure.
96 * We prefer toStream() to toString() because that keeps the expr-depth
97 * and expr-language settings present in the stream.
99 void toStream(std::ostream
& out
) const throw();
101 };/* class TypeCheckingExceptionPrivate */
104 * \typedef NodeTemplate<true> Node;
106 * The Node class encapsulates the NodeValue with reference counting.
108 * One should use generally use Nodes to manipulate expressions, to be safe.
109 * Every outstanding Node that references a NodeValue is counted in that
110 * NodeValue's reference count. Reference counts are maintained correctly
111 * on assignment of the Node object (to point to another NodeValue), and,
112 * upon destruction of the Node object, the NodeValue's reference count is
113 * decremented and, if zero, it becomes eligible for reclamation by the
116 typedef NodeTemplate
<true> Node
;
119 * \typedef NodeTemplate<false> TNode;
121 * The TNode class encapsulates the NodeValue but doesn't count references.
123 * TNodes are just like Nodes, but they don't update the reference count.
124 * Therefore, there is less overhead (copying a TNode is just the cost of
125 * the underlying pointer copy). Generally speaking, this is unsafe!
126 * However, there are certain situations where a TNode can be used safely.
128 * The largest class of uses for TNodes are when you need to use them in a
129 * "temporary," scoped fashion (hence the "T" in "TNode"). In general,
130 * it is safe to use TNode as a function parameter type, since the calling
131 * function (or some other function on the call stack) presumably has a Node
132 * reference to the expression data. It is generally _not_ safe, however,
133 * to return a TNode _from_ a function. (Functions that return Nodes often
134 * create the expression they return; such new expressions may not be
135 * referenced on the call stack, and have a reference count of 1 on
136 * creation. If this is returned as a TNode rather than a Node, the
137 * count drops to zero, marking the expression as eligible for reclamation.)
139 * More guidelines on when to use TNodes is available in the CVC4
141 * http://goedel.cims.nyu.edu/wiki/Developer%27s_Guide#Dealing_with_expressions_.28Nodes_and_TNodes.29
143 typedef NodeTemplate
<false> TNode
;
150 class AttributeManager
;
151 }/* CVC4::expr::attr namespace */
154 }/* CVC4::expr namespace */
158 struct NodeValueConstPrinter
;
159 }/* CVC4::kind::metakind namespace */
160 }/* CVC4::kind namespace */
163 * Encapsulation of an NodeValue pointer. The reference count is
164 * maintained in the NodeValue if ref_count is true.
165 * @param ref_count if true reference are counted in the NodeValue
167 template <bool ref_count
>
170 // for hash_maps, hash_sets..
171 template <bool ref_count1
>
172 struct HashFunction
{
173 size_t operator()(CVC4::NodeTemplate
<ref_count1
> node
) const {
174 return (size_t) node
.getId();
176 };/* struct HashFunction */
178 typedef HashFunction
<false> TNodeHashFunction
;
181 * The NodeValue has access to the private constructors, so that the
182 * iterators can can create new nodes.
184 friend class expr::NodeValue
;
186 friend class expr::pickle::PicklerPrivate
;
187 friend Node
expr::exportInternal(TNode n
, ExprManager
* from
, ExprManager
* to
, ExprManagerMapCollection
& vmap
);
189 /** A convenient null-valued encapsulated pointer */
190 static NodeTemplate s_null
;
192 /** The referenced NodeValue */
193 expr::NodeValue
* d_nv
;
196 * This constructor is reserved for use by the NodeTemplate package; one
197 * must construct an NodeTemplate using one of the build mechanisms of the
198 * NodeTemplate package.
200 * FIXME: there's a type-system escape here to cast away the const,
201 * since the refcount needs to be updated. But conceptually Nodes
202 * don't change their arguments, and it's nice to have
203 * const_iterators over them.
205 * This really does needs to be explicit to avoid hard to track errors with
206 * Nodes implicitly wrapping NodeValues
208 explicit NodeTemplate(const expr::NodeValue
*);
210 friend class NodeTemplate
<true>;
211 friend class NodeTemplate
<false>;
212 friend class TypeNode
;
213 friend class NodeManager
;
215 template <unsigned nchild_thresh
>
216 friend class NodeBuilder
;
218 friend class ::CVC4::expr::attr::AttributeManager
;
220 friend struct ::CVC4::kind::metakind::NodeValueConstPrinter
;
223 * Assigns the expression value and does reference counting. No assumptions
224 * are made on the expression, and should only be used if we know what we
227 * @param ev the expression value to assign
229 void assignNodeValue(expr::NodeValue
* ev
);
231 inline void assertTNodeNotExpired() const throw(AssertionException
) {
233 Assert( d_nv
->d_rc
> 0, "TNode pointing to an expired NodeValue" );
238 * Cache-aware, recursive version of substitute() used by the public
239 * member function with a similar signature.
241 Node
substitute(TNode node
, TNode replacement
,
242 std::hash_map
<TNode
, TNode
, TNodeHashFunction
>& cache
) const;
245 * Cache-aware, recursive version of substitute() used by the public
246 * member function with a similar signature.
248 template <class Iterator1
, class Iterator2
>
249 Node
substitute(Iterator1 nodesBegin
, Iterator1 nodesEnd
,
250 Iterator2 replacementsBegin
, Iterator2 replacementsEnd
,
251 std::hash_map
<TNode
, TNode
, TNodeHashFunction
>& cache
) const;
254 * Cache-aware, recursive version of substitute() used by the public
255 * member function with a similar signature.
257 template <class Iterator
>
258 Node
substitute(Iterator substitutionsBegin
, Iterator substitutionsEnd
,
259 std::hash_map
<TNode
, TNode
, TNodeHashFunction
>& cache
) const;
263 /** Default constructor, makes a null expression. */
264 NodeTemplate() : d_nv(&expr::NodeValue::s_null
) { }
267 * Conversion between nodes that are reference-counted and those that are
269 * @param node the node to make copy of
271 NodeTemplate(const NodeTemplate
<!ref_count
>& node
);
274 * Copy constructor. Note that GCC does NOT recognize an instantiation of
275 * the above template as a copy constructor and problems ensue. So we
276 * provide an explicit one here.
277 * @param node the node to make copy of
279 NodeTemplate(const NodeTemplate
& node
);
282 * Allow Exprs to become Nodes. This permits flexible translation of
283 * Exprs -> Nodes inside the CVC4 library without exposing a toNode()
284 * function in the public interface, or requiring lots of "friend"
287 NodeTemplate(const Expr
& e
);
290 * Assignment operator for nodes, copies the relevant information from node
292 * @param node the node to copy
293 * @return reference to this node
295 NodeTemplate
& operator=(const NodeTemplate
& node
);
298 * Assignment operator for nodes, copies the relevant information from node
300 * @param node the node to copy
301 * @return reference to this node
303 NodeTemplate
& operator=(const NodeTemplate
<!ref_count
>& node
);
306 * Destructor. If ref_count is true it will decrement the reference count
307 * and, if zero, collect the NodeValue.
309 ~NodeTemplate() throw(AssertionException
);
312 * Return the null node.
313 * @return the null node
315 static NodeTemplate
null() {
320 * Returns true if this expression is a null expression.
321 * @return true if null
323 bool isNull() const {
324 assertTNodeNotExpired();
325 return d_nv
== &expr::NodeValue::s_null
;
329 * Structural comparison operator for expressions.
330 * @param node the node to compare to
331 * @return true if expressions are equal, false otherwise
333 template <bool ref_count_1
>
334 bool operator==(const NodeTemplate
<ref_count_1
>& node
) const {
335 assertTNodeNotExpired();
336 node
.assertTNodeNotExpired();
337 return d_nv
== node
.d_nv
;
341 * Structural comparison operator for expressions.
342 * @param node the node to compare to
343 * @return false if expressions are equal, true otherwise
345 template <bool ref_count_1
>
346 bool operator!=(const NodeTemplate
<ref_count_1
>& node
) const {
347 assertTNodeNotExpired();
348 node
.assertTNodeNotExpired();
349 return d_nv
!= node
.d_nv
;
353 * We compare by expression ids so, keeping things deterministic and having
354 * that subexpressions have to be smaller than the enclosing expressions.
355 * @param node the node to compare to
356 * @return true if this expression is smaller
358 template <bool ref_count_1
>
359 inline bool operator<(const NodeTemplate
<ref_count_1
>& node
) const {
360 assertTNodeNotExpired();
361 node
.assertTNodeNotExpired();
362 return d_nv
->d_id
< node
.d_nv
->d_id
;
366 * We compare by expression ids so, keeping things deterministic and having
367 * that subexpressions have to be smaller than the enclosing expressions.
368 * @param node the node to compare to
369 * @return true if this expression is greater
371 template <bool ref_count_1
>
372 inline bool operator>(const NodeTemplate
<ref_count_1
>& node
) const {
373 assertTNodeNotExpired();
374 node
.assertTNodeNotExpired();
375 return d_nv
->d_id
> node
.d_nv
->d_id
;
379 * We compare by expression ids so, keeping things deterministic and having
380 * that subexpressions have to be smaller than the enclosing expressions.
381 * @param node the node to compare to
382 * @return true if this expression is smaller than or equal to
384 template <bool ref_count_1
>
385 inline bool operator<=(const NodeTemplate
<ref_count_1
>& node
) const {
386 assertTNodeNotExpired();
387 node
.assertTNodeNotExpired();
388 return d_nv
->d_id
<= node
.d_nv
->d_id
;
392 * We compare by expression ids so, keeping things deterministic and having
393 * that subexpressions have to be smaller than the enclosing expressions.
394 * @param node the node to compare to
395 * @return true if this expression is greater than or equal to
397 template <bool ref_count_1
>
398 inline bool operator>=(const NodeTemplate
<ref_count_1
>& node
) const {
399 assertTNodeNotExpired();
400 node
.assertTNodeNotExpired();
401 return d_nv
->d_id
>= node
.d_nv
->d_id
;
405 * Returns the i-th child of this node.
406 * @param i the index of the child
407 * @return the node representing the i-th child
409 NodeTemplate
operator[](int i
) const {
410 assertTNodeNotExpired();
411 return NodeTemplate(d_nv
->getChild(i
));
414 /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
416 * It has been decided for now to hold off on implementations of
417 * these functions, as they may only be needed in CNF conversion,
418 * where it's pointless to do a lazy isAtomic determination by
419 * searching through the DAG, and storing it, since the result will
420 * only be used once. For more details see the 4/27/2010 CVC4
421 * developer's meeting notes at:
423 * http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
425 // bool containsDecision(); // is "atomic"
426 // bool properlyContainsDecision(); // maybe not atomic but all children are
429 * Convert this Node into an Expr using the currently-in-scope
430 * manager. Essentially this is like an "operator Expr()" but we
431 * don't want it to compete with implicit conversions between e.g.
432 * Node and TNode, and we want internal-to-external interface
433 * (Node -> Expr) points to be explicit. We could write an
434 * explicit Expr(Node) constructor---but that dirties the public
437 inline Expr
toExpr();
440 * Convert an Expr into a Node.
442 static inline Node
fromExpr(const Expr
& e
);
445 * Returns true if this node represents a constant
446 * @return true if const
448 inline bool isConst() const {
449 assertTNodeNotExpired();
450 return getMetaKind() == kind::metakind::CONSTANT
;
454 * Returns the unique id of this node
457 unsigned getId() const {
458 assertTNodeNotExpired();
459 return d_nv
->getId();
463 * Returns a node representing the operator of this expression.
464 * If this is an APPLY, then the operator will be a functional term.
465 * Otherwise, it will be a node with kind BUILTIN.
467 NodeTemplate
<true> getOperator() const;
470 * Returns true if the node has an operator (i.e., it's not a
471 * variable or a constant).
473 inline bool hasOperator() const;
476 * Get the type for the node and optionally do type checking.
478 * Initial type computation will be near-constant time if
479 * type checking is not requested. Results are memoized, so that
480 * subsequent calls to getType() without type checking will be
483 * Initial type checking is linear in the size of the expression.
484 * Again, the results are memoized, so that subsequent calls to
485 * getType(), with or without type checking, will be constant
488 * NOTE: A TypeCheckingException can be thrown even when type
489 * checking is not requested. getType() will always return a
490 * valid and correct type and, thus, an exception will be thrown
491 * when no valid or correct type can be computed (e.g., if the
492 * arguments to a bit-vector operation aren't bit-vectors). When
493 * type checking is not requested, getType() will do the minimum
494 * amount of checking required to return a valid result.
496 * @param check whether we should check the type as we compute it
499 TypeNode
getType(bool check
= false) const
500 throw (CVC4::TypeCheckingExceptionPrivate
, CVC4::AssertionException
);
503 * Substitution of Nodes.
505 Node
substitute(TNode node
, TNode replacement
) const;
508 * Simultaneous substitution of Nodes. Elements in the Iterator1
509 * range will be replaced by their corresponding element in the
510 * Iterator2 range. Both ranges should have the same size.
512 template <class Iterator1
, class Iterator2
>
513 Node
substitute(Iterator1 nodesBegin
,
515 Iterator2 replacementsBegin
,
516 Iterator2 replacementsEnd
) const;
519 * Simultaneous substitution of Nodes. Iterators should be over
520 * pairs (x,y) for the rewrites [x->y].
522 template <class Iterator
>
523 Node
substitute(Iterator substitutionsBegin
,
524 Iterator substitutionsEnd
) const;
527 * Returns the kind of this node.
530 inline Kind
getKind() const {
531 assertTNodeNotExpired();
532 return Kind(d_nv
->d_kind
);
536 * Returns the metakind of this node.
537 * @return the metakind
539 inline kind::MetaKind
getMetaKind() const {
540 assertTNodeNotExpired();
541 return kind::metaKindOf(getKind());
545 * Returns the number of children this node has.
546 * @return the number of children
548 inline size_t getNumChildren() const;
551 * If this is a CONST_* Node, extract the constant from it.
554 inline const T
& getConst() const;
557 * Returns the value of the given attribute that this has been attached.
558 * @param attKind the kind of the attribute
559 * @return the value of the attribute
561 template <class AttrKind
>
562 inline typename
AttrKind::value_type
getAttribute(const AttrKind
& attKind
) const;
564 // Note that there are two, distinct hasAttribute() declarations for
565 // a reason (rather than using a pointer-valued argument with a
566 // default value): they permit more optimized code in the underlying
567 // hasAttribute() implementations.
570 * Returns true if this node has been associated an attribute of given kind.
571 * Additionaly, if a pointer to the value_kind is give, and the attribute
572 * value has been set for this node, it will be returned.
573 * @param attKind the kind of the attribute
574 * @return true if this node has the requested attribute
576 template <class AttrKind
>
577 inline bool hasAttribute(const AttrKind
& attKind
) const;
580 * Returns true if this node has been associated an attribute of given kind.
581 * Additionaly, if a pointer to the value_kind is give, and the attribute
582 * value has been set for this node, it will be returned.
583 * @param attKind the kind of the attribute
584 * @param value where to store the value if it exists
585 * @return true if this node has the requested attribute
587 template <class AttrKind
>
588 inline bool getAttribute(const AttrKind
& attKind
,
589 typename
AttrKind::value_type
& value
) const;
592 * Sets the given attribute of this node to the given value.
593 * @param attKind the kind of the atribute
594 * @param value the value to set the attribute to
596 template <class AttrKind
>
597 inline void setAttribute(const AttrKind
& attKind
,
598 const typename
AttrKind::value_type
& value
);
600 /** Iterator allowing for scanning through the children. */
601 typedef typename
expr::NodeValue::iterator
< NodeTemplate
<ref_count
> > iterator
;
602 /** Constant iterator allowing for scanning through the children. */
603 typedef typename
expr::NodeValue::iterator
< NodeTemplate
<ref_count
> > const_iterator
;
605 class kinded_iterator
{
606 friend class NodeTemplate
<ref_count
>;
608 NodeTemplate
<ref_count
> d_node
;
611 kinded_iterator(TNode node
, ssize_t child
) :
616 // These are factories to serve as clients to Node::begin<K>() and
618 static kinded_iterator
begin(TNode n
, Kind k
) {
619 return kinded_iterator(n
, n
.getKind() == k
? 0 : -2);
621 static kinded_iterator
end(TNode n
, Kind k
) {
622 return kinded_iterator(n
, n
.getKind() == k
? n
.getNumChildren() : -1);
626 typedef NodeTemplate
<ref_count
> value_type
;
627 typedef std::ptrdiff_t difference_type
;
628 typedef NodeTemplate
<ref_count
>* pointer
;
629 typedef NodeTemplate
<ref_count
>& reference
;
632 d_node(NodeTemplate
<ref_count
>::null()),
636 kinded_iterator(const kinded_iterator
& i
) :
641 NodeTemplate
<ref_count
> operator*() {
642 return d_child
< 0 ? d_node
: d_node
[d_child
];
645 bool operator==(const kinded_iterator
& i
) {
646 return d_node
== i
.d_node
&& d_child
== i
.d_child
;
649 bool operator!=(const kinded_iterator
& i
) {
650 return !(*this == i
);
653 kinded_iterator
& operator++() {
660 kinded_iterator
operator++(int) {
661 kinded_iterator i
= *this;
665 };/* class NodeTemplate<ref_count>::kinded_iterator */
667 typedef kinded_iterator const_kinded_iterator
;
670 * Returns the iterator pointing to the first child.
671 * @return the iterator
673 inline iterator
begin() {
674 assertTNodeNotExpired();
675 return d_nv
->begin
< NodeTemplate
<ref_count
> >();
679 * Returns the iterator pointing to the end of the children (one beyond the
681 * @return the end of the children iterator.
683 inline iterator
end() {
684 assertTNodeNotExpired();
685 return d_nv
->end
< NodeTemplate
<ref_count
> >();
689 * Returns the iterator pointing to the first child, if the node's
690 * kind is the same as the parameter, otherwise returns the iterator
691 * pointing to the node itself. This is useful if you want to
692 * pretend to iterate over a "unary" PLUS, for instance, since unary
693 * PLUSes don't exist---begin(PLUS) will give an iterator over the
694 * children if the node's a PLUS node, otherwise give an iterator
695 * over the node itself, as if it were a unary PLUS.
696 * @param kind the kind to match
697 * @return the kinded_iterator iterating over this Node (if its kind
698 * is not the passed kind) or its children
700 inline kinded_iterator
begin(Kind kind
) {
701 assertTNodeNotExpired();
702 return kinded_iterator::begin(*this, kind
);
706 * Returns the iterator pointing to the end of the children (one
707 * beyond the last one), if the node's kind is the same as the
708 * parameter, otherwise returns the iterator pointing to the
709 * one-of-the-node-itself. This is useful if you want to pretend to
710 * iterate over a "unary" PLUS, for instance, since unary PLUSes
711 * don't exist---begin(PLUS) will give an iterator over the children
712 * if the node's a PLUS node, otherwise give an iterator over the
713 * node itself, as if it were a unary PLUS.
714 * @param kind the kind to match
715 * @return the kinded_iterator pointing off-the-end of this Node (if
716 * its kind is not the passed kind) or off-the-end of its children
718 inline kinded_iterator
end(Kind kind
) {
719 assertTNodeNotExpired();
720 return kinded_iterator::end(*this, kind
);
724 * Returns the const_iterator pointing to the first child.
725 * @return the const_iterator
727 inline const_iterator
begin() const {
728 assertTNodeNotExpired();
729 return d_nv
->begin
< NodeTemplate
<ref_count
> >();
733 * Returns the const_iterator pointing to the end of the children (one
734 * beyond the last one.
735 * @return the end of the children const_iterator.
737 inline const_iterator
end() const {
738 assertTNodeNotExpired();
739 return d_nv
->end
< NodeTemplate
<ref_count
> >();
743 * Returns the iterator pointing to the first child, if the node's
744 * kind is the same as the parameter, otherwise returns the iterator
745 * pointing to the node itself. This is useful if you want to
746 * pretend to iterate over a "unary" PLUS, for instance, since unary
747 * PLUSes don't exist---begin(PLUS) will give an iterator over the
748 * children if the node's a PLUS node, otherwise give an iterator
749 * over the node itself, as if it were a unary PLUS.
750 * @param kind the kind to match
751 * @return the kinded_iterator iterating over this Node (if its kind
752 * is not the passed kind) or its children
754 inline const_kinded_iterator
begin(Kind kind
) const {
755 assertTNodeNotExpired();
756 return const_kinded_iterator::begin(*this, kind
);
760 * Returns the iterator pointing to the end of the children (one
761 * beyond the last one), if the node's kind is the same as the
762 * parameter, otherwise returns the iterator pointing to the
763 * one-of-the-node-itself. This is useful if you want to pretend to
764 * iterate over a "unary" PLUS, for instance, since unary PLUSes
765 * don't exist---begin(PLUS) will give an iterator over the children
766 * if the node's a PLUS node, otherwise give an iterator over the
767 * node itself, as if it were a unary PLUS.
768 * @param kind the kind to match
769 * @return the kinded_iterator pointing off-the-end of this Node (if
770 * its kind is not the passed kind) or off-the-end of its children
772 inline const_kinded_iterator
end(Kind kind
) const {
773 assertTNodeNotExpired();
774 return const_kinded_iterator::end(*this, kind
);
778 * Converts this node into a string representation.
779 * @return the string representation of this node.
781 inline std::string
toString() const {
782 assertTNodeNotExpired();
783 return d_nv
->toString();
787 * Converts this node into a string representation and sends it to the
790 * @param out the stream to serialize this node to
791 * @param toDepth the depth to which to print this expression, or -1 to
793 * @param types set to true to ascribe types to the output expressions
794 * (might break language compliance, but good for debugging expressions)
795 * @param language the language in which to output
797 inline void toStream(std::ostream
& out
, int toDepth
= -1, bool types
= false,
798 OutputLanguage language
= language::output::LANG_AST
) const {
799 assertTNodeNotExpired();
800 d_nv
->toStream(out
, toDepth
, types
, language
);
804 * IOStream manipulator to set the maximum depth of Nodes when
805 * pretty-printing. -1 means print to any depth. E.g.:
807 * // let a, b, c, and d be VARIABLEs
808 * Node n = nm->mkNode(OR, a, b, nm->mkNode(AND, c, nm->mkNode(NOT, d)))
809 * out << setdepth(3) << n;
811 * gives "(OR a b (AND c (NOT d)))", but
813 * out << setdepth(1) << [same node as above]
815 * gives "(OR a b (...))"
817 typedef expr::ExprSetDepth setdepth
;
820 * IOStream manipulator to print type ascriptions or not.
822 * // let a, b, c, and d be variables of sort U
823 * Node n = nm->mkNode(OR, a, b, nm->mkNode(AND, c, nm->mkNode(NOT, d)))
826 * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
828 typedef expr::ExprPrintTypes printtypes
;
831 * IOStream manipulator to set the output language for Exprs.
833 typedef expr::ExprSetLanguage setlanguage
;
836 * Very basic pretty printer for Node.
837 * @param out output stream to print to.
838 * @param indent number of spaces to indent the formula by.
840 inline void printAst(std::ostream
& out
, int indent
= 0) const;
843 * Check if the node has a subterm t.
845 inline bool hasSubterm(NodeTemplate
<false> t
, bool strict
= false) const;
847 template <bool ref_count2
>
848 NodeTemplate
<true> eqNode(const NodeTemplate
<ref_count2
>& right
) const;
850 NodeTemplate
<true> notNode() const;
851 NodeTemplate
<true> negate() const;
852 template <bool ref_count2
>
853 NodeTemplate
<true> andNode(const NodeTemplate
<ref_count2
>& right
) const;
854 template <bool ref_count2
>
855 NodeTemplate
<true> orNode(const NodeTemplate
<ref_count2
>& right
) const;
856 template <bool ref_count2
, bool ref_count3
>
857 NodeTemplate
<true> iteNode(const NodeTemplate
<ref_count2
>& thenpart
,
858 const NodeTemplate
<ref_count3
>& elsepart
) const;
859 template <bool ref_count2
>
860 NodeTemplate
<true> iffNode(const NodeTemplate
<ref_count2
>& right
) const;
861 template <bool ref_count2
>
862 NodeTemplate
<true> impNode(const NodeTemplate
<ref_count2
>& right
) const;
863 template <bool ref_count2
>
864 NodeTemplate
<true> xorNode(const NodeTemplate
<ref_count2
>& right
) const;
866 };/* class NodeTemplate<ref_count> */
869 * Serializes a given node to the given stream.
871 * @param out the output stream to use
872 * @param n the node to output to the stream
875 inline std::ostream
& operator<<(std::ostream
& out
, TNode n
) {
877 Node::setdepth::getDepth(out
),
878 Node::printtypes::getPrintTypes(out
),
879 Node::setlanguage::getLanguage(out
));
883 }/* CVC4 namespace */
885 #include <ext/hash_map>
887 #include "expr/attribute.h"
888 #include "expr/node_manager.h"
892 // for hash_maps, hash_sets..
893 struct NodeHashFunction
{
894 size_t operator()(CVC4::Node node
) const {
895 return (size_t) node
.getId();
897 };/* struct NodeHashFunction */
899 // for hash_maps, hash_sets..
900 struct TNodeHashFunction
{
901 size_t operator()(CVC4::TNode node
) const {
902 return (size_t) node
.getId();
904 };/* struct TNodeHashFunction */
906 struct TNodePairHashFunction
{
907 size_t operator()(const std::pair
<CVC4::TNode
, CVC4::TNode
>& pair
) const {
908 TNode n1
= pair
.first
;
909 TNode n2
= pair
.second
;
911 return (size_t) (n1
.getId() * 0x9e3779b9 + n2
.getId());
913 };/* struct TNodePairHashFunction */
915 template <bool ref_count
>
916 inline size_t NodeTemplate
<ref_count
>::getNumChildren() const {
917 assertTNodeNotExpired();
918 return d_nv
->getNumChildren();
921 template <bool ref_count
>
923 inline const T
& NodeTemplate
<ref_count
>::getConst() const {
924 assertTNodeNotExpired();
925 return d_nv
->getConst
<T
>();
928 template <bool ref_count
>
929 template <class AttrKind
>
930 inline typename
AttrKind::value_type NodeTemplate
<ref_count
>::
931 getAttribute(const AttrKind
&) const {
932 Assert( NodeManager::currentNM() != NULL
,
933 "There is no current CVC4::NodeManager associated to this thread.\n"
934 "Perhaps a public-facing function is missing a NodeManagerScope ?" );
936 assertTNodeNotExpired();
938 return NodeManager::currentNM()->getAttribute(*this, AttrKind());
941 template <bool ref_count
>
942 template <class AttrKind
>
943 inline bool NodeTemplate
<ref_count
>::
944 hasAttribute(const AttrKind
&) const {
945 Assert( NodeManager::currentNM() != NULL
,
946 "There is no current CVC4::NodeManager associated to this thread.\n"
947 "Perhaps a public-facing function is missing a NodeManagerScope ?" );
949 assertTNodeNotExpired();
951 return NodeManager::currentNM()->hasAttribute(*this, AttrKind());
954 template <bool ref_count
>
955 template <class AttrKind
>
956 inline bool NodeTemplate
<ref_count
>::getAttribute(const AttrKind
&,
957 typename
AttrKind::value_type
& ret
) const {
958 Assert( NodeManager::currentNM() != NULL
,
959 "There is no current CVC4::NodeManager associated to this thread.\n"
960 "Perhaps a public-facing function is missing a NodeManagerScope ?" );
962 assertTNodeNotExpired();
964 return NodeManager::currentNM()->getAttribute(*this, AttrKind(), ret
);
967 template <bool ref_count
>
968 template <class AttrKind
>
969 inline void NodeTemplate
<ref_count
>::
970 setAttribute(const AttrKind
&, const typename
AttrKind::value_type
& value
) {
971 Assert( NodeManager::currentNM() != NULL
,
972 "There is no current CVC4::NodeManager associated to this thread.\n"
973 "Perhaps a public-facing function is missing a NodeManagerScope ?" );
975 assertTNodeNotExpired();
977 NodeManager::currentNM()->setAttribute(*this, AttrKind(), value
);
980 template <bool ref_count
>
981 NodeTemplate
<ref_count
> NodeTemplate
<ref_count
>::s_null(&expr::NodeValue::s_null
);
983 // FIXME: escape from type system convenient but is there a better
984 // way? Nodes conceptually don't change their expr values but of
985 // course they do modify the refcount. But it's nice to be able to
986 // support node_iterators over const NodeValue*. So.... hm.
987 template <bool ref_count
>
988 NodeTemplate
<ref_count
>::NodeTemplate(const expr::NodeValue
* ev
) :
989 d_nv(const_cast<expr::NodeValue
*> (ev
)) {
990 Assert(d_nv
!= NULL
, "Expecting a non-NULL expression value!");
994 Assert(d_nv
->d_rc
> 0, "TNode constructed from NodeValue with rc == 0");
998 // the code for these two following constructors ("conversion/copy
999 // constructors") is identical, but we need both. see comment in the
1002 template <bool ref_count
>
1003 NodeTemplate
<ref_count
>::NodeTemplate(const NodeTemplate
<!ref_count
>& e
) {
1004 Assert(e
.d_nv
!= NULL
, "Expecting a non-NULL expression value!");
1007 Assert(d_nv
->d_rc
> 0, "Node constructed from TNode with rc == 0");
1010 // shouldn't ever fail
1011 Assert(d_nv
->d_rc
> 0, "TNode constructed from Node with rc == 0");
1015 template <bool ref_count
>
1016 NodeTemplate
<ref_count
>::NodeTemplate(const NodeTemplate
& e
) {
1017 Assert(e
.d_nv
!= NULL
, "Expecting a non-NULL expression value!");
1020 // shouldn't ever fail
1021 Assert(d_nv
->d_rc
> 0, "Node constructed from Node with rc == 0");
1024 Assert(d_nv
->d_rc
> 0, "TNode constructed from TNode with rc == 0");
1028 template <bool ref_count
>
1029 NodeTemplate
<ref_count
>::NodeTemplate(const Expr
& e
) {
1030 Assert(e
.d_node
!= NULL
, "Expecting a non-NULL expression value!");
1031 Assert(e
.d_node
->d_nv
!= NULL
, "Expecting a non-NULL expression value!");
1032 d_nv
= e
.d_node
->d_nv
;
1033 // shouldn't ever fail
1034 Assert(d_nv
->d_rc
> 0, "Node constructed from Expr with rc == 0");
1040 template <bool ref_count
>
1041 NodeTemplate
<ref_count
>::~NodeTemplate() throw(AssertionException
) {
1042 Assert(d_nv
!= NULL
, "Expecting a non-NULL expression value!");
1044 // shouldn't ever fail
1045 Assert(d_nv
->d_rc
> 0, "Node reference count would be negative");
1050 template <bool ref_count
>
1051 void NodeTemplate
<ref_count
>::assignNodeValue(expr::NodeValue
* ev
) {
1056 Assert(d_nv
->d_rc
> 0, "TNode assigned to NodeValue with rc == 0");
1060 template <bool ref_count
>
1061 NodeTemplate
<ref_count
>& NodeTemplate
<ref_count
>::
1062 operator=(const NodeTemplate
& e
) {
1063 Assert(d_nv
!= NULL
, "Expecting a non-NULL expression value!");
1064 Assert(e
.d_nv
!= NULL
, "Expecting a non-NULL expression value on RHS!");
1065 if(EXPECT_TRUE( d_nv
!= e
.d_nv
)) {
1067 // shouldn't ever fail
1068 Assert(d_nv
->d_rc
> 0,
1069 "Node reference count would be negative");
1074 // shouldn't ever fail
1075 Assert(d_nv
->d_rc
> 0, "Node assigned from Node with rc == 0");
1078 Assert(d_nv
->d_rc
> 0, "TNode assigned from TNode with rc == 0");
1084 template <bool ref_count
>
1085 NodeTemplate
<ref_count
>& NodeTemplate
<ref_count
>::
1086 operator=(const NodeTemplate
<!ref_count
>& e
) {
1087 Assert(d_nv
!= NULL
, "Expecting a non-NULL expression value!");
1088 Assert(e
.d_nv
!= NULL
, "Expecting a non-NULL expression value on RHS!");
1089 if(EXPECT_TRUE( d_nv
!= e
.d_nv
)) {
1091 // shouldn't ever fail
1092 Assert(d_nv
->d_rc
> 0, "Node reference count would be negative");
1097 Assert(d_nv
->d_rc
> 0, "Node assigned from TNode with rc == 0");
1100 // shouldn't ever happen
1101 Assert(d_nv
->d_rc
> 0, "TNode assigned from Node with rc == 0");
1107 template <bool ref_count
>
1108 template <bool ref_count2
>
1110 NodeTemplate
<ref_count
>::eqNode(const NodeTemplate
<ref_count2
>& right
) const {
1111 assertTNodeNotExpired();
1112 return NodeManager::currentNM()->mkNode(kind::EQUAL
, *this, right
);
1115 template <bool ref_count
>
1116 NodeTemplate
<true> NodeTemplate
<ref_count
>::notNode() const {
1117 assertTNodeNotExpired();
1118 return NodeManager::currentNM()->mkNode(kind::NOT
, *this);
1121 template <bool ref_count
>
1122 NodeTemplate
<true> NodeTemplate
<ref_count
>::negate() const {
1123 assertTNodeNotExpired();
1124 return (getKind() == kind::NOT
) ? NodeTemplate
<true>(d_nv
->getChild(0)) : NodeManager::currentNM()->mkNode(kind::NOT
, *this);
1127 template <bool ref_count
>
1128 template <bool ref_count2
>
1130 NodeTemplate
<ref_count
>::andNode(const NodeTemplate
<ref_count2
>& right
) const {
1131 assertTNodeNotExpired();
1132 return NodeManager::currentNM()->mkNode(kind::AND
, *this, right
);
1135 template <bool ref_count
>
1136 template <bool ref_count2
>
1138 NodeTemplate
<ref_count
>::orNode(const NodeTemplate
<ref_count2
>& right
) const {
1139 assertTNodeNotExpired();
1140 return NodeManager::currentNM()->mkNode(kind::OR
, *this, right
);
1143 template <bool ref_count
>
1144 template <bool ref_count2
, bool ref_count3
>
1146 NodeTemplate
<ref_count
>::iteNode(const NodeTemplate
<ref_count2
>& thenpart
,
1147 const NodeTemplate
<ref_count3
>& elsepart
) const {
1148 assertTNodeNotExpired();
1149 return NodeManager::currentNM()->mkNode(kind::ITE
, *this, thenpart
, elsepart
);
1152 template <bool ref_count
>
1153 template <bool ref_count2
>
1155 NodeTemplate
<ref_count
>::iffNode(const NodeTemplate
<ref_count2
>& right
) const {
1156 assertTNodeNotExpired();
1157 return NodeManager::currentNM()->mkNode(kind::IFF
, *this, right
);
1160 template <bool ref_count
>
1161 template <bool ref_count2
>
1163 NodeTemplate
<ref_count
>::impNode(const NodeTemplate
<ref_count2
>& right
) const {
1164 assertTNodeNotExpired();
1165 return NodeManager::currentNM()->mkNode(kind::IMPLIES
, *this, right
);
1168 template <bool ref_count
>
1169 template <bool ref_count2
>
1171 NodeTemplate
<ref_count
>::xorNode(const NodeTemplate
<ref_count2
>& right
) const {
1172 assertTNodeNotExpired();
1173 return NodeManager::currentNM()->mkNode(kind::XOR
, *this, right
);
1176 template <bool ref_count
>
1178 NodeTemplate
<ref_count
>::printAst(std::ostream
& out
, int indent
) const {
1179 assertTNodeNotExpired();
1180 d_nv
->printAst(out
, indent
);
1184 * Returns a node representing the operator of this expression.
1185 * If this is an APPLY, then the operator will be a functional term.
1186 * Otherwise, it will be a node with kind BUILTIN.
1188 template <bool ref_count
>
1189 NodeTemplate
<true> NodeTemplate
<ref_count
>::getOperator() const {
1190 Assert( NodeManager::currentNM() != NULL
,
1191 "There is no current CVC4::NodeManager associated to this thread.\n"
1192 "Perhaps a public-facing function is missing a NodeManagerScope ?" );
1194 assertTNodeNotExpired();
1196 switch(kind::MetaKind mk
= getMetaKind()) {
1197 case kind::metakind::INVALID
:
1198 IllegalArgument(*this, "getOperator() called on Node with INVALID-kinded kind");
1200 case kind::metakind::VARIABLE
:
1201 IllegalArgument(*this, "getOperator() called on Node with VARIABLE-kinded kind");
1203 case kind::metakind::OPERATOR
: {
1204 /* Returns a BUILTIN node. */
1205 return NodeManager::currentNM()->operatorOf(getKind());
1208 case kind::metakind::PARAMETERIZED
:
1209 /* The operator is the first child. */
1210 return Node(d_nv
->d_children
[0]);
1212 case kind::metakind::CONSTANT
:
1213 IllegalArgument(*this, "getOperator() called on Node with CONSTANT-kinded kind");
1221 * Returns true if the node has an operator (i.e., it's not a variable
1224 template <bool ref_count
>
1225 inline bool NodeTemplate
<ref_count
>::hasOperator() const {
1226 assertTNodeNotExpired();
1227 return NodeManager::hasOperator(getKind());
1230 template <bool ref_count
>
1231 TypeNode NodeTemplate
<ref_count
>::getType(bool check
) const
1232 throw (CVC4::TypeCheckingExceptionPrivate
, CVC4::AssertionException
) {
1233 Assert( NodeManager::currentNM() != NULL
,
1234 "There is no current CVC4::NodeManager associated to this thread.\n"
1235 "Perhaps a public-facing function is missing a NodeManagerScope ?" );
1237 assertTNodeNotExpired();
1239 return NodeManager::currentNM()->getType(*this, check
);
1242 template <bool ref_count
>
1244 NodeTemplate
<ref_count
>::substitute(TNode node
, TNode replacement
) const {
1245 if (node
== *this) {
1248 std::hash_map
<TNode
, TNode
, TNodeHashFunction
> cache
;
1249 return substitute(node
, replacement
, cache
);
1252 template <bool ref_count
>
1254 NodeTemplate
<ref_count
>::substitute(TNode node
, TNode replacement
,
1255 std::hash_map
<TNode
, TNode
, TNodeHashFunction
>& cache
) const {
1256 Assert(node
!= *this);
1258 if (getNumChildren() == 0) {
1263 typename
std::hash_map
<TNode
, TNode
, TNodeHashFunction
>::const_iterator i
= cache
.find(*this);
1264 if(i
!= cache
.end()) {
1268 // otherwise compute
1269 NodeBuilder
<> nb(getKind());
1270 if(getMetaKind() == kind::metakind::PARAMETERIZED
) {
1271 // push the operator
1272 nb
<< getOperator();
1274 for(const_iterator i
= begin(),
1281 nb
<< (*i
).substitute(node
, replacement
, cache
);
1292 template <bool ref_count
>
1293 template <class Iterator1
, class Iterator2
>
1295 NodeTemplate
<ref_count
>::substitute(Iterator1 nodesBegin
,
1297 Iterator2 replacementsBegin
,
1298 Iterator2 replacementsEnd
) const {
1299 std::hash_map
<TNode
, TNode
, TNodeHashFunction
> cache
;
1300 return substitute(nodesBegin
, nodesEnd
,
1301 replacementsBegin
, replacementsEnd
, cache
);
1304 template <bool ref_count
>
1305 template <class Iterator1
, class Iterator2
>
1307 NodeTemplate
<ref_count
>::substitute(Iterator1 nodesBegin
,
1309 Iterator2 replacementsBegin
,
1310 Iterator2 replacementsEnd
,
1311 std::hash_map
<TNode
, TNode
, TNodeHashFunction
>& cache
) const {
1313 typename
std::hash_map
<TNode
, TNode
, TNodeHashFunction
>::const_iterator i
= cache
.find(*this);
1314 if(i
!= cache
.end()) {
1318 // otherwise compute
1319 Assert( std::distance(nodesBegin
, nodesEnd
) == std::distance(replacementsBegin
, replacementsEnd
),
1320 "Substitution iterator ranges must be equal size" );
1321 Iterator1 j
= find(nodesBegin
, nodesEnd
, TNode(*this));
1323 Iterator2 b
= replacementsBegin
;
1324 std::advance(b
, std::distance(nodesBegin
, j
));
1328 } else if(getNumChildren() == 0) {
1329 cache
[*this] = *this;
1332 NodeBuilder
<> nb(getKind());
1333 if(getMetaKind() == kind::metakind::PARAMETERIZED
) {
1334 // push the operator
1335 nb
<< getOperator();
1337 for(const_iterator i
= begin(),
1341 nb
<< (*i
).substitute(nodesBegin
, nodesEnd
,
1342 replacementsBegin
, replacementsEnd
,
1351 template <bool ref_count
>
1352 template <class Iterator
>
1354 NodeTemplate
<ref_count
>::substitute(Iterator substitutionsBegin
,
1355 Iterator substitutionsEnd
) const {
1356 std::hash_map
<TNode
, TNode
, TNodeHashFunction
> cache
;
1357 return substitute(substitutionsBegin
, substitutionsEnd
, cache
);
1360 template <bool ref_count
>
1361 template <class Iterator
>
1363 NodeTemplate
<ref_count
>::substitute(Iterator substitutionsBegin
,
1364 Iterator substitutionsEnd
,
1365 std::hash_map
<TNode
, TNode
, TNodeHashFunction
>& cache
) const {
1367 typename
std::hash_map
<TNode
, TNode
, TNodeHashFunction
>::const_iterator i
= cache
.find(*this);
1368 if(i
!= cache
.end()) {
1372 // otherwise compute
1373 Iterator j
= find_if(substitutionsBegin
, substitutionsEnd
,
1374 bind2nd(first_equal_to
<typename
Iterator::value_type::first_type
, typename
Iterator::value_type::second_type
>(), *this));
1375 if(j
!= substitutionsEnd
) {
1376 Node n
= (*j
).second
;
1379 } else if(getNumChildren() == 0) {
1380 cache
[*this] = *this;
1383 NodeBuilder
<> nb(getKind());
1384 if(getMetaKind() == kind::metakind::PARAMETERIZED
) {
1385 // push the operator
1386 nb
<< getOperator();
1388 for(const_iterator i
= begin(),
1392 nb
<< (*i
).substitute(substitutionsBegin
, substitutionsEnd
, cache
);
1400 template <bool ref_count
>
1401 inline Expr NodeTemplate
<ref_count
>::toExpr() {
1402 assertTNodeNotExpired();
1403 return NodeManager::currentNM()->toExpr(*this);
1406 // intentionally not defined for TNode
1408 inline Node NodeTemplate
<true>::fromExpr(const Expr
& e
) {
1409 return NodeManager::fromExpr(e
);
1412 template<bool ref_count
>
1413 bool NodeTemplate
<ref_count
>::hasSubterm(NodeTemplate
<false> t
, bool strict
) const {
1414 typedef std::hash_set
<TNode
, TNodeHashFunction
> node_set
;
1416 if (!strict
&& *this == t
) {
1421 std::vector
<TNode
> toProcess
;
1423 toProcess
.push_back(*this);
1425 for (unsigned i
= 0; i
< toProcess
.size(); ++ i
) {
1426 TNode current
= toProcess
[i
];
1427 for(unsigned j
= 0, j_end
= current
.getNumChildren(); j
< j_end
; ++ j
) {
1428 TNode child
= current
[j
];
1432 if (visited
.find(child
) != visited
.end()) {
1435 visited
.insert(child
);
1436 toProcess
.push_back(child
);
1446 * Pretty printer for use within gdb. This is not intended to be used
1447 * outside of gdb. This writes to the Warning() stream and immediately
1448 * flushes the stream.
1450 * Note that this function cannot be a template, since the compiler
1451 * won't instantiate it. Even if we explicitly instantiate. (Odd?)
1452 * So we implement twice. We mark as __attribute__((used)) so that
1453 * GCC emits code for it even though static analysis indicates it's
1456 * Tim's Note: I moved this into the node.h file because this allows gdb
1457 * to find the symbol, and use it, which is the first standard this code needs
1458 * to meet. A cleaner solution is welcomed.
1460 static void __attribute__((used
)) debugPrintNode(const NodeTemplate
<true>& n
) {
1461 Warning() << Node::setdepth(-1)
1462 << Node::setlanguage(language::output::LANG_AST
)
1466 static void __attribute__((used
)) debugPrintRawNode(const NodeTemplate
<true>& n
) {
1467 n
.printAst(Warning(), 0);
1471 static void __attribute__((used
)) debugPrintTNode(const NodeTemplate
<false>& n
) {
1472 Warning() << Node::setdepth(-1)
1473 << Node::setlanguage(language::output::LANG_AST
)
1477 static void __attribute__((used
)) debugPrintRawTNode(const NodeTemplate
<false>& n
) {
1478 n
.printAst(Warning(), 0);
1481 #endif /* CVC4_DEBUG */
1483 }/* CVC4 namespace */
1485 #endif /* __CVC4__NODE_H */