1 /********************* */
3 ** Original author: mdeters
4 ** Major contributors: cconway
5 ** Minor contributors (to current version): taking, dejan
6 ** This file is part of the CVC4 prototype.
7 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
8 ** Courant Institute of Mathematical Sciences
10 ** See the file COPYING in the top-level source directory for licensing
13 ** A manager for Nodes.
15 ** Reviewed by Chris Conway, Apr 5 2010 (bug #65).
18 #include "cvc4_private.h"
20 /* circular dependency; force node.h first */
21 #include "expr/attribute.h"
22 #include "expr/node.h"
23 #include "expr/type_node.h"
25 #ifndef __CVC4__NODE_MANAGER_H
26 #define __CVC4__NODE_MANAGER_H
30 #include <ext/hash_set>
32 #include "expr/kind.h"
33 #include "expr/metakind.h"
34 #include "expr/node_value.h"
35 #include "context/context.h"
41 // Definition of an attribute for the variable name.
42 // TODO: hide this attribute behind a NodeManager interface.
45 }/* CVC4::expr::attr namespace */
47 typedef expr::Attribute
<attr::VarNameTag
, std::string
> VarNameAttr
;
49 }/* CVC4::expr namespace */
52 template <class Builder
> friend class CVC4::NodeBuilderBase
;
53 friend class NodeManagerScope
;
54 friend class expr::NodeValue
;
56 typedef __gnu_cxx::hash_set
<expr::NodeValue
*,
57 expr::NodeValuePoolHashFcn
,
58 expr::NodeValuePoolEq
> NodeValuePool
;
59 typedef __gnu_cxx::hash_set
<expr::NodeValue
*,
60 expr::NodeValueIDHashFunction
,
61 expr::NodeValueEq
> ZombieSet
;
63 static __thread NodeManager
* s_current
;
65 NodeValuePool d_nodeValuePool
;
67 expr::attr::AttributeManager d_attrManager
;
70 * The node value we're currently freeing. This unique node value
71 * is permitted to have outstanding TNodes to it (in "soft"
72 * contexts, like as a key in attribute tables), even though
73 * normally it's an error to have a TNode to a node value with a
74 * reference count of 0. Being "under deletion" also enables
75 * assertions that inc() is not called on it. (A poorly-behaving
76 * attribute cleanup function could otherwise create a "Node" that
77 * points to the node value that is in the process of being deleted,
78 * springing it back to life.)
80 expr::NodeValue
* d_nodeUnderDeletion
;
83 * True iff we are in reclaimZombies(). This avoids unnecessary
84 * recursion; a NodeValue being deleted might zombify other
85 * NodeValues, but these shouldn't trigger a (recursive) call to
91 * Marks that we are in the Destructor currently.
96 * The set of zombie nodes. We may want to revisit this design, as
97 * we might like to delete nodes in least-recently-used order. But
98 * we also need to avoid processing a zombie twice.
103 * A set of operator singletons (w.r.t. to this NodeManager
104 * instance) for operators. Conceptually, Nodes with kind, say,
105 * PLUS, are APPLYs of a PLUS operator to arguments. This array
106 * holds the set of operators for these things. A PLUS operator is
107 * a Node with kind "BUILTIN", and if you call
108 * plusOperator->getConst<CVC4::Kind>(), you get kind::PLUS back.
110 Node d_operators
[kind::LAST_KIND
];
113 * Look up a NodeValue in the pool associated to this NodeManager.
114 * The NodeValue argument need not be a "completely-constructed"
115 * NodeValue. In particular, "non-inlined" constants are permitted
118 * For non-CONSTANT metakinds, nv's d_kind and d_nchildren should be
119 * correctly set, and d_children[0..n-1] should be valid (extant)
120 * NodeValues for lookup.
122 * For CONSTANT metakinds, nv's d_kind should be set correctly.
123 * Normally a CONSTANT would have d_nchildren == 0 and the constant
124 * value inlined in the d_children space. However, here we permit
125 * "non-inlined" NodeValues to avoid unnecessary copying. For
126 * these, d_nchildren == 1, and d_nchildren is a pointer to the
129 * The point of this complex design is to permit efficient lookups
130 * (without fully constructing a NodeValue). In the case that the
131 * argument is not fully constructed, and this function returns
132 * NULL, the caller should fully construct an equivalent one before
133 * calling poolInsert(). NON-FULLY-CONSTRUCTED NODEVALUES are not
134 * permitted in the pool!
136 inline expr::NodeValue
* poolLookup(expr::NodeValue
* nv
) const;
139 * Insert a NodeValue into the NodeManager's pool.
141 * It is an error to insert a NodeValue already in the pool.
142 * Enquire first with poolLookup().
144 inline void poolInsert(expr::NodeValue
* nv
);
147 * Remove a NodeValue from the NodeManager's pool.
149 * It is an error to request the removal of a NodeValue from the
150 * pool that is not in the pool.
152 inline void poolRemove(expr::NodeValue
* nv
);
155 * Determine if nv is currently being deleted by the NodeManager.
157 inline bool isCurrentlyDeleting(const expr::NodeValue
* nv
) const {
158 return d_nodeUnderDeletion
== nv
;
162 * Register a NodeValue as a zombie.
164 inline void markForDeletion(expr::NodeValue
* nv
) {
165 Assert(nv
->d_rc
== 0);
167 // if d_reclaiming is set, make sure we don't call
168 // reclaimZombies(), because it's already running.
169 Debug("gc") << "zombifying node value " << nv
170 << " [" << nv
->d_id
<< "]: " << *nv
171 << (d_dontGC
? " [CURRENTLY-RECLAIMING]" : "")
173 d_zombies
.insert(nv
);// FIXME multithreading
175 if(!d_dontGC
) {// FIXME multithreading
176 // for now, collect eagerly. can add heuristic here later..
182 * Reclaim all zombies.
184 void reclaimZombies();
187 * This template gives a mechanism to stack-allocate a NodeValue
188 * with enough space for N children (where N is a compile-time
189 * constant). You use it like this:
191 * NVStorage<4> nvStorage;
192 * NodeValue& nvStack = reinterpret_cast<NodeValue&>(nvStorage);
194 * ...and then you can use nvStack as a NodeValue that you know has
195 * room for 4 children.
200 expr::NodeValue
* child
[N
];
201 };/* struct NodeManager::NVStorage<N> */
207 // NodeManager's attributes. These aren't exposed outside of this
208 // class; use the getters.
209 typedef expr::Attribute
<TypeTag
, TypeNode
> TypeAttr
;
210 typedef expr::Attribute
<AtomicTag
, bool> AtomicAttr
;
213 * Returns true if this node is atomic (has no more Boolean
214 * structure). This is the NodeValue version for NodeManager's
215 * internal use. There's a public version of this function below
216 * that takes a TNode.
217 * @param nv the node to check for atomicity
218 * @return true if atomic
220 inline bool isAtomic(expr::NodeValue
* nv
) const {
221 // The kindCanBeAtomic() and metakind checking are just optimizations
222 // (to avoid the hashtable lookup). We assume that all nodes have
223 // the atomic attribute pre-computed and set at their time of
224 // creation. This is because:
225 // (1) it's super cheap to do it bottom-up.
226 // (2) if we computed it lazily, we'd need a second attribute to
227 // tell us whether we had computed it yet or not.
228 // The pre-computation and registration occurs in poolInsert().
229 AssertArgument(nv
->getMetaKind() != kind::metakind::INVALID
, *nv
,
230 "NodeManager::isAtomic() called on INVALID node (%s)",
231 kind::kindToString(nv
->getKind()).c_str());
233 nv
->getMetaKind() == kind::metakind::VARIABLE
||
234 nv
->getMetaKind() == kind::metakind::CONSTANT
||
235 ( kind::kindCanBeAtomic(nv
->getKind()) &&
236 getAttribute(nv
, AtomicAttr()) );
241 NodeManager(context::Context
* ctxt
);
245 * Return true if we are in destruction.
247 bool inDestruction() const { return d_inDestruction
; }
249 /** The node manager in the current context. */
250 static NodeManager
* currentNM() { return s_current
; }
252 // general expression-builders
254 /** Create a node with no children. */
255 Node
mkNode(Kind kind
);
256 Node
* mkNodePtr(Kind kind
);
258 /** Create a node with one child. */
259 Node
mkNode(Kind kind
, TNode child1
);
260 Node
* mkNodePtr(Kind kind
, TNode child1
);
262 /** Create a node with two children. */
263 Node
mkNode(Kind kind
, TNode child1
, TNode child2
);
264 Node
* mkNodePtr(Kind kind
, TNode child1
, TNode child2
);
266 /** Create a node with three children. */
267 Node
mkNode(Kind kind
, TNode child1
, TNode child2
, TNode child3
);
268 Node
* mkNodePtr(Kind kind
, TNode child1
, TNode child2
, TNode child3
);
270 /** Create a node with four children. */
271 Node
mkNode(Kind kind
, TNode child1
, TNode child2
, TNode child3
,
273 Node
* mkNodePtr(Kind kind
, TNode child1
, TNode child2
, TNode child3
,
276 /** Create a node with five children. */
277 Node
mkNode(Kind kind
, TNode child1
, TNode child2
, TNode child3
,
278 TNode child4
, TNode child5
);
279 Node
* mkNodePtr(Kind kind
, TNode child1
, TNode child2
, TNode child3
,
280 TNode child4
, TNode child5
);
282 /** Create a node with an arbitrary number of children. */
283 template <bool ref_count
>
284 Node
mkNode(Kind kind
, const std::vector
<NodeTemplate
<ref_count
> >& children
);
285 template <bool ref_count
>
286 Node
* mkNodePtr(Kind kind
, const std::vector
<NodeTemplate
<ref_count
> >& children
);
289 * Create a variable with the given name and type. NOTE that no
290 * lookup is done on the name. If you mkVar("a", type) and then
291 * mkVar("a", type) again, you have two variables.
293 Node
mkVar(const std::string
& name
, const TypeNode
& type
);
294 Node
* mkVarPtr(const std::string
& name
, const TypeNode
& type
);
296 /** Create a variable with the given type. */
297 Node
mkVar(const TypeNode
& type
);
298 Node
* mkVarPtr(const TypeNode
& type
);
302 * Create a constant of type T. It will have the appropriate
303 * CONST_* kind defined for T.
306 Node
mkConst(const T
&);
309 TypeNode
mkTypeConst(const T
&);
311 template <class NodeClass
, class T
>
312 NodeClass
mkConstInternal(const T
&);
314 /** Create a type-variable */
315 TypeNode
mkTypeVar();
316 TypeNode
mkTypeVar(const std::string
& name
);
318 /** Create a node with no children. */
319 TypeNode
mkTypeNode(Kind kind
, const std::vector
<TypeNode
>& children
);
322 * Determine whether Nodes of a particular Kind have operators.
323 * @returns true if Nodes of Kind k have operators.
325 static inline bool hasOperator(Kind k
);
328 * Get the (singleton) operator of an OPERATOR-kinded kind. The
329 * returned node n will have kind BUILTIN, and calling
330 * n.getConst<CVC4::Kind>() will yield k.
332 inline TNode
operatorOf(Kind k
) {
333 AssertArgument( kind::metaKindOf(k
) == kind::metakind::OPERATOR
, k
,
334 "Kind is not an OPERATOR-kinded kind "
335 "in NodeManager::operatorOf()" );
336 return d_operators
[k
];
340 * Retrieve an attribute for a node.
342 * @param nv the node value
343 * @param attr an instance of the attribute kind to retrieve.
344 * @returns the attribute, if set, or a default-constructed
345 * <code>AttrKind::value_type</code> if not.
347 template <class AttrKind
>
348 inline typename
AttrKind::value_type
getAttribute(expr::NodeValue
* nv
,
349 const AttrKind
& attr
) const;
352 * Check whether an attribute is set for a node.
354 * @param nv the node value
355 * @param attr an instance of the attribute kind to check
356 * @returns <code>true</code> iff <code>attr</code> is set for
359 template <class AttrKind
>
360 inline bool hasAttribute(expr::NodeValue
* nv
,
361 const AttrKind
& attr
) const;
364 * Check whether an attribute is set for a node, and, if so,
367 * @param nv the node value
368 * @param attr an instance of the attribute kind to check
369 * @param value a reference to an object of the attribute's value type.
370 * <code>value</code> will be set to the value of the attribute, if it is
371 * set for <code>nv</code>; otherwise, it will be set to the default
372 * value of the attribute.
373 * @returns <code>true</code> iff <code>attr</code> is set for
376 template <class AttrKind
>
377 inline bool getAttribute(expr::NodeValue
* nv
,
378 const AttrKind
& attr
,
379 typename
AttrKind::value_type
& value
) const;
382 * Set an attribute for a node. If the node doesn't have the
383 * attribute, this function assigns one. If the node has one, this
386 * @param nv the node value
387 * @param attr an instance of the attribute kind to set
388 * @param value the value of <code>attr</code> for <code>nv</code>
390 template <class AttrKind
>
391 inline void setAttribute(expr::NodeValue
* nv
,
392 const AttrKind
& attr
,
393 const typename
AttrKind::value_type
& value
);
396 * Retrieve an attribute for a TNode.
399 * @param attr an instance of the attribute kind to retrieve.
400 * @returns the attribute, if set, or a default-constructed
401 * <code>AttrKind::value_type</code> if not.
403 template <class AttrKind
>
404 inline typename
AttrKind::value_type
405 getAttribute(TNode n
, const AttrKind
& attr
) const;
408 * Check whether an attribute is set for a TNode.
411 * @param attr an instance of the attribute kind to check
412 * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
414 template <class AttrKind
>
415 inline bool hasAttribute(TNode n
,
416 const AttrKind
& attr
) const;
419 * Check whether an attribute is set for a TNode and, if so, retieve
423 * @param attr an instance of the attribute kind to check
424 * @param value a reference to an object of the attribute's value type.
425 * <code>value</code> will be set to the value of the attribute, if it is
426 * set for <code>nv</code>; otherwise, it will be set to the default value of
428 * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
430 template <class AttrKind
>
431 inline bool getAttribute(TNode n
,
432 const AttrKind
& attr
,
433 typename
AttrKind::value_type
& value
) const;
436 * Set an attribute for a node. If the node doesn't have the
437 * attribute, this function assigns one. If the node has one, this
441 * @param attr an instance of the attribute kind to set
442 * @param value the value of <code>attr</code> for <code>n</code>
444 template <class AttrKind
>
445 inline void setAttribute(TNode n
,
446 const AttrKind
& attr
,
447 const typename
AttrKind::value_type
& value
);
449 /** Get the (singleton) type for booleans. */
450 inline TypeNode
booleanType();
452 /** Get the (singleton) type for sorts. */
453 inline TypeNode
kindType();
456 * Make a function type from domain to range.
458 * @param domain the domain type
459 * @param range the range type
460 * @returns the functional type domain -> range
462 inline TypeNode
mkFunctionType(const TypeNode
& domain
, const TypeNode
& range
);
465 * Make a function type with input types from
466 * argTypes. <code>argTypes</code> must have at least one element.
468 * @param argTypes the domain is a tuple (argTypes[0], ..., argTypes[n])
469 * @param range the range type
470 * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range
472 inline TypeNode
mkFunctionType(const std::vector
<TypeNode
>& argTypes
, const TypeNode
& range
);
475 * Make a function type with input types from
476 * <code>sorts[0..sorts.size()-2]</code> and result type
477 * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
478 * at least 2 elements.
480 inline TypeNode
mkFunctionType(const std::vector
<TypeNode
>& sorts
);
483 * Make a predicate type with input types from
484 * <code>sorts</code>. The result with be a function type with range
485 * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
488 inline TypeNode
mkPredicateType(const std::vector
<TypeNode
>& sorts
);
490 /** Make a new sort. */
491 inline TypeNode
mkSort();
493 /** Make a new sort with the given name. */
494 inline TypeNode
mkSort(const std::string
& name
);
497 * Get the type for the given node.
499 inline TypeNode
getType(TNode n
);
502 * Returns true if this node is atomic (has no more Boolean structure)
503 * @param n the node to check for atomicity
504 * @return true if atomic
506 inline bool isAtomic(TNode n
) const {
507 return isAtomic(n
.d_nv
);
512 * This class changes the "current" thread-global
513 * <code>NodeManager</code> when it is created and reinstates the
514 * previous thread-global <code>NodeManager</code> when it is
515 * destroyed, effectively maintaining a set of nested
516 * <code>NodeManager</code> scopes. This is especially useful on
517 * public-interface calls into the CVC4 library, where CVC4's notion
518 * of the "current" <code>NodeManager</code> should be set to match
519 * the calling context. See, for example, the implementations of
520 * public calls in the <code>ExprManager</code> and
521 * <code>SmtEngine</code> classes.
523 * The client must be careful to create and destroy
524 * <code>NodeManagerScope</code> objects in a well-nested manner (such
525 * as on the stack). You may create a <code>NodeManagerScope</code>
526 * with <code>new</code> and destroy it with <code>delete</code>, or
527 * place it as a data member of an object that is, but if the scope of
528 * these <code>new</code>/<code>delete</code> pairs isn't properly
529 * maintained, the incorrect "current" <code>NodeManager</code>
530 * pointer may be restored after a delete.
532 class NodeManagerScope
{
533 /** The old NodeManager, to be restored on destruction. */
534 NodeManager
*d_oldNodeManager
;
538 NodeManagerScope(NodeManager
* nm
) : d_oldNodeManager(NodeManager::s_current
) {
539 NodeManager::s_current
= nm
;
540 Debug("current") << "node manager scope: "
541 << NodeManager::s_current
<< "\n";
544 ~NodeManagerScope() {
545 NodeManager::s_current
= d_oldNodeManager
;
546 Debug("current") << "node manager scope: "
547 << "returning to " << NodeManager::s_current
<< "\n";
552 template <class AttrKind
>
553 inline typename
AttrKind::value_type
554 NodeManager::getAttribute(expr::NodeValue
* nv
, const AttrKind
&) const {
555 return d_attrManager
.getAttribute(nv
, AttrKind());
558 template <class AttrKind
>
559 inline bool NodeManager::hasAttribute(expr::NodeValue
* nv
,
560 const AttrKind
&) const {
561 return d_attrManager
.hasAttribute(nv
, AttrKind());
564 template <class AttrKind
>
566 NodeManager::getAttribute(expr::NodeValue
* nv
, const AttrKind
&,
567 typename
AttrKind::value_type
& ret
) const {
568 return d_attrManager
.getAttribute(nv
, AttrKind(), ret
);
571 template <class AttrKind
>
573 NodeManager::setAttribute(expr::NodeValue
* nv
, const AttrKind
&,
574 const typename
AttrKind::value_type
& value
) {
575 d_attrManager
.setAttribute(nv
, AttrKind(), value
);
578 template <class AttrKind
>
579 inline typename
AttrKind::value_type
580 NodeManager::getAttribute(TNode n
, const AttrKind
&) const {
581 return d_attrManager
.getAttribute(n
.d_nv
, AttrKind());
584 template <class AttrKind
>
586 NodeManager::hasAttribute(TNode n
, const AttrKind
&) const {
587 return d_attrManager
.hasAttribute(n
.d_nv
, AttrKind());
590 template <class AttrKind
>
592 NodeManager::getAttribute(TNode n
, const AttrKind
&,
593 typename
AttrKind::value_type
& ret
) const {
594 return d_attrManager
.getAttribute(n
.d_nv
, AttrKind(), ret
);
597 template <class AttrKind
>
599 NodeManager::setAttribute(TNode n
, const AttrKind
&,
600 const typename
AttrKind::value_type
& value
) {
601 d_attrManager
.setAttribute(n
.d_nv
, AttrKind(), value
);
605 /** Get the (singleton) type for booleans. */
606 inline TypeNode
NodeManager::booleanType() {
607 return TypeNode(mkTypeConst
<TypeConstant
>(BOOLEAN_TYPE
));
610 /** Get the (singleton) type for sorts. */
611 inline TypeNode
NodeManager::kindType() {
612 return TypeNode(mkTypeConst
<TypeConstant
>(KIND_TYPE
));
615 /** Make a function type from domain to range. */
616 inline TypeNode
NodeManager::mkFunctionType(const TypeNode
& domain
, const TypeNode
& range
) {
617 std::vector
<TypeNode
> sorts
;
618 sorts
.push_back(domain
);
619 sorts
.push_back(range
);
620 return mkFunctionType(sorts
);
623 inline TypeNode
NodeManager::mkFunctionType(const std::vector
<TypeNode
>& argTypes
, const TypeNode
& range
) {
624 Assert(argTypes
.size() >= 1);
625 std::vector
<TypeNode
> sorts(argTypes
);
626 sorts
.push_back(range
);
627 return mkFunctionType(sorts
);
631 NodeManager::mkFunctionType(const std::vector
<TypeNode
>& sorts
) {
632 Assert(sorts
.size() >= 2);
633 std::vector
<TypeNode
> sortNodes
;
634 for (unsigned i
= 0; i
< sorts
.size(); ++ i
) {
635 sortNodes
.push_back(sorts
[i
]);
637 return mkTypeNode(kind::FUNCTION_TYPE
, sortNodes
);
641 NodeManager::mkPredicateType(const std::vector
<TypeNode
>& sorts
) {
642 Assert(sorts
.size() >= 1);
643 std::vector
<TypeNode
> sortNodes
;
644 for (unsigned i
= 0; i
< sorts
.size(); ++ i
) {
645 sortNodes
.push_back(sorts
[i
]);
647 sortNodes
.push_back(booleanType());
648 return mkTypeNode(kind::FUNCTION_TYPE
, sortNodes
);
651 inline TypeNode
NodeManager::mkSort() {
655 inline TypeNode
NodeManager::mkSort(const std::string
& name
) {
656 return mkTypeVar(name
);
659 inline TypeNode
NodeManager::getType(TNode n
) {
661 getAttribute(n
, TypeAttr(), typeNode
);
662 // TODO: Type computation
666 inline expr::NodeValue
* NodeManager::poolLookup(expr::NodeValue
* nv
) const {
667 NodeValuePool::const_iterator find
= d_nodeValuePool
.find(nv
);
668 if(find
== d_nodeValuePool
.end()) {
675 inline void NodeManager::poolInsert(expr::NodeValue
* nv
) {
676 Assert(d_nodeValuePool
.find(nv
) == d_nodeValuePool
.end(),
677 "NodeValue already in the pool!");
678 d_nodeValuePool
.insert(nv
);// FIXME multithreading
680 switch(nv
->getMetaKind()) {
681 case kind::metakind::INVALID
:
682 case kind::metakind::VARIABLE
:
683 case kind::metakind::CONSTANT
:
684 // nothing to do (don't bother setting the attribute, isAtomic()
685 // on VARIABLEs and CONSTANTs is always true)
688 case kind::metakind::OPERATOR
:
689 case kind::metakind::PARAMETERIZED
:
691 // register this NodeValue as atomic or not; use nv_begin/end
692 // because we need to consider the operator too in the case of
693 // PARAMETERIZED-metakinded nodes (i.e. APPLYs); they could have a
696 // assume it's atomic if its kind can be atomic, check children
697 // to see if that is actually true
698 bool atomic
= kind::kindCanBeAtomic(nv
->getKind());
700 for(expr::NodeValue::nv_iterator i
= nv
->nv_begin();
703 if(!(atomic
= isAtomic(*i
))) {
709 setAttribute(nv
, AtomicAttr(), atomic
);
714 inline void NodeManager::poolRemove(expr::NodeValue
* nv
) {
715 Assert(d_nodeValuePool
.find(nv
) != d_nodeValuePool
.end(),
716 "NodeValue is not in the pool!");
718 d_nodeValuePool
.erase(nv
);// FIXME multithreading
721 }/* CVC4 namespace */
723 #define __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
724 #include "expr/metakind.h"
725 #undef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
727 #include "expr/node_builder.h"
731 // general expression-builders
733 inline bool NodeManager::hasOperator(Kind k
) {
734 switch(kind::MetaKind mk
= kind::metaKindOf(k
)) {
736 case kind::metakind::INVALID
:
737 case kind::metakind::VARIABLE
:
740 case kind::metakind::OPERATOR
:
741 case kind::metakind::PARAMETERIZED
:
744 case kind::metakind::CONSTANT
:
752 inline Node
NodeManager::mkNode(Kind kind
) {
753 return NodeBuilder
<0>(this, kind
);
756 inline Node
* NodeManager::mkNodePtr(Kind kind
) {
757 NodeBuilder
<0> nb(this, kind
);
758 return nb
.constructNodePtr();
761 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
) {
762 return NodeBuilder
<1>(this, kind
) << child1
;
765 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
) {
766 NodeBuilder
<1> nb(this, kind
);
768 return nb
.constructNodePtr();
771 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
, TNode child2
) {
772 return NodeBuilder
<2>(this, kind
) << child1
<< child2
;
775 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
, TNode child2
) {
776 NodeBuilder
<2> nb(this, kind
);
777 nb
<< child1
<< child2
;
778 return nb
.constructNodePtr();
781 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
, TNode child2
,
783 return NodeBuilder
<3>(this, kind
) << child1
<< child2
<< child3
;
786 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
, TNode child2
,
788 NodeBuilder
<3> nb(this, kind
);
789 nb
<< child1
<< child2
<< child3
;
790 return nb
.constructNodePtr();
793 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
, TNode child2
,
794 TNode child3
, TNode child4
) {
795 return NodeBuilder
<4>(this, kind
) << child1
<< child2
<< child3
<< child4
;
798 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
, TNode child2
,
799 TNode child3
, TNode child4
) {
800 NodeBuilder
<4> nb(this, kind
);
801 nb
<< child1
<< child2
<< child3
<< child4
;
802 return nb
.constructNodePtr();
805 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
, TNode child2
,
806 TNode child3
, TNode child4
, TNode child5
) {
807 return NodeBuilder
<5>(this, kind
) << child1
<< child2
<< child3
<< child4
811 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
, TNode child2
,
812 TNode child3
, TNode child4
, TNode child5
) {
813 NodeBuilder
<5> nb(this, kind
);
814 nb
<< child1
<< child2
<< child3
<< child4
<< child5
;
815 return nb
.constructNodePtr();
819 template <bool ref_count
>
820 inline Node
NodeManager::mkNode(Kind kind
,
821 const std::vector
<NodeTemplate
<ref_count
> >&
823 return NodeBuilder
<>(this, kind
).append(children
);
826 template <bool ref_count
>
827 inline Node
* NodeManager::mkNodePtr(Kind kind
,
828 const std::vector
<NodeTemplate
<ref_count
> >&
830 return NodeBuilder
<>(this, kind
).append(children
).constructNodePtr();
833 // N-ary version for types
834 inline TypeNode
NodeManager::mkTypeNode(Kind kind
, const std::vector
<TypeNode
>& children
) {
835 return NodeBuilder
<>(this, kind
).append(children
).constructTypeNode();
839 inline Node
NodeManager::mkVar(const std::string
& name
, const TypeNode
& type
) {
840 Node n
= mkVar(type
);
841 n
.setAttribute(expr::VarNameAttr(), name
);
845 inline Node
* NodeManager::mkVarPtr(const std::string
& name
, const TypeNode
& type
) {
846 Node
* n
= mkVarPtr(type
);
847 n
->setAttribute(expr::VarNameAttr(), name
);
851 inline Node
NodeManager::mkVar(const TypeNode
& type
) {
852 Node n
= NodeBuilder
<0>(this, kind::VARIABLE
);
853 n
.setAttribute(TypeAttr(), type
);
857 inline TypeNode
NodeManager::mkTypeVar(const std::string
& name
) {
858 TypeNode type
= mkTypeVar();
859 type
.setAttribute(expr::VarNameAttr(), name
);
863 inline TypeNode
NodeManager::mkTypeVar() {
864 TypeNode type
= NodeBuilder
<0>(this, kind::VARIABLE
).constructTypeNode();
868 inline Node
* NodeManager::mkVarPtr(const TypeNode
& type
) {
869 Node
* n
= NodeBuilder
<0>(this, kind::VARIABLE
).constructNodePtr();
870 n
->setAttribute(TypeAttr(), type
);
875 Node
NodeManager::mkConst(const T
& val
) {
876 return mkConstInternal
<Node
, T
>(val
);
880 TypeNode
NodeManager::mkTypeConst(const T
& val
) {
881 return mkConstInternal
<TypeNode
, T
>(val
);
884 template <class NodeClass
, class T
>
885 NodeClass
NodeManager::mkConstInternal(const T
& val
) {
887 // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
888 NVStorage
<1> nvStorage
;
889 expr::NodeValue
& nvStack
= reinterpret_cast<expr::NodeValue
&>(nvStorage
);
892 nvStack
.d_kind
= kind::metakind::ConstantMap
<T
>::kind
;
894 nvStack
.d_nchildren
= 1;
895 nvStack
.d_children
[0] =
896 const_cast<expr::NodeValue
*>(reinterpret_cast<const expr::NodeValue
*>(&val
));
897 expr::NodeValue
* nv
= poolLookup(&nvStack
);
900 return NodeClass(nv
);
903 nv
= (expr::NodeValue
*)
904 std::malloc(sizeof(expr::NodeValue
) + sizeof(T
));
906 throw std::bad_alloc();
910 nv
->d_kind
= kind::metakind::ConstantMap
<T
>::kind
;
911 nv
->d_id
= expr::NodeValue::next_id
++;// FIXME multithreading
914 //OwningTheory::mkConst(val);
915 new (&nv
->d_children
) T(val
);
918 Debug("gc") << "creating node value " << nv
919 << " [" << nv
->d_id
<< "]: " << *nv
<< "\n";
921 return NodeClass(nv
);
924 }/* CVC4 namespace */
926 #endif /* __CVC4__EXPR_MANAGER_H */