1 /********************* */
2 /*! \file node_manager.h
4 ** Top contributors (to current version):
5 ** Morgan Deters, Christopher L. Conway, Dejan Jovanovic
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief A manager for Nodes
14 ** A manager for Nodes.
16 ** Reviewed by Chris Conway, Apr 5 2010 (bug #65).
19 #include "cvc4_private.h"
21 /* circular dependency; force node.h first */
22 //#include "expr/attribute.h"
23 #include "expr/node.h"
24 #include "expr/type_node.h"
25 #include "expr/expr.h"
26 #include "expr/expr_manager.h"
28 #ifndef CVC4__NODE_MANAGER_H
29 #define CVC4__NODE_MANAGER_H
33 #include <unordered_set>
35 #include "expr/kind.h"
36 #include "expr/metakind.h"
37 #include "expr/node_value.h"
38 #include "options/options.h"
42 class StatisticsRegistry
;
43 class ResourceManager
;
47 class AttributeUniqueId
;
48 class AttributeManager
;
49 }/* CVC4::expr::attr namespace */
52 }/* CVC4::expr namespace */
55 * An interface that an interested party can implement and then subscribe
56 * to NodeManager events via NodeManager::subscribeEvents(this).
58 class NodeManagerListener
{
60 virtual ~NodeManagerListener() {}
61 virtual void nmNotifyNewSort(TypeNode tn
, uint32_t flags
) {}
62 virtual void nmNotifyNewSortConstructor(TypeNode tn
, uint32_t flags
) {}
63 virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor
, TypeNode sort
,
65 virtual void nmNotifyNewDatatypes(const std::vector
<DatatypeType
>& datatypes
,
69 virtual void nmNotifyNewVar(TNode n
, uint32_t flags
) {}
70 virtual void nmNotifyNewSkolem(TNode n
, const std::string
& comment
,
73 * Notify a listener of a Node that's being GCed. If this function stores a
75 * to the Node somewhere, very bad things will happen.
77 virtual void nmNotifyDeleteNode(TNode n
) {}
78 }; /* class NodeManagerListener */
81 template <unsigned nchild_thresh
> friend class CVC4::NodeBuilder
;
82 friend class NodeManagerScope
;
83 friend class expr::NodeValue
;
84 friend class expr::TypeChecker
;
86 // friends so they can access mkVar() here, which is private
87 friend Expr
ExprManager::mkVar(const std::string
&, Type
, uint32_t flags
);
88 friend Expr
ExprManager::mkVar(Type
, uint32_t flags
);
90 // friend so it can access NodeManager's d_listeners and notify clients
91 friend std::vector
<DatatypeType
> ExprManager::mkMutualDatatypeTypes(
92 std::vector
<Datatype
>&, std::set
<Type
>&, uint32_t);
94 /** Predicate for use with STL algorithms */
95 struct NodeValueReferenceCountNonZero
{
96 bool operator()(expr::NodeValue
* nv
) { return nv
->d_rc
> 0; }
99 typedef std::unordered_set
<expr::NodeValue
*,
100 expr::NodeValuePoolHashFunction
,
101 expr::NodeValuePoolEq
> NodeValuePool
;
102 typedef std::unordered_set
<expr::NodeValue
*,
103 expr::NodeValueIDHashFunction
,
104 expr::NodeValueIDEquality
> NodeValueIDSet
;
106 static thread_local NodeManager
* s_current
;
109 StatisticsRegistry
* d_statisticsRegistry
;
111 ResourceManager
* d_resourceManager
;
114 * A list of registrations on d_options to that call into d_resourceManager.
115 * These must be garbage collected before d_options and d_resourceManager.
117 ListenerRegistrationList
* d_registrations
;
119 NodeValuePool d_nodeValuePool
;
123 expr::attr::AttributeManager
* d_attrManager
;
125 /** The associated ExprManager */
126 ExprManager
* d_exprManager
;
129 * The node value we're currently freeing. This unique node value
130 * is permitted to have outstanding TNodes to it (in "soft"
131 * contexts, like as a key in attribute tables), even though
132 * normally it's an error to have a TNode to a node value with a
133 * reference count of 0. Being "under deletion" also enables
134 * assertions that inc() is not called on it.
136 expr::NodeValue
* d_nodeUnderDeletion
;
139 * True iff we are in reclaimZombies(). This avoids unnecessary
140 * recursion; a NodeValue being deleted might zombify other
141 * NodeValues, but these shouldn't trigger a (recursive) call to
144 bool d_inReclaimZombies
;
147 * The set of zombie nodes. We may want to revisit this design, as
148 * we might like to delete nodes in least-recently-used order. But
149 * we also need to avoid processing a zombie twice.
151 NodeValueIDSet d_zombies
;
154 * NodeValues with maxed out reference counts. These live as long as the
155 * NodeManager. They have a custom deallocation procedure at the very end.
157 std::vector
<expr::NodeValue
*> d_maxedOut
;
160 * A set of operator singletons (w.r.t. to this NodeManager
161 * instance) for operators. Conceptually, Nodes with kind, say,
162 * PLUS, are APPLYs of a PLUS operator to arguments. This array
163 * holds the set of operators for these things. A PLUS operator is
164 * a Node with kind "BUILTIN", and if you call
165 * plusOperator->getConst<CVC4::Kind>(), you get kind::PLUS back.
167 Node d_operators
[kind::LAST_KIND
];
169 /** unique vars per (Kind,Type) */
170 std::map
< Kind
, std::map
< TypeNode
, Node
> > d_unique_vars
;
173 * A list of subscribers for NodeManager events.
175 std::vector
<NodeManagerListener
*> d_listeners
;
177 /** A list of datatypes owned by this node manager. */
178 std::vector
<Datatype
*> d_ownedDatatypes
;
181 * A map of tuple and record types to their corresponding datatype.
183 class TupleTypeCache
{
185 std::map
< TypeNode
, TupleTypeCache
> d_children
;
187 TypeNode
getTupleType( NodeManager
* nm
, std::vector
< TypeNode
>& types
, unsigned index
= 0 );
191 std::map
< TypeNode
, std::map
< std::string
, RecTypeCache
> > d_children
;
193 TypeNode
getRecordType( NodeManager
* nm
, const Record
& rec
, unsigned index
= 0 );
195 TupleTypeCache d_tt_cache
;
196 RecTypeCache d_rt_cache
;
199 * Keep a count of all abstract values produced by this NodeManager.
200 * Abstract values have a type attribute, so if multiple SmtEngines
201 * are attached to this NodeManager, we don't want their abstract
204 unsigned d_abstractValueCount
;
207 * A counter used to produce unique skolem names.
209 * Note that it is NOT incremented when skolems are created using
210 * SKOLEM_EXACT_NAME, so it is NOT a count of the skolems produced
211 * by this node manager.
213 unsigned d_skolemCounter
;
216 * Look up a NodeValue in the pool associated to this NodeManager.
217 * The NodeValue argument need not be a "completely-constructed"
218 * NodeValue. In particular, "non-inlined" constants are permitted
221 * For non-CONSTANT metakinds, nv's d_kind and d_nchildren should be
222 * correctly set, and d_children[0..n-1] should be valid (extant)
223 * NodeValues for lookup.
225 * For CONSTANT metakinds, nv's d_kind should be set correctly.
226 * Normally a CONSTANT would have d_nchildren == 0 and the constant
227 * value inlined in the d_children space. However, here we permit
228 * "non-inlined" NodeValues to avoid unnecessary copying. For
229 * these, d_nchildren == 1, and d_nchildren is a pointer to the
232 * The point of this complex design is to permit efficient lookups
233 * (without fully constructing a NodeValue). In the case that the
234 * argument is not fully constructed, and this function returns
235 * NULL, the caller should fully construct an equivalent one before
236 * calling poolInsert(). NON-FULLY-CONSTRUCTED NODEVALUES are not
237 * permitted in the pool!
239 inline expr::NodeValue
* poolLookup(expr::NodeValue
* nv
) const;
242 * Insert a NodeValue into the NodeManager's pool.
244 * It is an error to insert a NodeValue already in the pool.
245 * Enquire first with poolLookup().
247 inline void poolInsert(expr::NodeValue
* nv
);
250 * Remove a NodeValue from the NodeManager's pool.
252 * It is an error to request the removal of a NodeValue from the
253 * pool that is not in the pool.
255 inline void poolRemove(expr::NodeValue
* nv
);
258 * Determine if nv is currently being deleted by the NodeManager.
260 inline bool isCurrentlyDeleting(const expr::NodeValue
* nv
) const {
261 return d_nodeUnderDeletion
== nv
;
265 * Register a NodeValue as a zombie.
267 inline void markForDeletion(expr::NodeValue
* nv
) {
268 Assert(nv
->d_rc
== 0);
270 // if d_reclaiming is set, make sure we don't call
271 // reclaimZombies(), because it's already running.
272 if(Debug
.isOn("gc")) {
273 Debug("gc") << "zombifying node value " << nv
274 << " [" << nv
->d_id
<< "]: ";
275 nv
->printAst(Debug("gc"));
276 Debug("gc") << (d_inReclaimZombies
? " [CURRENTLY-RECLAIMING]" : "")
280 // `d_zombies` uses the node id to hash and compare nodes. If `d_zombies`
281 // already contains a node value with the same id as `nv`, but the pointers
282 // are different, then the wrong `NodeManager` was in scope for one of the
283 // two nodes when it reached refcount zero. This can happen for example if
284 // you create a node with a `NodeManager` n1 and then call `Node::toExpr()`
285 // on that node while a different `NodeManager` n2 is in scope. When that
286 // `Expr` is deleted and the node reaches refcount zero in the `Expr`'s
287 // destructor, then `markForDeletion()` will be called on n2.
288 Assert(d_zombies
.find(nv
) == d_zombies
.end() || *d_zombies
.find(nv
) == nv
);
290 d_zombies
.insert(nv
); // FIXME multithreading
292 if(safeToReclaimZombies()) {
293 if(d_zombies
.size() > 5000) {
300 * Register a NodeValue as having a maxed out reference count. This NodeValue
301 * will live as long as its containing NodeManager.
303 inline void markRefCountMaxedOut(expr::NodeValue
* nv
) {
304 Assert(nv
->HasMaximizedReferenceCount());
305 if(Debug
.isOn("gc")) {
306 Debug("gc") << "marking node value " << nv
307 << " [" << nv
->d_id
<< "]: as maxed out" << std::endl
;
309 d_maxedOut
.push_back(nv
);
313 * Reclaim all zombies.
315 void reclaimZombies();
318 * It is safe to collect zombies.
320 bool safeToReclaimZombies() const;
323 * Returns a reverse topological sort of a list of NodeValues. The NodeValues
324 * must be valid and have ids. The NodeValues are not modified (including ref
327 static std::vector
<expr::NodeValue
*> TopologicalSort(
328 const std::vector
<expr::NodeValue
*>& roots
);
331 * This template gives a mechanism to stack-allocate a NodeValue
332 * with enough space for N children (where N is a compile-time
333 * constant). You use it like this:
335 * NVStorage<4> nvStorage;
336 * NodeValue& nvStack = reinterpret_cast<NodeValue&>(nvStorage);
338 * ...and then you can use nvStack as a NodeValue that you know has
339 * room for 4 children.
344 expr::NodeValue
* child
[N
];
345 };/* struct NodeManager::NVStorage<N> */
347 /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
349 * It has been decided for now to hold off on implementations of
350 * these functions, as they may only be needed in CNF conversion,
351 * where it's pointless to do a lazy isAtomic determination by
352 * searching through the DAG, and storing it, since the result will
353 * only be used once. For more details see the 4/27/2010 CVC4
354 * developer's meeting notes at:
356 * http://cvc4.cs.stanford.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
358 // bool containsDecision(TNode); // is "atomic"
359 // bool properlyContainsDecision(TNode); // all children are atomic
361 // undefined private copy constructor (disallow copy)
362 NodeManager(const NodeManager
&) = delete;
364 NodeManager
& operator=(const NodeManager
&) = delete;
369 * Create a variable with the given name and type. NOTE that no
370 * lookup is done on the name. If you mkVar("a", type) and then
371 * mkVar("a", type) again, you have two variables. The NodeManager
372 * version of this is private to avoid internal uses of mkVar() from
373 * within CVC4. Such uses should employ mkSkolem() instead.
375 Node
mkVar(const std::string
& name
, const TypeNode
& type
, uint32_t flags
= ExprManager::VAR_FLAG_NONE
);
376 Node
* mkVarPtr(const std::string
& name
, const TypeNode
& type
, uint32_t flags
= ExprManager::VAR_FLAG_NONE
);
378 /** Create a variable with the given type. */
379 Node
mkVar(const TypeNode
& type
, uint32_t flags
= ExprManager::VAR_FLAG_NONE
);
380 Node
* mkVarPtr(const TypeNode
& type
, uint32_t flags
= ExprManager::VAR_FLAG_NONE
);
384 explicit NodeManager(ExprManager
* exprManager
);
385 explicit NodeManager(ExprManager
* exprManager
, const Options
& options
);
388 /** The node manager in the current public-facing CVC4 library context */
389 static NodeManager
* currentNM() { return s_current
; }
390 /** The resource manager associated with the current node manager */
391 static ResourceManager
* currentResourceManager() { return s_current
->d_resourceManager
; }
393 /** Get this node manager's options (const version) */
394 const Options
& getOptions() const {
398 /** Get this node manager's options (non-const version) */
399 Options
& getOptions() {
403 /** Get this node manager's resource manager */
404 ResourceManager
* getResourceManager() { return d_resourceManager
; }
406 /** Get this node manager's statistics registry */
407 StatisticsRegistry
* getStatisticsRegistry() const
409 return d_statisticsRegistry
;
412 /** Subscribe to NodeManager events */
413 void subscribeEvents(NodeManagerListener
* listener
) {
414 Assert(std::find(d_listeners
.begin(), d_listeners
.end(), listener
) == d_listeners
.end(), "listener already subscribed");
415 d_listeners
.push_back(listener
);
418 /** Unsubscribe from NodeManager events */
419 void unsubscribeEvents(NodeManagerListener
* listener
) {
420 std::vector
<NodeManagerListener
*>::iterator elt
= std::find(d_listeners
.begin(), d_listeners
.end(), listener
);
421 Assert(elt
!= d_listeners
.end(), "listener not subscribed");
422 d_listeners
.erase(elt
);
425 /** register datatype */
426 unsigned registerDatatype(Datatype
* dt
);
427 /** get datatype for index */
428 const Datatype
& getDatatypeForIndex( unsigned index
) const;
430 /** Get a Kind from an operator expression */
431 static inline Kind
operatorToKind(TNode n
);
433 // general expression-builders
435 /** Create a node with one child. */
436 Node
mkNode(Kind kind
, TNode child1
);
437 Node
* mkNodePtr(Kind kind
, TNode child1
);
439 /** Create a node with two children. */
440 Node
mkNode(Kind kind
, TNode child1
, TNode child2
);
441 Node
* mkNodePtr(Kind kind
, TNode child1
, TNode child2
);
443 /** Create a node with three children. */
444 Node
mkNode(Kind kind
, TNode child1
, TNode child2
, TNode child3
);
445 Node
* mkNodePtr(Kind kind
, TNode child1
, TNode child2
, TNode child3
);
447 /** Create a node with four children. */
448 Node
mkNode(Kind kind
, TNode child1
, TNode child2
, TNode child3
,
450 Node
* mkNodePtr(Kind kind
, TNode child1
, TNode child2
, TNode child3
,
453 /** Create a node with five children. */
454 Node
mkNode(Kind kind
, TNode child1
, TNode child2
, TNode child3
,
455 TNode child4
, TNode child5
);
456 Node
* mkNodePtr(Kind kind
, TNode child1
, TNode child2
, TNode child3
,
457 TNode child4
, TNode child5
);
459 /** Create a node with an arbitrary number of children. */
460 template <bool ref_count
>
461 Node
mkNode(Kind kind
, const std::vector
<NodeTemplate
<ref_count
> >& children
);
462 template <bool ref_count
>
463 Node
* mkNodePtr(Kind kind
, const std::vector
<NodeTemplate
<ref_count
> >& children
);
465 /** Create a node (with no children) by operator. */
466 Node
mkNode(TNode opNode
);
467 Node
* mkNodePtr(TNode opNode
);
469 /** Create a node with one child by operator. */
470 Node
mkNode(TNode opNode
, TNode child1
);
471 Node
* mkNodePtr(TNode opNode
, TNode child1
);
473 /** Create a node with two children by operator. */
474 Node
mkNode(TNode opNode
, TNode child1
, TNode child2
);
475 Node
* mkNodePtr(TNode opNode
, TNode child1
, TNode child2
);
477 /** Create a node with three children by operator. */
478 Node
mkNode(TNode opNode
, TNode child1
, TNode child2
, TNode child3
);
479 Node
* mkNodePtr(TNode opNode
, TNode child1
, TNode child2
, TNode child3
);
481 /** Create a node with four children by operator. */
482 Node
mkNode(TNode opNode
, TNode child1
, TNode child2
, TNode child3
,
484 Node
* mkNodePtr(TNode opNode
, TNode child1
, TNode child2
, TNode child3
,
487 /** Create a node with five children by operator. */
488 Node
mkNode(TNode opNode
, TNode child1
, TNode child2
, TNode child3
,
489 TNode child4
, TNode child5
);
490 Node
* mkNodePtr(TNode opNode
, TNode child1
, TNode child2
, TNode child3
,
491 TNode child4
, TNode child5
);
493 /** Create a node by applying an operator to the children. */
494 template <bool ref_count
>
495 Node
mkNode(TNode opNode
, const std::vector
<NodeTemplate
<ref_count
> >& children
);
496 template <bool ref_count
>
497 Node
* mkNodePtr(TNode opNode
, const std::vector
<NodeTemplate
<ref_count
> >& children
);
499 Node
mkBoundVar(const std::string
& name
, const TypeNode
& type
);
500 Node
* mkBoundVarPtr(const std::string
& name
, const TypeNode
& type
);
502 Node
mkBoundVar(const TypeNode
& type
);
503 Node
* mkBoundVarPtr(const TypeNode
& type
);
505 /** get the canonical bound variable list for function type tn */
506 static Node
getBoundVarListForFunctionType( TypeNode tn
);
509 * Optional flags used to control behavior of NodeManager::mkSkolem().
510 * They should be composed with a bitwise OR (e.g.,
511 * "SKOLEM_NO_NOTIFY | SKOLEM_EXACT_NAME"). Of course, SKOLEM_DEFAULT
512 * cannot be composed in such a manner.
515 SKOLEM_DEFAULT
= 0, /**< default behavior */
516 SKOLEM_NO_NOTIFY
= 1, /**< do not notify subscribers */
517 SKOLEM_EXACT_NAME
= 2,/**< do not make the name unique by adding the id */
518 SKOLEM_IS_GLOBAL
= 4 /**< global vars appear in models even after a pop */
519 };/* enum SkolemFlags */
522 * Create a skolem constant with the given name, type, and comment.
524 * @param prefix the name of the new skolem variable is the prefix
525 * appended with a unique ID. This way a family of skolem variables
526 * can be made with unique identifiers, used in dump, tracing, and
527 * debugging output. Use SKOLEM_EXECT_NAME flag if you don't want
528 * a unique ID appended and use prefix as the name.
530 * @param type the type of the skolem variable to create
532 * @param comment a comment for dumping output; if declarations are
533 * being dumped, this is included in a comment before the declaration
534 * and can be quite useful for debugging
536 * @param flags an optional mask of bits from SkolemFlags to control
537 * mkSkolem() behavior
539 Node
mkSkolem(const std::string
& prefix
, const TypeNode
& type
,
540 const std::string
& comment
= "", int flags
= SKOLEM_DEFAULT
);
542 /** Create a instantiation constant with the given type. */
543 Node
mkInstConstant(const TypeNode
& type
);
545 /** Create a boolean term variable. */
546 Node
mkBooleanTermVariable();
548 /** Make a new abstract value with the given type. */
549 Node
mkAbstractValue(const TypeNode
& type
);
551 /** make unique (per Type,Kind) variable. */
552 Node
mkNullaryOperator(const TypeNode
& type
, Kind k
);
555 * Create a constant of type T. It will have the appropriate
556 * CONST_* kind defined for T.
559 Node
mkConst(const T
&);
562 TypeNode
mkTypeConst(const T
&);
564 template <class NodeClass
, class T
>
565 NodeClass
mkConstInternal(const T
&);
567 /** Create a node with children. */
568 TypeNode
mkTypeNode(Kind kind
, TypeNode child1
);
569 TypeNode
mkTypeNode(Kind kind
, TypeNode child1
, TypeNode child2
);
570 TypeNode
mkTypeNode(Kind kind
, TypeNode child1
, TypeNode child2
,
572 TypeNode
mkTypeNode(Kind kind
, const std::vector
<TypeNode
>& children
);
575 * Determine whether Nodes of a particular Kind have operators.
576 * @returns true if Nodes of Kind k have operators.
578 static inline bool hasOperator(Kind k
);
581 * Get the (singleton) operator of an OPERATOR-kinded kind. The
582 * returned node n will have kind BUILTIN, and calling
583 * n.getConst<CVC4::Kind>() will yield k.
585 inline TNode
operatorOf(Kind k
) {
586 AssertArgument( kind::metaKindOf(k
) == kind::metakind::OPERATOR
, k
,
587 "Kind is not an OPERATOR-kinded kind "
588 "in NodeManager::operatorOf()" );
589 return d_operators
[k
];
593 * Retrieve an attribute for a node.
595 * @param nv the node value
596 * @param attr an instance of the attribute kind to retrieve.
597 * @returns the attribute, if set, or a default-constructed
598 * <code>AttrKind::value_type</code> if not.
600 template <class AttrKind
>
601 inline typename
AttrKind::value_type
getAttribute(expr::NodeValue
* nv
,
602 const AttrKind
& attr
) const;
605 * Check whether an attribute is set for a node.
607 * @param nv the node value
608 * @param attr an instance of the attribute kind to check
609 * @returns <code>true</code> iff <code>attr</code> is set for
612 template <class AttrKind
>
613 inline bool hasAttribute(expr::NodeValue
* nv
,
614 const AttrKind
& attr
) const;
617 * Check whether an attribute is set for a node, and, if so,
620 * @param nv the node value
621 * @param attr an instance of the attribute kind to check
622 * @param value a reference to an object of the attribute's value type.
623 * <code>value</code> will be set to the value of the attribute, if it is
624 * set for <code>nv</code>; otherwise, it will be set to the default
625 * value of the attribute.
626 * @returns <code>true</code> iff <code>attr</code> is set for
629 template <class AttrKind
>
630 inline bool getAttribute(expr::NodeValue
* nv
,
631 const AttrKind
& attr
,
632 typename
AttrKind::value_type
& value
) const;
635 * Set an attribute for a node. If the node doesn't have the
636 * attribute, this function assigns one. If the node has one, this
639 * @param nv the node value
640 * @param attr an instance of the attribute kind to set
641 * @param value the value of <code>attr</code> for <code>nv</code>
643 template <class AttrKind
>
644 inline void setAttribute(expr::NodeValue
* nv
,
645 const AttrKind
& attr
,
646 const typename
AttrKind::value_type
& value
);
649 * Retrieve an attribute for a TNode.
652 * @param attr an instance of the attribute kind to retrieve.
653 * @returns the attribute, if set, or a default-constructed
654 * <code>AttrKind::value_type</code> if not.
656 template <class AttrKind
>
657 inline typename
AttrKind::value_type
658 getAttribute(TNode n
, const AttrKind
& attr
) const;
661 * Check whether an attribute is set for a TNode.
664 * @param attr an instance of the attribute kind to check
665 * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
667 template <class AttrKind
>
668 inline bool hasAttribute(TNode n
,
669 const AttrKind
& attr
) const;
672 * Check whether an attribute is set for a TNode and, if so, retieve
676 * @param attr an instance of the attribute kind to check
677 * @param value a reference to an object of the attribute's value type.
678 * <code>value</code> will be set to the value of the attribute, if it is
679 * set for <code>nv</code>; otherwise, it will be set to the default value of
681 * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
683 template <class AttrKind
>
684 inline bool getAttribute(TNode n
,
685 const AttrKind
& attr
,
686 typename
AttrKind::value_type
& value
) const;
689 * Set an attribute for a node. If the node doesn't have the
690 * attribute, this function assigns one. If the node has one, this
694 * @param attr an instance of the attribute kind to set
695 * @param value the value of <code>attr</code> for <code>n</code>
697 template <class AttrKind
>
698 inline void setAttribute(TNode n
,
699 const AttrKind
& attr
,
700 const typename
AttrKind::value_type
& value
);
703 * Retrieve an attribute for a TypeNode.
705 * @param n the type node
706 * @param attr an instance of the attribute kind to retrieve.
707 * @returns the attribute, if set, or a default-constructed
708 * <code>AttrKind::value_type</code> if not.
710 template <class AttrKind
>
711 inline typename
AttrKind::value_type
712 getAttribute(TypeNode n
, const AttrKind
& attr
) const;
715 * Check whether an attribute is set for a TypeNode.
717 * @param n the type node
718 * @param attr an instance of the attribute kind to check
719 * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
721 template <class AttrKind
>
722 inline bool hasAttribute(TypeNode n
,
723 const AttrKind
& attr
) const;
726 * Check whether an attribute is set for a TypeNode and, if so, retieve
729 * @param n the type node
730 * @param attr an instance of the attribute kind to check
731 * @param value a reference to an object of the attribute's value type.
732 * <code>value</code> will be set to the value of the attribute, if it is
733 * set for <code>nv</code>; otherwise, it will be set to the default value of
735 * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
737 template <class AttrKind
>
738 inline bool getAttribute(TypeNode n
,
739 const AttrKind
& attr
,
740 typename
AttrKind::value_type
& value
) const;
743 * Set an attribute for a type node. If the node doesn't have the
744 * attribute, this function assigns one. If the type node has one,
745 * this overwrites it.
747 * @param n the type node
748 * @param attr an instance of the attribute kind to set
749 * @param value the value of <code>attr</code> for <code>n</code>
751 template <class AttrKind
>
752 inline void setAttribute(TypeNode n
,
753 const AttrKind
& attr
,
754 const typename
AttrKind::value_type
& value
);
756 /** Get the (singleton) type for Booleans. */
757 inline TypeNode
booleanType();
759 /** Get the (singleton) type for integers. */
760 inline TypeNode
integerType();
762 /** Get the (singleton) type for reals. */
763 inline TypeNode
realType();
765 /** Get the (singleton) type for strings. */
766 inline TypeNode
stringType();
768 /** Get the (singleton) type for RegExp. */
769 inline TypeNode
regExpType();
771 /** Get the (singleton) type for rounding modes. */
772 inline TypeNode
roundingModeType();
774 /** Get the bound var list type. */
775 inline TypeNode
boundVarListType();
777 /** Get the instantiation pattern type. */
778 inline TypeNode
instPatternType();
780 /** Get the instantiation pattern type. */
781 inline TypeNode
instPatternListType();
784 * Get the (singleton) type for builtin operators (that is, the type
785 * of the Node returned from Node::getOperator() when the operator
786 * is built-in, like EQUAL). */
787 inline TypeNode
builtinOperatorType();
790 * Make a function type from domain to range.
792 * @param domain the domain type
793 * @param range the range type
794 * @returns the functional type domain -> range
796 inline TypeNode
mkFunctionType(const TypeNode
& domain
, const TypeNode
& range
);
799 * Make a function type with input types from
800 * argTypes. <code>argTypes</code> must have at least one element.
802 * @param argTypes the domain is a tuple (argTypes[0], ..., argTypes[n])
803 * @param range the range type
804 * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range
806 inline TypeNode
mkFunctionType(const std::vector
<TypeNode
>& argTypes
,
807 const TypeNode
& range
);
810 * Make a function type with input types from
811 * <code>sorts[0..sorts.size()-2]</code> and result type
812 * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
813 * at least 2 elements.
815 inline TypeNode
mkFunctionType(const std::vector
<TypeNode
>& sorts
);
818 * Make a predicate type with input types from
819 * <code>sorts</code>. The result with be a function type with range
820 * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
823 inline TypeNode
mkPredicateType(const std::vector
<TypeNode
>& sorts
);
826 * Make a tuple type with types from
827 * <code>types</code>. <code>types</code> must have at least one
830 * @param types a vector of types
831 * @returns the tuple type (types[0], ..., types[n])
833 TypeNode
mkTupleType(const std::vector
<TypeNode
>& types
);
836 * Make a record type with the description from rec.
838 * @param rec a description of the record
839 * @returns the record type
841 TypeNode
mkRecordType(const Record
& rec
);
844 * Make a symbolic expression type with types from
845 * <code>types</code>. <code>types</code> may have any number of
848 * @param types a vector of types
849 * @returns the symbolic expression type (types[0], ..., types[n])
851 inline TypeNode
mkSExprType(const std::vector
<TypeNode
>& types
);
853 /** Make the type of floating-point with <code>exp</code> bit exponent and
854 <code>sig</code> bit significand */
855 inline TypeNode
mkFloatingPointType(unsigned exp
, unsigned sig
);
856 inline TypeNode
mkFloatingPointType(FloatingPointSize fs
);
858 /** Make the type of bitvectors of size <code>size</code> */
859 inline TypeNode
mkBitVectorType(unsigned size
);
861 /** Make the type of arrays with the given parameterization */
862 inline TypeNode
mkArrayType(TypeNode indexType
, TypeNode constituentType
);
864 /** Make the type of arrays with the given parameterization */
865 inline TypeNode
mkSetType(TypeNode elementType
);
867 /** Make a type representing a constructor with the given parameterization */
868 TypeNode
mkConstructorType(const DatatypeConstructor
& constructor
, TypeNode range
);
870 /** Make a type representing a selector with the given parameterization */
871 inline TypeNode
mkSelectorType(TypeNode domain
, TypeNode range
);
873 /** Make a type representing a tester with given parameterization */
874 inline TypeNode
mkTesterType(TypeNode domain
);
876 /** Make a new (anonymous) sort of arity 0. */
877 TypeNode
mkSort(uint32_t flags
= ExprManager::SORT_FLAG_NONE
);
879 /** Make a new sort with the given name of arity 0. */
880 TypeNode
mkSort(const std::string
& name
, uint32_t flags
= ExprManager::SORT_FLAG_NONE
);
882 /** Make a new sort by parameterizing the given sort constructor. */
883 TypeNode
mkSort(TypeNode constructor
,
884 const std::vector
<TypeNode
>& children
,
885 uint32_t flags
= ExprManager::SORT_FLAG_NONE
);
887 /** Make a new sort with the given name and arity. */
888 TypeNode
mkSortConstructor(const std::string
& name
,
890 uint32_t flags
= ExprManager::SORT_FLAG_NONE
);
893 * Get the type for the given node and optionally do type checking.
895 * Initial type computation will be near-constant time if
896 * type checking is not requested. Results are memoized, so that
897 * subsequent calls to getType() without type checking will be
900 * Initial type checking is linear in the size of the expression.
901 * Again, the results are memoized, so that subsequent calls to
902 * getType(), with or without type checking, will be constant
905 * NOTE: A TypeCheckingException can be thrown even when type
906 * checking is not requested. getType() will always return a
907 * valid and correct type and, thus, an exception will be thrown
908 * when no valid or correct type can be computed (e.g., if the
909 * arguments to a bit-vector operation aren't bit-vectors). When
910 * type checking is not requested, getType() will do the minimum
911 * amount of checking required to return a valid result.
913 * @param n the Node for which we want a type
914 * @param check whether we should check the type as we compute it
917 TypeNode
getType(TNode n
, bool check
= false);
920 * Convert a node to an expression. Uses the ExprManager
921 * associated to this NodeManager.
923 inline Expr
toExpr(TNode n
);
926 * Convert an expression to a node.
928 static inline Node
fromExpr(const Expr
& e
);
931 * Convert a node manager to an expression manager.
933 inline ExprManager
* toExprManager();
936 * Convert an expression manager to a node manager.
938 static inline NodeManager
* fromExprManager(ExprManager
* exprManager
);
941 * Convert a type node to a type.
943 inline Type
toType(TypeNode tn
);
946 * Convert a type to a type node.
948 static inline TypeNode
fromType(Type t
);
950 /** Reclaim zombies while there are more than k nodes in the pool (if possible).*/
951 void reclaimZombiesUntil(uint32_t k
);
953 /** Reclaims all zombies (if possible).*/
954 void reclaimAllZombies();
956 /** Size of the node pool. */
957 size_t poolSize() const;
959 /** Deletes a list of attributes from the NM's AttributeManager.*/
960 void deleteAttributes(const std::vector
< const expr::attr::AttributeUniqueId
* >& ids
);
963 * This function gives developers a hook into the NodeManager.
964 * This can be changed in node_manager.cpp without recompiling most of cvc4.
966 * debugHook is a debugging only function, and should not be present in
967 * any published code!
969 void debugHook(int debugFlag
);
970 };/* class NodeManager */
973 * This class changes the "current" thread-global
974 * <code>NodeManager</code> when it is created and reinstates the
975 * previous thread-global <code>NodeManager</code> when it is
976 * destroyed, effectively maintaining a set of nested
977 * <code>NodeManager</code> scopes. This is especially useful on
978 * public-interface calls into the CVC4 library, where CVC4's notion
979 * of the "current" <code>NodeManager</code> should be set to match
980 * the calling context. See, for example, the implementations of
981 * public calls in the <code>ExprManager</code> and
982 * <code>SmtEngine</code> classes.
984 * The client must be careful to create and destroy
985 * <code>NodeManagerScope</code> objects in a well-nested manner (such
986 * as on the stack). You may create a <code>NodeManagerScope</code>
987 * with <code>new</code> and destroy it with <code>delete</code>, or
988 * place it as a data member of an object that is, but if the scope of
989 * these <code>new</code>/<code>delete</code> pairs isn't properly
990 * maintained, the incorrect "current" <code>NodeManager</code>
991 * pointer may be restored after a delete.
993 class NodeManagerScope
{
994 /** The old NodeManager, to be restored on destruction. */
995 NodeManager
* d_oldNodeManager
;
996 Options::OptionsScope d_optionsScope
;
999 NodeManagerScope(NodeManager
* nm
)
1000 : d_oldNodeManager(NodeManager::s_current
)
1001 , d_optionsScope(nm
? nm
->d_options
: NULL
) {
1002 // There are corner cases where nm can be NULL and it's ok.
1003 // For example, if you write { Expr e; }, then when the null
1004 // Expr is destructed, there's no active node manager.
1005 //Assert(nm != NULL);
1006 NodeManager::s_current
= nm
;
1007 //Options::s_current = nm ? nm->d_options : NULL;
1008 Debug("current") << "node manager scope: "
1009 << NodeManager::s_current
<< "\n";
1012 ~NodeManagerScope() {
1013 NodeManager::s_current
= d_oldNodeManager
;
1014 //Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL;
1015 Debug("current") << "node manager scope: "
1016 << "returning to " << NodeManager::s_current
<< "\n";
1018 };/* class NodeManagerScope */
1020 /** Get the (singleton) type for booleans. */
1021 inline TypeNode
NodeManager::booleanType() {
1022 return TypeNode(mkTypeConst
<TypeConstant
>(BOOLEAN_TYPE
));
1025 /** Get the (singleton) type for integers. */
1026 inline TypeNode
NodeManager::integerType() {
1027 return TypeNode(mkTypeConst
<TypeConstant
>(INTEGER_TYPE
));
1030 /** Get the (singleton) type for reals. */
1031 inline TypeNode
NodeManager::realType() {
1032 return TypeNode(mkTypeConst
<TypeConstant
>(REAL_TYPE
));
1035 /** Get the (singleton) type for strings. */
1036 inline TypeNode
NodeManager::stringType() {
1037 return TypeNode(mkTypeConst
<TypeConstant
>(STRING_TYPE
));
1040 /** Get the (singleton) type for regexps. */
1041 inline TypeNode
NodeManager::regExpType() {
1042 return TypeNode(mkTypeConst
<TypeConstant
>(REGEXP_TYPE
));
1045 /** Get the (singleton) type for rounding modes. */
1046 inline TypeNode
NodeManager::roundingModeType() {
1047 return TypeNode(mkTypeConst
<TypeConstant
>(ROUNDINGMODE_TYPE
));
1050 /** Get the bound var list type. */
1051 inline TypeNode
NodeManager::boundVarListType() {
1052 return TypeNode(mkTypeConst
<TypeConstant
>(BOUND_VAR_LIST_TYPE
));
1055 /** Get the instantiation pattern type. */
1056 inline TypeNode
NodeManager::instPatternType() {
1057 return TypeNode(mkTypeConst
<TypeConstant
>(INST_PATTERN_TYPE
));
1060 /** Get the instantiation pattern type. */
1061 inline TypeNode
NodeManager::instPatternListType() {
1062 return TypeNode(mkTypeConst
<TypeConstant
>(INST_PATTERN_LIST_TYPE
));
1065 /** Get the (singleton) type for builtin operators. */
1066 inline TypeNode
NodeManager::builtinOperatorType() {
1067 return TypeNode(mkTypeConst
<TypeConstant
>(BUILTIN_OPERATOR_TYPE
));
1070 /** Make a function type from domain to range. */
1071 inline TypeNode
NodeManager::mkFunctionType(const TypeNode
& domain
, const TypeNode
& range
) {
1072 std::vector
<TypeNode
> sorts
;
1073 sorts
.push_back(domain
);
1074 sorts
.push_back(range
);
1075 return mkFunctionType(sorts
);
1078 inline TypeNode
NodeManager::mkFunctionType(const std::vector
<TypeNode
>& argTypes
, const TypeNode
& range
) {
1079 Assert(argTypes
.size() >= 1);
1080 std::vector
<TypeNode
> sorts(argTypes
);
1081 sorts
.push_back(range
);
1082 return mkFunctionType(sorts
);
1086 NodeManager::mkFunctionType(const std::vector
<TypeNode
>& sorts
) {
1087 Assert(sorts
.size() >= 2);
1088 std::vector
<TypeNode
> sortNodes
;
1089 for (unsigned i
= 0; i
< sorts
.size(); ++ i
) {
1090 CheckArgument(sorts
[i
].isFirstClass(), sorts
,
1091 "cannot create function types for argument types that are not first-class");
1092 sortNodes
.push_back(sorts
[i
]);
1094 CheckArgument(!sorts
[sorts
.size()-1].isFunction(), sorts
[sorts
.size()-1],
1095 "must flatten function types");
1096 return mkTypeNode(kind::FUNCTION_TYPE
, sortNodes
);
1100 NodeManager::mkPredicateType(const std::vector
<TypeNode
>& sorts
) {
1101 Assert(sorts
.size() >= 1);
1102 std::vector
<TypeNode
> sortNodes
;
1103 for (unsigned i
= 0; i
< sorts
.size(); ++ i
) {
1104 CheckArgument(sorts
[i
].isFirstClass(), sorts
,
1105 "cannot create predicate types for argument types that are not first-class");
1106 sortNodes
.push_back(sorts
[i
]);
1108 sortNodes
.push_back(booleanType());
1109 return mkTypeNode(kind::FUNCTION_TYPE
, sortNodes
);
1112 inline TypeNode
NodeManager::mkSExprType(const std::vector
<TypeNode
>& types
) {
1113 std::vector
<TypeNode
> typeNodes
;
1114 for (unsigned i
= 0; i
< types
.size(); ++ i
) {
1115 typeNodes
.push_back(types
[i
]);
1117 return mkTypeNode(kind::SEXPR_TYPE
, typeNodes
);
1120 inline TypeNode
NodeManager::mkBitVectorType(unsigned size
) {
1121 return TypeNode(mkTypeConst
<BitVectorSize
>(BitVectorSize(size
)));
1124 inline TypeNode
NodeManager::mkFloatingPointType(unsigned exp
, unsigned sig
) {
1125 return TypeNode(mkTypeConst
<FloatingPointSize
>(FloatingPointSize(exp
,sig
)));
1128 inline TypeNode
NodeManager::mkFloatingPointType(FloatingPointSize fs
) {
1129 return TypeNode(mkTypeConst
<FloatingPointSize
>(fs
));
1132 inline TypeNode
NodeManager::mkArrayType(TypeNode indexType
,
1133 TypeNode constituentType
) {
1134 CheckArgument(!indexType
.isNull(), indexType
,
1135 "unexpected NULL index type");
1136 CheckArgument(!constituentType
.isNull(), constituentType
,
1137 "unexpected NULL constituent type");
1138 CheckArgument(indexType
.isFirstClass(), indexType
,
1139 "cannot index arrays by types that are not first-class");
1140 CheckArgument(constituentType
.isFirstClass(), constituentType
,
1141 "cannot store types that are not first-class in arrays");
1142 Debug("arrays") << "making array type " << indexType
<< " "
1143 << constituentType
<< std::endl
;
1144 return mkTypeNode(kind::ARRAY_TYPE
, indexType
, constituentType
);
1147 inline TypeNode
NodeManager::mkSetType(TypeNode elementType
) {
1148 CheckArgument(!elementType
.isNull(), elementType
,
1149 "unexpected NULL element type");
1150 CheckArgument(elementType
.isFirstClass(), elementType
,
1151 "cannot store types that are not first-class in sets");
1152 Debug("sets") << "making sets type " << elementType
<< std::endl
;
1153 return mkTypeNode(kind::SET_TYPE
, elementType
);
1156 inline TypeNode
NodeManager::mkSelectorType(TypeNode domain
, TypeNode range
) {
1157 CheckArgument(domain
.isDatatype(), domain
,
1158 "cannot create non-datatype selector type");
1159 CheckArgument(range
.isFirstClass(), range
,
1160 "cannot have selector fields that are not first-class types");
1161 return mkTypeNode(kind::SELECTOR_TYPE
, domain
, range
);
1164 inline TypeNode
NodeManager::mkTesterType(TypeNode domain
) {
1165 CheckArgument(domain
.isDatatype(), domain
,
1166 "cannot create non-datatype tester");
1167 return mkTypeNode(kind::TESTER_TYPE
, domain
);
1170 inline expr::NodeValue
* NodeManager::poolLookup(expr::NodeValue
* nv
) const {
1171 NodeValuePool::const_iterator find
= d_nodeValuePool
.find(nv
);
1172 if(find
== d_nodeValuePool
.end()) {
1179 inline void NodeManager::poolInsert(expr::NodeValue
* nv
) {
1180 Assert(d_nodeValuePool
.find(nv
) == d_nodeValuePool
.end(),
1181 "NodeValue already in the pool!");
1182 d_nodeValuePool
.insert(nv
);// FIXME multithreading
1185 inline void NodeManager::poolRemove(expr::NodeValue
* nv
) {
1186 Assert(d_nodeValuePool
.find(nv
) != d_nodeValuePool
.end(),
1187 "NodeValue is not in the pool!");
1189 d_nodeValuePool
.erase(nv
);// FIXME multithreading
1192 inline Expr
NodeManager::toExpr(TNode n
) {
1193 return Expr(d_exprManager
, new Node(n
));
1196 inline Node
NodeManager::fromExpr(const Expr
& e
) {
1200 inline ExprManager
* NodeManager::toExprManager() {
1201 return d_exprManager
;
1204 inline NodeManager
* NodeManager::fromExprManager(ExprManager
* exprManager
) {
1205 return exprManager
->getNodeManager();
1208 inline Type
NodeManager::toType(TypeNode tn
) {
1209 return Type(this, new TypeNode(tn
));
1212 inline TypeNode
NodeManager::fromType(Type t
) {
1213 return *Type::getTypeNode(t
);
1216 }/* CVC4 namespace */
1218 #define CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
1219 #include "expr/metakind.h"
1220 #undef CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
1222 #include "expr/node_builder.h"
1226 // general expression-builders
1228 inline bool NodeManager::hasOperator(Kind k
) {
1229 switch(kind::MetaKind mk
= kind::metaKindOf(k
)) {
1231 case kind::metakind::INVALID
:
1232 case kind::metakind::VARIABLE
:
1233 case kind::metakind::NULLARY_OPERATOR
:
1236 case kind::metakind::OPERATOR
:
1237 case kind::metakind::PARAMETERIZED
:
1240 case kind::metakind::CONSTANT
:
1248 inline Kind
NodeManager::operatorToKind(TNode n
) {
1249 return kind::operatorToKind(n
.d_nv
);
1252 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
) {
1253 NodeBuilder
<1> nb(this, kind
);
1255 return nb
.constructNode();
1258 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
) {
1259 NodeBuilder
<1> nb(this, kind
);
1261 return nb
.constructNodePtr();
1264 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
, TNode child2
) {
1265 NodeBuilder
<2> nb(this, kind
);
1266 nb
<< child1
<< child2
;
1267 return nb
.constructNode();
1270 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
, TNode child2
) {
1271 NodeBuilder
<2> nb(this, kind
);
1272 nb
<< child1
<< child2
;
1273 return nb
.constructNodePtr();
1276 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
, TNode child2
,
1278 NodeBuilder
<3> nb(this, kind
);
1279 nb
<< child1
<< child2
<< child3
;
1280 return nb
.constructNode();
1283 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
, TNode child2
,
1285 NodeBuilder
<3> nb(this, kind
);
1286 nb
<< child1
<< child2
<< child3
;
1287 return nb
.constructNodePtr();
1290 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
, TNode child2
,
1291 TNode child3
, TNode child4
) {
1292 NodeBuilder
<4> nb(this, kind
);
1293 nb
<< child1
<< child2
<< child3
<< child4
;
1294 return nb
.constructNode();
1297 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
, TNode child2
,
1298 TNode child3
, TNode child4
) {
1299 NodeBuilder
<4> nb(this, kind
);
1300 nb
<< child1
<< child2
<< child3
<< child4
;
1301 return nb
.constructNodePtr();
1304 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
, TNode child2
,
1305 TNode child3
, TNode child4
, TNode child5
) {
1306 NodeBuilder
<5> nb(this, kind
);
1307 nb
<< child1
<< child2
<< child3
<< child4
<< child5
;
1308 return nb
.constructNode();
1311 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
, TNode child2
,
1312 TNode child3
, TNode child4
, TNode child5
) {
1313 NodeBuilder
<5> nb(this, kind
);
1314 nb
<< child1
<< child2
<< child3
<< child4
<< child5
;
1315 return nb
.constructNodePtr();
1319 template <bool ref_count
>
1320 inline Node
NodeManager::mkNode(Kind kind
,
1321 const std::vector
<NodeTemplate
<ref_count
> >&
1323 NodeBuilder
<> nb(this, kind
);
1324 nb
.append(children
);
1325 return nb
.constructNode();
1328 template <bool ref_count
>
1329 inline Node
* NodeManager::mkNodePtr(Kind kind
,
1330 const std::vector
<NodeTemplate
<ref_count
> >&
1332 NodeBuilder
<> nb(this, kind
);
1333 nb
.append(children
);
1334 return nb
.constructNodePtr();
1338 inline Node
NodeManager::mkNode(TNode opNode
) {
1339 NodeBuilder
<1> nb(this, operatorToKind(opNode
));
1340 if(opNode
.getKind() != kind::BUILTIN
) {
1343 return nb
.constructNode();
1346 inline Node
* NodeManager::mkNodePtr(TNode opNode
) {
1347 NodeBuilder
<1> nb(this, operatorToKind(opNode
));
1348 if(opNode
.getKind() != kind::BUILTIN
) {
1351 return nb
.constructNodePtr();
1354 inline Node
NodeManager::mkNode(TNode opNode
, TNode child1
) {
1355 NodeBuilder
<2> nb(this, operatorToKind(opNode
));
1356 if(opNode
.getKind() != kind::BUILTIN
) {
1360 return nb
.constructNode();
1363 inline Node
* NodeManager::mkNodePtr(TNode opNode
, TNode child1
) {
1364 NodeBuilder
<2> nb(this, operatorToKind(opNode
));
1365 if(opNode
.getKind() != kind::BUILTIN
) {
1369 return nb
.constructNodePtr();
1372 inline Node
NodeManager::mkNode(TNode opNode
, TNode child1
, TNode child2
) {
1373 NodeBuilder
<3> nb(this, operatorToKind(opNode
));
1374 if(opNode
.getKind() != kind::BUILTIN
) {
1377 nb
<< child1
<< child2
;
1378 return nb
.constructNode();
1381 inline Node
* NodeManager::mkNodePtr(TNode opNode
, TNode child1
, TNode child2
) {
1382 NodeBuilder
<3> nb(this, operatorToKind(opNode
));
1383 if(opNode
.getKind() != kind::BUILTIN
) {
1386 nb
<< child1
<< child2
;
1387 return nb
.constructNodePtr();
1390 inline Node
NodeManager::mkNode(TNode opNode
, TNode child1
, TNode child2
,
1392 NodeBuilder
<4> nb(this, operatorToKind(opNode
));
1393 if(opNode
.getKind() != kind::BUILTIN
) {
1396 nb
<< child1
<< child2
<< child3
;
1397 return nb
.constructNode();
1400 inline Node
* NodeManager::mkNodePtr(TNode opNode
, TNode child1
, TNode child2
,
1402 NodeBuilder
<4> nb(this, operatorToKind(opNode
));
1403 if(opNode
.getKind() != kind::BUILTIN
) {
1406 nb
<< child1
<< child2
<< child3
;
1407 return nb
.constructNodePtr();
1410 inline Node
NodeManager::mkNode(TNode opNode
, TNode child1
, TNode child2
,
1411 TNode child3
, TNode child4
) {
1412 NodeBuilder
<5> nb(this, operatorToKind(opNode
));
1413 if(opNode
.getKind() != kind::BUILTIN
) {
1416 nb
<< child1
<< child2
<< child3
<< child4
;
1417 return nb
.constructNode();
1420 inline Node
* NodeManager::mkNodePtr(TNode opNode
, TNode child1
, TNode child2
,
1421 TNode child3
, TNode child4
) {
1422 NodeBuilder
<5> nb(this, operatorToKind(opNode
));
1423 if(opNode
.getKind() != kind::BUILTIN
) {
1426 nb
<< child1
<< child2
<< child3
<< child4
;
1427 return nb
.constructNodePtr();
1430 inline Node
NodeManager::mkNode(TNode opNode
, TNode child1
, TNode child2
,
1431 TNode child3
, TNode child4
, TNode child5
) {
1432 NodeBuilder
<6> nb(this, operatorToKind(opNode
));
1433 if(opNode
.getKind() != kind::BUILTIN
) {
1436 nb
<< child1
<< child2
<< child3
<< child4
<< child5
;
1437 return nb
.constructNode();
1440 inline Node
* NodeManager::mkNodePtr(TNode opNode
, TNode child1
, TNode child2
,
1441 TNode child3
, TNode child4
, TNode child5
) {
1442 NodeBuilder
<6> nb(this, operatorToKind(opNode
));
1443 if(opNode
.getKind() != kind::BUILTIN
) {
1446 nb
<< child1
<< child2
<< child3
<< child4
<< child5
;
1447 return nb
.constructNodePtr();
1450 // N-ary version for operators
1451 template <bool ref_count
>
1452 inline Node
NodeManager::mkNode(TNode opNode
,
1453 const std::vector
<NodeTemplate
<ref_count
> >&
1455 NodeBuilder
<> nb(this, operatorToKind(opNode
));
1456 if(opNode
.getKind() != kind::BUILTIN
) {
1459 nb
.append(children
);
1460 return nb
.constructNode();
1463 template <bool ref_count
>
1464 inline Node
* NodeManager::mkNodePtr(TNode opNode
,
1465 const std::vector
<NodeTemplate
<ref_count
> >&
1467 NodeBuilder
<> nb(this, operatorToKind(opNode
));
1468 if(opNode
.getKind() != kind::BUILTIN
) {
1471 nb
.append(children
);
1472 return nb
.constructNodePtr();
1476 inline TypeNode
NodeManager::mkTypeNode(Kind kind
, TypeNode child1
) {
1477 return (NodeBuilder
<1>(this, kind
) << child1
).constructTypeNode();
1480 inline TypeNode
NodeManager::mkTypeNode(Kind kind
, TypeNode child1
,
1482 return (NodeBuilder
<2>(this, kind
) << child1
<< child2
).constructTypeNode();
1485 inline TypeNode
NodeManager::mkTypeNode(Kind kind
, TypeNode child1
,
1486 TypeNode child2
, TypeNode child3
) {
1487 return (NodeBuilder
<3>(this, kind
) << child1
<< child2
<< child3
).constructTypeNode();
1490 // N-ary version for types
1491 inline TypeNode
NodeManager::mkTypeNode(Kind kind
,
1492 const std::vector
<TypeNode
>& children
) {
1493 return NodeBuilder
<>(this, kind
).append(children
).constructTypeNode();
1497 Node
NodeManager::mkConst(const T
& val
) {
1498 return mkConstInternal
<Node
, T
>(val
);
1502 TypeNode
NodeManager::mkTypeConst(const T
& val
) {
1503 return mkConstInternal
<TypeNode
, T
>(val
);
1506 template <class NodeClass
, class T
>
1507 NodeClass
NodeManager::mkConstInternal(const T
& val
) {
1509 // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
1510 NVStorage
<1> nvStorage
;
1511 expr::NodeValue
& nvStack
= reinterpret_cast<expr::NodeValue
&>(nvStorage
);
1514 nvStack
.d_kind
= kind::metakind::ConstantMap
<T
>::kind
;
1516 nvStack
.d_nchildren
= 1;
1518 #if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6))
1519 #pragma GCC diagnostic push
1520 #pragma GCC diagnostic ignored "-Warray-bounds"
1523 nvStack
.d_children
[0] =
1524 const_cast<expr::NodeValue
*>(reinterpret_cast<const expr::NodeValue
*>(&val
));
1525 expr::NodeValue
* nv
= poolLookup(&nvStack
);
1527 #if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6))
1528 #pragma GCC diagnostic pop
1532 return NodeClass(nv
);
1535 nv
= (expr::NodeValue
*)
1536 std::malloc(sizeof(expr::NodeValue
) + sizeof(T
));
1538 throw std::bad_alloc();
1541 nv
->d_nchildren
= 0;
1542 nv
->d_kind
= kind::metakind::ConstantMap
<T
>::kind
;
1543 nv
->d_id
= next_id
++;// FIXME multithreading
1546 //OwningTheory::mkConst(val);
1547 new (&nv
->d_children
) T(val
);
1550 if(Debug
.isOn("gc")) {
1551 Debug("gc") << "creating node value " << nv
1552 << " [" << nv
->d_id
<< "]: ";
1553 nv
->printAst(Debug("gc"));
1554 Debug("gc") << std::endl
;
1557 return NodeClass(nv
);
1560 }/* CVC4 namespace */
1562 #endif /* CVC4__NODE_MANAGER_H */