1 /********************* */
2 /*! \file node_manager.h
4 ** Original author: mdeters
5 ** Major contributors: cconway, dejan
6 ** Minor contributors (to current version): taking
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 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 A manager for Nodes.
16 ** A manager for Nodes.
18 ** Reviewed by Chris Conway, Apr 5 2010 (bug #65).
21 #include "cvc4_private.h"
23 /* circular dependency; force node.h first */
24 #include "expr/attribute.h"
25 #include "expr/node.h"
26 #include "expr/type_node.h"
27 #include "expr/expr.h"
29 #ifndef __CVC4__NODE_MANAGER_H
30 #define __CVC4__NODE_MANAGER_H
34 #include <ext/hash_set>
36 #include "expr/kind.h"
37 #include "expr/metakind.h"
38 #include "expr/node_value.h"
39 #include "context/context.h"
40 #include "util/configuration_private.h"
47 // Definition of an attribute for the variable name.
48 // TODO: hide this attribute behind a NodeManager interface.
51 }/* CVC4::expr::attr namespace */
53 typedef expr::Attribute
<attr::VarNameTag
, std::string
> VarNameAttr
;
55 }/* CVC4::expr namespace */
58 template <unsigned nchild_thresh
> friend class CVC4::NodeBuilder
;
59 friend class NodeManagerScope
;
60 friend class expr::NodeValue
;
62 /** Predicate for use with STL algorithms */
63 struct NodeValueReferenceCountNonZero
{
64 bool operator()(expr::NodeValue
* nv
) { return nv
->d_rc
> 0; }
67 typedef __gnu_cxx::hash_set
<expr::NodeValue
*,
68 expr::NodeValuePoolHashFcn
,
69 expr::NodeValuePoolEq
> NodeValuePool
;
70 typedef __gnu_cxx::hash_set
<expr::NodeValue
*,
71 expr::NodeValueIDHashFunction
,
72 expr::NodeValueEq
> ZombieSet
;
74 static CVC4_THREADLOCAL(NodeManager
*) s_current
;
76 NodeValuePool d_nodeValuePool
;
78 expr::attr::AttributeManager d_attrManager
;
81 * The node value we're currently freeing. This unique node value
82 * is permitted to have outstanding TNodes to it (in "soft"
83 * contexts, like as a key in attribute tables), even though
84 * normally it's an error to have a TNode to a node value with a
85 * reference count of 0. Being "under deletion" also enables
86 * assertions that inc() is not called on it. (A poorly-behaving
87 * attribute cleanup function could otherwise create a "Node" that
88 * points to the node value that is in the process of being deleted,
89 * springing it back to life.)
91 expr::NodeValue
* d_nodeUnderDeletion
;
94 * True iff we are in reclaimZombies(). This avoids unnecessary
95 * recursion; a NodeValue being deleted might zombify other
96 * NodeValues, but these shouldn't trigger a (recursive) call to
99 bool d_inReclaimZombies
;
102 * The set of zombie nodes. We may want to revisit this design, as
103 * we might like to delete nodes in least-recently-used order. But
104 * we also need to avoid processing a zombie twice.
109 * A set of operator singletons (w.r.t. to this NodeManager
110 * instance) for operators. Conceptually, Nodes with kind, say,
111 * PLUS, are APPLYs of a PLUS operator to arguments. This array
112 * holds the set of operators for these things. A PLUS operator is
113 * a Node with kind "BUILTIN", and if you call
114 * plusOperator->getConst<CVC4::Kind>(), you get kind::PLUS back.
116 Node d_operators
[kind::LAST_KIND
];
119 * Look up a NodeValue in the pool associated to this NodeManager.
120 * The NodeValue argument need not be a "completely-constructed"
121 * NodeValue. In particular, "non-inlined" constants are permitted
124 * For non-CONSTANT metakinds, nv's d_kind and d_nchildren should be
125 * correctly set, and d_children[0..n-1] should be valid (extant)
126 * NodeValues for lookup.
128 * For CONSTANT metakinds, nv's d_kind should be set correctly.
129 * Normally a CONSTANT would have d_nchildren == 0 and the constant
130 * value inlined in the d_children space. However, here we permit
131 * "non-inlined" NodeValues to avoid unnecessary copying. For
132 * these, d_nchildren == 1, and d_nchildren is a pointer to the
135 * The point of this complex design is to permit efficient lookups
136 * (without fully constructing a NodeValue). In the case that the
137 * argument is not fully constructed, and this function returns
138 * NULL, the caller should fully construct an equivalent one before
139 * calling poolInsert(). NON-FULLY-CONSTRUCTED NODEVALUES are not
140 * permitted in the pool!
142 inline expr::NodeValue
* poolLookup(expr::NodeValue
* nv
) const;
145 * Insert a NodeValue into the NodeManager's pool.
147 * It is an error to insert a NodeValue already in the pool.
148 * Enquire first with poolLookup().
150 inline void poolInsert(expr::NodeValue
* nv
);
153 * Remove a NodeValue from the NodeManager's pool.
155 * It is an error to request the removal of a NodeValue from the
156 * pool that is not in the pool.
158 inline void poolRemove(expr::NodeValue
* nv
);
161 * Determine if nv is currently being deleted by the NodeManager.
163 inline bool isCurrentlyDeleting(const expr::NodeValue
* nv
) const {
164 return d_nodeUnderDeletion
== nv
;
168 * Register a NodeValue as a zombie.
170 inline void markForDeletion(expr::NodeValue
* nv
) {
171 Assert(nv
->d_rc
== 0);
173 // if d_reclaiming is set, make sure we don't call
174 // reclaimZombies(), because it's already running.
175 Debug("gc") << "zombifying node value " << nv
176 << " [" << nv
->d_id
<< "]: " << *nv
177 << (d_inReclaimZombies
? " [CURRENTLY-RECLAIMING]" : "")
179 d_zombies
.insert(nv
);// FIXME multithreading
181 if(!d_inReclaimZombies
) {// FIXME multithreading
182 // for now, collect eagerly. can add heuristic here later..
183 if(d_zombies
.size() > 5000) {
190 * Reclaim all zombies.
192 void reclaimZombies();
195 * This template gives a mechanism to stack-allocate a NodeValue
196 * with enough space for N children (where N is a compile-time
197 * constant). You use it like this:
199 * NVStorage<4> nvStorage;
200 * NodeValue& nvStack = reinterpret_cast<NodeValue&>(nvStorage);
202 * ...and then you can use nvStack as a NodeValue that you know has
203 * room for 4 children.
208 expr::NodeValue
* child
[N
];
209 };/* struct NodeManager::NVStorage<N> */
213 struct TypeCheckedTag
;
215 // NodeManager's attributes. These aren't exposed outside of this
216 // class; use the getters.
217 typedef expr::Attribute
<TypeTag
, TypeNode
> TypeAttr
;
218 typedef expr::Attribute
<TypeCheckedTag
, bool> TypeCheckedAttr
;
220 /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
222 * It has been decided for now to hold off on implementations of
223 * these functions, as they may only be needed in CNF conversion,
224 * where it's pointless to do a lazy isAtomic determination by
225 * searching through the DAG, and storing it, since the result will
226 * only be used once. For more details see the 4/27/2010 CVC4
227 * developer's meeting notes at:
229 * http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
231 // bool containsDecision(TNode); // is "atomic"
232 // bool properlyContainsDecision(TNode); // all children are atomic
236 NodeManager(context::Context
* ctxt
);
239 /** The node manager in the current context. */
240 static NodeManager
* currentNM() { return s_current
; }
242 // general expression-builders
244 /** Create a node with one child. */
245 Node
mkNode(Kind kind
, TNode child1
);
246 Node
* mkNodePtr(Kind kind
, TNode child1
);
248 /** Create a node with two children. */
249 Node
mkNode(Kind kind
, TNode child1
, TNode child2
);
250 Node
* mkNodePtr(Kind kind
, TNode child1
, TNode child2
);
252 /** Create a node with three children. */
253 Node
mkNode(Kind kind
, TNode child1
, TNode child2
, TNode child3
);
254 Node
* mkNodePtr(Kind kind
, TNode child1
, TNode child2
, TNode child3
);
256 /** Create a node with four children. */
257 Node
mkNode(Kind kind
, TNode child1
, TNode child2
, TNode child3
,
259 Node
* mkNodePtr(Kind kind
, TNode child1
, TNode child2
, TNode child3
,
262 /** Create a node with five children. */
263 Node
mkNode(Kind kind
, TNode child1
, TNode child2
, TNode child3
,
264 TNode child4
, TNode child5
);
265 Node
* mkNodePtr(Kind kind
, TNode child1
, TNode child2
, TNode child3
,
266 TNode child4
, TNode child5
);
268 /** Create a node with an arbitrary number of children. */
269 template <bool ref_count
>
270 Node
mkNode(Kind kind
, const std::vector
<NodeTemplate
<ref_count
> >& children
);
271 template <bool ref_count
>
272 Node
* mkNodePtr(Kind kind
, const std::vector
<NodeTemplate
<ref_count
> >& children
);
274 /** Create a node by applying an operator to the children */
275 template <bool ref_count
>
276 Node
mkNode(TNode opNode
, const std::vector
<NodeTemplate
<ref_count
> >& children
);
277 template <bool ref_count
>
278 Node
* mkNodePtr(TNode opNode
, const std::vector
<NodeTemplate
<ref_count
> >& children
);
281 * Create a variable with the given name and type. NOTE that no
282 * lookup is done on the name. If you mkVar("a", type) and then
283 * mkVar("a", type) again, you have two variables.
285 Node
mkVar(const std::string
& name
, const TypeNode
& type
);
286 Node
* mkVarPtr(const std::string
& name
, const TypeNode
& type
);
288 /** Create a variable with the given type. */
289 Node
mkVar(const TypeNode
& type
);
290 Node
* mkVarPtr(const TypeNode
& type
);
292 /** Create a skolem constant with the given type. */
293 Node
mkSkolem(const TypeNode
& type
);
296 * Create a constant of type T. It will have the appropriate
297 * CONST_* kind defined for T.
300 Node
mkConst(const T
&);
303 TypeNode
mkTypeConst(const T
&);
305 template <class NodeClass
, class T
>
306 NodeClass
mkConstInternal(const T
&);
308 /** Create a node with children. */
309 TypeNode
mkTypeNode(Kind kind
, TypeNode child1
);
310 TypeNode
mkTypeNode(Kind kind
, TypeNode child1
, TypeNode child2
);
311 TypeNode
mkTypeNode(Kind kind
, TypeNode child1
, TypeNode child2
,
313 TypeNode
mkTypeNode(Kind kind
, const std::vector
<TypeNode
>& children
);
316 * Determine whether Nodes of a particular Kind have operators.
317 * @returns true if Nodes of Kind k have operators.
319 static inline bool hasOperator(Kind k
);
322 * Get the (singleton) operator of an OPERATOR-kinded kind. The
323 * returned node n will have kind BUILTIN, and calling
324 * n.getConst<CVC4::Kind>() will yield k.
326 inline TNode
operatorOf(Kind k
) {
327 AssertArgument( kind::metaKindOf(k
) == kind::metakind::OPERATOR
, k
,
328 "Kind is not an OPERATOR-kinded kind "
329 "in NodeManager::operatorOf()" );
330 return d_operators
[k
];
334 * Retrieve an attribute for a node.
336 * @param nv the node value
337 * @param attr an instance of the attribute kind to retrieve.
338 * @returns the attribute, if set, or a default-constructed
339 * <code>AttrKind::value_type</code> if not.
341 template <class AttrKind
>
342 inline typename
AttrKind::value_type
getAttribute(expr::NodeValue
* nv
,
343 const AttrKind
& attr
) const;
346 * Check whether an attribute is set for a node.
348 * @param nv the node value
349 * @param attr an instance of the attribute kind to check
350 * @returns <code>true</code> iff <code>attr</code> is set for
353 template <class AttrKind
>
354 inline bool hasAttribute(expr::NodeValue
* nv
,
355 const AttrKind
& attr
) const;
358 * Check whether an attribute is set for a node, and, if so,
361 * @param nv the node value
362 * @param attr an instance of the attribute kind to check
363 * @param value a reference to an object of the attribute's value type.
364 * <code>value</code> will be set to the value of the attribute, if it is
365 * set for <code>nv</code>; otherwise, it will be set to the default
366 * value of the attribute.
367 * @returns <code>true</code> iff <code>attr</code> is set for
370 template <class AttrKind
>
371 inline bool getAttribute(expr::NodeValue
* nv
,
372 const AttrKind
& attr
,
373 typename
AttrKind::value_type
& value
) const;
376 * Set an attribute for a node. If the node doesn't have the
377 * attribute, this function assigns one. If the node has one, this
380 * @param nv the node value
381 * @param attr an instance of the attribute kind to set
382 * @param value the value of <code>attr</code> for <code>nv</code>
384 template <class AttrKind
>
385 inline void setAttribute(expr::NodeValue
* nv
,
386 const AttrKind
& attr
,
387 const typename
AttrKind::value_type
& value
);
390 * Retrieve an attribute for a TNode.
393 * @param attr an instance of the attribute kind to retrieve.
394 * @returns the attribute, if set, or a default-constructed
395 * <code>AttrKind::value_type</code> if not.
397 template <class AttrKind
>
398 inline typename
AttrKind::value_type
399 getAttribute(TNode n
, const AttrKind
& attr
) const;
402 * Check whether an attribute is set for a TNode.
405 * @param attr an instance of the attribute kind to check
406 * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
408 template <class AttrKind
>
409 inline bool hasAttribute(TNode n
,
410 const AttrKind
& attr
) const;
413 * Check whether an attribute is set for a TNode and, if so, retieve
417 * @param attr an instance of the attribute kind to check
418 * @param value a reference to an object of the attribute's value type.
419 * <code>value</code> will be set to the value of the attribute, if it is
420 * set for <code>nv</code>; otherwise, it will be set to the default value of
422 * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
424 template <class AttrKind
>
425 inline bool getAttribute(TNode n
,
426 const AttrKind
& attr
,
427 typename
AttrKind::value_type
& value
) const;
430 * Set an attribute for a node. If the node doesn't have the
431 * attribute, this function assigns one. If the node has one, this
435 * @param attr an instance of the attribute kind to set
436 * @param value the value of <code>attr</code> for <code>n</code>
438 template <class AttrKind
>
439 inline void setAttribute(TNode n
,
440 const AttrKind
& attr
,
441 const typename
AttrKind::value_type
& value
);
443 /** Get the (singleton) type for Booleans. */
444 inline TypeNode
booleanType();
446 /** Get the (singleton) type for integers. */
447 inline TypeNode
integerType();
449 /** Get the (singleton) type for booleans. */
450 inline TypeNode
realType();
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
,
473 const TypeNode
& range
);
476 * Make a function type with input types from
477 * <code>sorts[0..sorts.size()-2]</code> and result type
478 * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
479 * at least 2 elements.
481 inline TypeNode
mkFunctionType(const std::vector
<TypeNode
>& sorts
);
484 * Make a predicate type with input types from
485 * <code>sorts</code>. The result with be a function type with range
486 * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
489 inline TypeNode
mkPredicateType(const std::vector
<TypeNode
>& sorts
);
492 * Make a tuple type with types from
493 * <code>types</code>. <code>types</code> must have at least two
496 * @param types a vector of types
497 * @returns the tuple type (types[0], ..., types[n])
499 inline TypeNode
mkTupleType(const std::vector
<TypeNode
>& types
);
501 /** Make the type of bitvectors of size <code>size</code> */
502 inline TypeNode
mkBitVectorType(unsigned size
);
504 /** Make the type of arrays with the given parameterization */
505 inline TypeNode
mkArrayType(TypeNode indexType
, TypeNode constituentType
);
507 /** Make a new sort. */
508 inline TypeNode
mkSort();
510 /** Make a new sort with the given name. */
511 inline TypeNode
mkSort(const std::string
& name
);
514 * Get the type for the given node and optionally do type checking.
516 * Initial type computation will be near-constant time if
517 * type checking is not requested. Results are memoized, so that
518 * subsequent calls to getType() without type checking will be
521 * Initial type checking is linear in the size of the expression.
522 * Again, the results are memoized, so that subsequent calls to
523 * getType(), with or without type checking, will be constant
526 * NOTE: A TypeCheckingException can be thrown even when type
527 * checking is not requested. getType() will always return a
528 * valid and correct type and, thus, an exception will be thrown
529 * when no valid or correct type can be computed (e.g., if the
530 * arguments to a bit-vector operation aren't bit-vectors). When
531 * type checking is not requested, getType() will do the minimum
532 * amount of checking required to return a valid result.
534 * @param n the Node for which we want a type
535 * @param check whether we should check the type as we compute it
538 TypeNode
getType(TNode n
, bool check
= false)
539 throw (TypeCheckingExceptionPrivate
, AssertionException
);
543 * This class changes the "current" thread-global
544 * <code>NodeManager</code> when it is created and reinstates the
545 * previous thread-global <code>NodeManager</code> when it is
546 * destroyed, effectively maintaining a set of nested
547 * <code>NodeManager</code> scopes. This is especially useful on
548 * public-interface calls into the CVC4 library, where CVC4's notion
549 * of the "current" <code>NodeManager</code> should be set to match
550 * the calling context. See, for example, the implementations of
551 * public calls in the <code>ExprManager</code> and
552 * <code>SmtEngine</code> classes.
554 * The client must be careful to create and destroy
555 * <code>NodeManagerScope</code> objects in a well-nested manner (such
556 * as on the stack). You may create a <code>NodeManagerScope</code>
557 * with <code>new</code> and destroy it with <code>delete</code>, or
558 * place it as a data member of an object that is, but if the scope of
559 * these <code>new</code>/<code>delete</code> pairs isn't properly
560 * maintained, the incorrect "current" <code>NodeManager</code>
561 * pointer may be restored after a delete.
563 class NodeManagerScope
{
564 /** The old NodeManager, to be restored on destruction. */
565 NodeManager
* d_oldNodeManager
;
569 NodeManagerScope(NodeManager
* nm
) :
570 d_oldNodeManager(NodeManager::s_current
) {
571 NodeManager::s_current
= nm
;
572 Debug("current") << "node manager scope: "
573 << NodeManager::s_current
<< "\n";
576 ~NodeManagerScope() {
577 NodeManager::s_current
= d_oldNodeManager
;
578 Debug("current") << "node manager scope: "
579 << "returning to " << NodeManager::s_current
<< "\n";
584 template <class AttrKind
>
585 inline typename
AttrKind::value_type
586 NodeManager::getAttribute(expr::NodeValue
* nv
, const AttrKind
&) const {
587 return d_attrManager
.getAttribute(nv
, AttrKind());
590 template <class AttrKind
>
591 inline bool NodeManager::hasAttribute(expr::NodeValue
* nv
,
592 const AttrKind
&) const {
593 return d_attrManager
.hasAttribute(nv
, AttrKind());
596 template <class AttrKind
>
598 NodeManager::getAttribute(expr::NodeValue
* nv
, const AttrKind
&,
599 typename
AttrKind::value_type
& ret
) const {
600 return d_attrManager
.getAttribute(nv
, AttrKind(), ret
);
603 template <class AttrKind
>
605 NodeManager::setAttribute(expr::NodeValue
* nv
, const AttrKind
&,
606 const typename
AttrKind::value_type
& value
) {
607 d_attrManager
.setAttribute(nv
, AttrKind(), value
);
610 template <class AttrKind
>
611 inline typename
AttrKind::value_type
612 NodeManager::getAttribute(TNode n
, const AttrKind
&) const {
613 return d_attrManager
.getAttribute(n
.d_nv
, AttrKind());
616 template <class AttrKind
>
618 NodeManager::hasAttribute(TNode n
, const AttrKind
&) const {
619 return d_attrManager
.hasAttribute(n
.d_nv
, AttrKind());
622 template <class AttrKind
>
624 NodeManager::getAttribute(TNode n
, const AttrKind
&,
625 typename
AttrKind::value_type
& ret
) const {
626 return d_attrManager
.getAttribute(n
.d_nv
, AttrKind(), ret
);
629 template <class AttrKind
>
631 NodeManager::setAttribute(TNode n
, const AttrKind
&,
632 const typename
AttrKind::value_type
& value
) {
633 d_attrManager
.setAttribute(n
.d_nv
, AttrKind(), value
);
637 /** Get the (singleton) type for booleans. */
638 inline TypeNode
NodeManager::booleanType() {
639 return TypeNode(mkTypeConst
<TypeConstant
>(BOOLEAN_TYPE
));
642 /** Get the (singleton) type for integers. */
643 inline TypeNode
NodeManager::integerType() {
644 return TypeNode(mkTypeConst
<TypeConstant
>(INTEGER_TYPE
));
647 /** Get the (singleton) type for reals. */
648 inline TypeNode
NodeManager::realType() {
649 return TypeNode(mkTypeConst
<TypeConstant
>(REAL_TYPE
));
652 /** Get the (singleton) type for sorts. */
653 inline TypeNode
NodeManager::kindType() {
654 return TypeNode(mkTypeConst
<TypeConstant
>(KIND_TYPE
));
657 /** Make a function type from domain to range. */
658 inline TypeNode
NodeManager::mkFunctionType(const TypeNode
& domain
, const TypeNode
& range
) {
659 std::vector
<TypeNode
> sorts
;
660 sorts
.push_back(domain
);
661 sorts
.push_back(range
);
662 return mkFunctionType(sorts
);
665 inline TypeNode
NodeManager::mkFunctionType(const std::vector
<TypeNode
>& argTypes
, const TypeNode
& range
) {
666 Assert(argTypes
.size() >= 1);
667 std::vector
<TypeNode
> sorts(argTypes
);
668 sorts
.push_back(range
);
669 return mkFunctionType(sorts
);
673 NodeManager::mkFunctionType(const std::vector
<TypeNode
>& sorts
) {
674 Assert(sorts
.size() >= 2);
675 std::vector
<TypeNode
> sortNodes
;
676 for (unsigned i
= 0; i
< sorts
.size(); ++ i
) {
677 sortNodes
.push_back(sorts
[i
]);
679 return mkTypeNode(kind::FUNCTION_TYPE
, sortNodes
);
683 NodeManager::mkPredicateType(const std::vector
<TypeNode
>& sorts
) {
684 Assert(sorts
.size() >= 1);
685 std::vector
<TypeNode
> sortNodes
;
686 for (unsigned i
= 0; i
< sorts
.size(); ++ i
) {
687 sortNodes
.push_back(sorts
[i
]);
689 sortNodes
.push_back(booleanType());
690 return mkTypeNode(kind::FUNCTION_TYPE
, sortNodes
);
693 inline TypeNode
NodeManager::mkTupleType(const std::vector
<TypeNode
>& types
) {
694 Assert(types
.size() >= 2);
695 std::vector
<TypeNode
> typeNodes
;
696 for (unsigned i
= 0; i
< types
.size(); ++ i
) {
697 typeNodes
.push_back(types
[i
]);
699 return mkTypeNode(kind::TUPLE_TYPE
, typeNodes
);
702 inline TypeNode
NodeManager::mkBitVectorType(unsigned size
) {
703 return TypeNode(mkTypeConst
<BitVectorSize
>(BitVectorSize(size
)));
706 inline TypeNode
NodeManager::mkArrayType(TypeNode indexType
,
707 TypeNode constituentType
) {
708 return mkTypeNode(kind::ARRAY_TYPE
, indexType
, constituentType
);
711 inline expr::NodeValue
* NodeManager::poolLookup(expr::NodeValue
* nv
) const {
712 NodeValuePool::const_iterator find
= d_nodeValuePool
.find(nv
);
713 if(find
== d_nodeValuePool
.end()) {
720 inline void NodeManager::poolInsert(expr::NodeValue
* nv
) {
721 Assert(d_nodeValuePool
.find(nv
) == d_nodeValuePool
.end(),
722 "NodeValue already in the pool!");
723 d_nodeValuePool
.insert(nv
);// FIXME multithreading
726 inline void NodeManager::poolRemove(expr::NodeValue
* nv
) {
727 Assert(d_nodeValuePool
.find(nv
) != d_nodeValuePool
.end(),
728 "NodeValue is not in the pool!");
730 d_nodeValuePool
.erase(nv
);// FIXME multithreading
733 }/* CVC4 namespace */
735 #define __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
736 #include "expr/metakind.h"
737 #undef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
739 #include "expr/node_builder.h"
743 // general expression-builders
745 inline bool NodeManager::hasOperator(Kind k
) {
746 switch(kind::MetaKind mk
= kind::metaKindOf(k
)) {
748 case kind::metakind::INVALID
:
749 case kind::metakind::VARIABLE
:
752 case kind::metakind::OPERATOR
:
753 case kind::metakind::PARAMETERIZED
:
756 case kind::metakind::CONSTANT
:
764 inline TypeNode
NodeManager::mkSort() {
765 return NodeBuilder
<0>(this, kind::SORT_TYPE
).constructTypeNode();
768 inline TypeNode
NodeManager::mkSort(const std::string
& name
) {
769 TypeNode type
= mkSort();
770 type
.setAttribute(expr::VarNameAttr(), name
);
774 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
) {
775 NodeBuilder
<1> nb(this, kind
);
777 return nb
.constructNode();
780 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
) {
781 NodeBuilder
<1> nb(this, kind
);
783 return nb
.constructNodePtr();
786 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
, TNode child2
) {
787 NodeBuilder
<2> nb(this, kind
);
788 nb
<< child1
<< child2
;
789 return nb
.constructNode();
792 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
, TNode child2
) {
793 NodeBuilder
<2> nb(this, kind
);
794 nb
<< child1
<< child2
;
795 return nb
.constructNodePtr();
798 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
, TNode child2
,
800 NodeBuilder
<3> nb(this, kind
);
801 nb
<< child1
<< child2
<< child3
;
802 return nb
.constructNode();
805 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
, TNode child2
,
807 NodeBuilder
<3> nb(this, kind
);
808 nb
<< child1
<< child2
<< child3
;
809 return nb
.constructNodePtr();
812 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
, TNode child2
,
813 TNode child3
, TNode child4
) {
814 NodeBuilder
<4> nb(this, kind
);
815 nb
<< child1
<< child2
<< child3
<< child4
;
816 return nb
.constructNode();
819 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
, TNode child2
,
820 TNode child3
, TNode child4
) {
821 NodeBuilder
<4> nb(this, kind
);
822 nb
<< child1
<< child2
<< child3
<< child4
;
823 return nb
.constructNodePtr();
826 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
, TNode child2
,
827 TNode child3
, TNode child4
, TNode child5
) {
828 NodeBuilder
<5> nb(this, kind
);
829 nb
<< child1
<< child2
<< child3
<< child4
<< child5
;
830 return nb
.constructNode();
833 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
, TNode child2
,
834 TNode child3
, TNode child4
, TNode child5
) {
835 NodeBuilder
<5> nb(this, kind
);
836 nb
<< child1
<< child2
<< child3
<< child4
<< child5
;
837 return nb
.constructNodePtr();
841 template <bool ref_count
>
842 inline Node
NodeManager::mkNode(Kind kind
,
843 const std::vector
<NodeTemplate
<ref_count
> >&
845 NodeBuilder
<> nb(this, kind
);
847 return nb
.constructNode();
850 template <bool ref_count
>
851 inline Node
* NodeManager::mkNodePtr(Kind kind
,
852 const std::vector
<NodeTemplate
<ref_count
> >&
854 NodeBuilder
<> nb(this, kind
);
856 return nb
.constructNodePtr();
859 // N-ary version for operators
860 template <bool ref_count
>
861 inline Node
NodeManager::mkNode(TNode opNode
,
862 const std::vector
<NodeTemplate
<ref_count
> >&
864 NodeBuilder
<> nb(this, kind::operatorKindToKind(opNode
.getKind()));
867 return nb
.constructNode();
870 template <bool ref_count
>
871 inline Node
* NodeManager::mkNodePtr(TNode opNode
,
872 const std::vector
<NodeTemplate
<ref_count
> >&
874 NodeBuilder
<> nb(this, kind::operatorKindToKind(opNode
.getKind()));
877 return nb
.constructNodePtr();
881 inline TypeNode
NodeManager::mkTypeNode(Kind kind
, TypeNode child1
) {
882 return (NodeBuilder
<1>(this, kind
) << child1
).constructTypeNode();
885 inline TypeNode
NodeManager::mkTypeNode(Kind kind
, TypeNode child1
,
887 return (NodeBuilder
<2>(this, kind
) << child1
<< child2
).constructTypeNode();
890 inline TypeNode
NodeManager::mkTypeNode(Kind kind
, TypeNode child1
,
891 TypeNode child2
, TypeNode child3
) {
892 return (NodeBuilder
<3>(this, kind
) << child1
<< child2
<< child3
).constructTypeNode();;
895 // N-ary version for types
896 inline TypeNode
NodeManager::mkTypeNode(Kind kind
,
897 const std::vector
<TypeNode
>& children
) {
898 return NodeBuilder
<>(this, kind
).append(children
).constructTypeNode();
902 inline Node
NodeManager::mkVar(const std::string
& name
, const TypeNode
& type
) {
903 Node n
= mkVar(type
);
904 n
.setAttribute(expr::VarNameAttr(), name
);
908 inline Node
* NodeManager::mkVarPtr(const std::string
& name
,
909 const TypeNode
& type
) {
910 Node
* n
= mkVarPtr(type
);
911 n
->setAttribute(expr::VarNameAttr(), name
);
915 inline Node
NodeManager::mkVar(const TypeNode
& type
) {
916 Node n
= NodeBuilder
<0>(this, kind::VARIABLE
);
917 n
.setAttribute(TypeAttr(), type
);
918 n
.setAttribute(TypeCheckedAttr(), true);
922 inline Node
* NodeManager::mkVarPtr(const TypeNode
& type
) {
923 Node
* n
= NodeBuilder
<0>(this, kind::VARIABLE
).constructNodePtr();
924 n
->setAttribute(TypeAttr(), type
);
925 n
->setAttribute(TypeCheckedAttr(), true);
929 inline Node
NodeManager::mkSkolem(const TypeNode
& type
) {
930 Node n
= NodeBuilder
<0>(this, kind::SKOLEM
);
931 n
.setAttribute(TypeAttr(), type
);
932 n
.setAttribute(TypeCheckedAttr(), true);
937 Node
NodeManager::mkConst(const T
& val
) {
938 return mkConstInternal
<Node
, T
>(val
);
942 TypeNode
NodeManager::mkTypeConst(const T
& val
) {
943 return mkConstInternal
<TypeNode
, T
>(val
);
946 template <class NodeClass
, class T
>
947 NodeClass
NodeManager::mkConstInternal(const T
& val
) {
949 // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
950 NVStorage
<1> nvStorage
;
951 expr::NodeValue
& nvStack
= reinterpret_cast<expr::NodeValue
&>(nvStorage
);
954 nvStack
.d_kind
= kind::metakind::ConstantMap
<T
>::kind
;
956 nvStack
.d_nchildren
= 1;
957 nvStack
.d_children
[0] =
958 const_cast<expr::NodeValue
*>(reinterpret_cast<const expr::NodeValue
*>(&val
));
959 expr::NodeValue
* nv
= poolLookup(&nvStack
);
962 return NodeClass(nv
);
965 nv
= (expr::NodeValue
*)
966 std::malloc(sizeof(expr::NodeValue
) + sizeof(T
));
968 throw std::bad_alloc();
972 nv
->d_kind
= kind::metakind::ConstantMap
<T
>::kind
;
973 nv
->d_id
= expr::NodeValue::next_id
++;// FIXME multithreading
976 //OwningTheory::mkConst(val);
977 new (&nv
->d_children
) T(val
);
980 Debug("gc") << "creating node value " << nv
981 << " [" << nv
->d_id
<< "]: " << *nv
<< "\n";
983 return NodeClass(nv
);
986 }/* CVC4 namespace */
988 #endif /* __CVC4__EXPR_MANAGER_H */