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 "base/check.h"
36 #include "expr/kind.h"
37 #include "expr/metakind.h"
38 #include "expr/node_value.h"
39 #include "options/options.h"
43 class StatisticsRegistry
;
44 class ResourceManager
;
50 class AttributeUniqueId
;
51 class AttributeManager
;
52 }/* CVC4::expr::attr namespace */
55 }/* CVC4::expr namespace */
58 * An interface that an interested party can implement and then subscribe
59 * to NodeManager events via NodeManager::subscribeEvents(this).
61 class NodeManagerListener
{
63 virtual ~NodeManagerListener() {}
64 virtual void nmNotifyNewSort(TypeNode tn
, uint32_t flags
) {}
65 virtual void nmNotifyNewSortConstructor(TypeNode tn
, uint32_t flags
) {}
66 virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor
, TypeNode sort
,
68 virtual void nmNotifyNewDatatypes(const std::vector
<DatatypeType
>& datatypes
,
72 virtual void nmNotifyNewVar(TNode n
, uint32_t flags
) {}
73 virtual void nmNotifyNewSkolem(TNode n
, const std::string
& comment
,
76 * Notify a listener of a Node that's being GCed. If this function stores a
78 * to the Node somewhere, very bad things will happen.
80 virtual void nmNotifyDeleteNode(TNode n
) {}
81 }; /* class NodeManagerListener */
84 template <unsigned nchild_thresh
> friend class CVC4::NodeBuilder
;
85 friend class NodeManagerScope
;
86 friend class expr::NodeValue
;
87 friend class expr::TypeChecker
;
89 // friends so they can access mkVar() here, which is private
90 friend Expr
ExprManager::mkVar(const std::string
&, Type
, uint32_t flags
);
91 friend Expr
ExprManager::mkVar(Type
, uint32_t flags
);
93 // friend so it can access NodeManager's d_listeners and notify clients
94 friend std::vector
<DatatypeType
> ExprManager::mkMutualDatatypeTypes(
95 std::vector
<Datatype
>&, std::set
<Type
>&, uint32_t);
97 /** Predicate for use with STL algorithms */
98 struct NodeValueReferenceCountNonZero
{
99 bool operator()(expr::NodeValue
* nv
) { return nv
->d_rc
> 0; }
102 typedef std::unordered_set
<expr::NodeValue
*,
103 expr::NodeValuePoolHashFunction
,
104 expr::NodeValuePoolEq
> NodeValuePool
;
105 typedef std::unordered_set
<expr::NodeValue
*,
106 expr::NodeValueIDHashFunction
,
107 expr::NodeValueIDEquality
> NodeValueIDSet
;
109 static thread_local NodeManager
* s_current
;
112 StatisticsRegistry
* d_statisticsRegistry
;
114 ResourceManager
* d_resourceManager
;
117 * A list of registrations on d_options to that call into d_resourceManager.
118 * These must be garbage collected before d_options and d_resourceManager.
120 ListenerRegistrationList
* d_registrations
;
122 NodeValuePool d_nodeValuePool
;
126 expr::attr::AttributeManager
* d_attrManager
;
128 /** The associated ExprManager */
129 ExprManager
* d_exprManager
;
132 * The node value we're currently freeing. This unique node value
133 * is permitted to have outstanding TNodes to it (in "soft"
134 * contexts, like as a key in attribute tables), even though
135 * normally it's an error to have a TNode to a node value with a
136 * reference count of 0. Being "under deletion" also enables
137 * assertions that inc() is not called on it.
139 expr::NodeValue
* d_nodeUnderDeletion
;
142 * True iff we are in reclaimZombies(). This avoids unnecessary
143 * recursion; a NodeValue being deleted might zombify other
144 * NodeValues, but these shouldn't trigger a (recursive) call to
147 bool d_inReclaimZombies
;
150 * The set of zombie nodes. We may want to revisit this design, as
151 * we might like to delete nodes in least-recently-used order. But
152 * we also need to avoid processing a zombie twice.
154 NodeValueIDSet d_zombies
;
157 * NodeValues with maxed out reference counts. These live as long as the
158 * NodeManager. They have a custom deallocation procedure at the very end.
160 std::vector
<expr::NodeValue
*> d_maxedOut
;
163 * A set of operator singletons (w.r.t. to this NodeManager
164 * instance) for operators. Conceptually, Nodes with kind, say,
165 * PLUS, are APPLYs of a PLUS operator to arguments. This array
166 * holds the set of operators for these things. A PLUS operator is
167 * a Node with kind "BUILTIN", and if you call
168 * plusOperator->getConst<CVC4::Kind>(), you get kind::PLUS back.
170 Node d_operators
[kind::LAST_KIND
];
172 /** unique vars per (Kind,Type) */
173 std::map
< Kind
, std::map
< TypeNode
, Node
> > d_unique_vars
;
176 * A list of subscribers for NodeManager events.
178 std::vector
<NodeManagerListener
*> d_listeners
;
180 /** A list of datatypes owned by this node manager. */
181 std::vector
<std::shared_ptr
<DType
> > d_ownedDTypes
;
184 * A map of tuple and record types to their corresponding datatype.
186 class TupleTypeCache
{
188 std::map
< TypeNode
, TupleTypeCache
> d_children
;
190 TypeNode
getTupleType( NodeManager
* nm
, std::vector
< TypeNode
>& types
, unsigned index
= 0 );
194 std::map
< TypeNode
, std::map
< std::string
, RecTypeCache
> > d_children
;
196 TypeNode
getRecordType( NodeManager
* nm
, const Record
& rec
, unsigned index
= 0 );
198 TupleTypeCache d_tt_cache
;
199 RecTypeCache d_rt_cache
;
202 * Keep a count of all abstract values produced by this NodeManager.
203 * Abstract values have a type attribute, so if multiple SmtEngines
204 * are attached to this NodeManager, we don't want their abstract
207 unsigned d_abstractValueCount
;
210 * A counter used to produce unique skolem names.
212 * Note that it is NOT incremented when skolems are created using
213 * SKOLEM_EXACT_NAME, so it is NOT a count of the skolems produced
214 * by this node manager.
216 unsigned d_skolemCounter
;
219 * Look up a NodeValue in the pool associated to this NodeManager.
220 * The NodeValue argument need not be a "completely-constructed"
221 * NodeValue. In particular, "non-inlined" constants are permitted
224 * For non-CONSTANT metakinds, nv's d_kind and d_nchildren should be
225 * correctly set, and d_children[0..n-1] should be valid (extant)
226 * NodeValues for lookup.
228 * For CONSTANT metakinds, nv's d_kind should be set correctly.
229 * Normally a CONSTANT would have d_nchildren == 0 and the constant
230 * value inlined in the d_children space. However, here we permit
231 * "non-inlined" NodeValues to avoid unnecessary copying. For
232 * these, d_nchildren == 1, and d_nchildren is a pointer to the
235 * The point of this complex design is to permit efficient lookups
236 * (without fully constructing a NodeValue). In the case that the
237 * argument is not fully constructed, and this function returns
238 * NULL, the caller should fully construct an equivalent one before
239 * calling poolInsert(). NON-FULLY-CONSTRUCTED NODEVALUES are not
240 * permitted in the pool!
242 inline expr::NodeValue
* poolLookup(expr::NodeValue
* nv
) const;
245 * Insert a NodeValue into the NodeManager's pool.
247 * It is an error to insert a NodeValue already in the pool.
248 * Enquire first with poolLookup().
250 inline void poolInsert(expr::NodeValue
* nv
);
253 * Remove a NodeValue from the NodeManager's pool.
255 * It is an error to request the removal of a NodeValue from the
256 * pool that is not in the pool.
258 inline void poolRemove(expr::NodeValue
* nv
);
261 * Determine if nv is currently being deleted by the NodeManager.
263 inline bool isCurrentlyDeleting(const expr::NodeValue
* nv
) const {
264 return d_nodeUnderDeletion
== nv
;
268 * Register a NodeValue as a zombie.
270 inline void markForDeletion(expr::NodeValue
* nv
) {
271 Assert(nv
->d_rc
== 0);
273 // if d_reclaiming is set, make sure we don't call
274 // reclaimZombies(), because it's already running.
275 if(Debug
.isOn("gc")) {
276 Debug("gc") << "zombifying node value " << nv
277 << " [" << nv
->d_id
<< "]: ";
278 nv
->printAst(Debug("gc"));
279 Debug("gc") << (d_inReclaimZombies
? " [CURRENTLY-RECLAIMING]" : "")
283 // `d_zombies` uses the node id to hash and compare nodes. If `d_zombies`
284 // already contains a node value with the same id as `nv`, but the pointers
285 // are different, then the wrong `NodeManager` was in scope for one of the
286 // two nodes when it reached refcount zero. This can happen for example if
287 // you create a node with a `NodeManager` n1 and then call `Node::toExpr()`
288 // on that node while a different `NodeManager` n2 is in scope. When that
289 // `Expr` is deleted and the node reaches refcount zero in the `Expr`'s
290 // destructor, then `markForDeletion()` will be called on n2.
291 Assert(d_zombies
.find(nv
) == d_zombies
.end() || *d_zombies
.find(nv
) == nv
);
293 d_zombies
.insert(nv
); // FIXME multithreading
295 if(safeToReclaimZombies()) {
296 if(d_zombies
.size() > 5000) {
303 * Register a NodeValue as having a maxed out reference count. This NodeValue
304 * will live as long as its containing NodeManager.
306 inline void markRefCountMaxedOut(expr::NodeValue
* nv
) {
307 Assert(nv
->HasMaximizedReferenceCount());
308 if(Debug
.isOn("gc")) {
309 Debug("gc") << "marking node value " << nv
310 << " [" << nv
->d_id
<< "]: as maxed out" << std::endl
;
312 d_maxedOut
.push_back(nv
);
316 * Reclaim all zombies.
318 void reclaimZombies();
321 * It is safe to collect zombies.
323 bool safeToReclaimZombies() const;
326 * Returns a reverse topological sort of a list of NodeValues. The NodeValues
327 * must be valid and have ids. The NodeValues are not modified (including ref
330 static std::vector
<expr::NodeValue
*> TopologicalSort(
331 const std::vector
<expr::NodeValue
*>& roots
);
334 * This template gives a mechanism to stack-allocate a NodeValue
335 * with enough space for N children (where N is a compile-time
336 * constant). You use it like this:
338 * NVStorage<4> nvStorage;
339 * NodeValue& nvStack = reinterpret_cast<NodeValue&>(nvStorage);
341 * ...and then you can use nvStack as a NodeValue that you know has
342 * room for 4 children.
347 expr::NodeValue
* child
[N
];
348 };/* struct NodeManager::NVStorage<N> */
350 /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
352 * It has been decided for now to hold off on implementations of
353 * these functions, as they may only be needed in CNF conversion,
354 * where it's pointless to do a lazy isAtomic determination by
355 * searching through the DAG, and storing it, since the result will
356 * only be used once. For more details see the 4/27/2010 CVC4
357 * developer's meeting notes at:
359 * http://cvc4.cs.stanford.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
361 // bool containsDecision(TNode); // is "atomic"
362 // bool properlyContainsDecision(TNode); // all children are atomic
364 // undefined private copy constructor (disallow copy)
365 NodeManager(const NodeManager
&) = delete;
367 NodeManager
& operator=(const NodeManager
&) = delete;
372 * Create a variable with the given name and type. NOTE that no
373 * lookup is done on the name. If you mkVar("a", type) and then
374 * mkVar("a", type) again, you have two variables. The NodeManager
375 * version of this is private to avoid internal uses of mkVar() from
376 * within CVC4. Such uses should employ mkSkolem() instead.
378 Node
mkVar(const std::string
& name
, const TypeNode
& type
, uint32_t flags
= ExprManager::VAR_FLAG_NONE
);
379 Node
* mkVarPtr(const std::string
& name
, const TypeNode
& type
, uint32_t flags
= ExprManager::VAR_FLAG_NONE
);
381 /** Create a variable with the given type. */
382 Node
mkVar(const TypeNode
& type
, uint32_t flags
= ExprManager::VAR_FLAG_NONE
);
383 Node
* mkVarPtr(const TypeNode
& type
, uint32_t flags
= ExprManager::VAR_FLAG_NONE
);
387 explicit NodeManager(ExprManager
* exprManager
);
388 explicit NodeManager(ExprManager
* exprManager
, const Options
& options
);
391 /** The node manager in the current public-facing CVC4 library context */
392 static NodeManager
* currentNM() { return s_current
; }
393 /** The resource manager associated with the current node manager */
394 static ResourceManager
* currentResourceManager() { return s_current
->d_resourceManager
; }
396 /** Get this node manager's options (const version) */
397 const Options
& getOptions() const {
401 /** Get this node manager's options (non-const version) */
402 Options
& getOptions() {
406 /** Get this node manager's resource manager */
407 ResourceManager
* getResourceManager() { return d_resourceManager
; }
409 /** Get this node manager's statistics registry */
410 StatisticsRegistry
* getStatisticsRegistry() const
412 return d_statisticsRegistry
;
415 /** Subscribe to NodeManager events */
416 void subscribeEvents(NodeManagerListener
* listener
) {
417 Assert(std::find(d_listeners
.begin(), d_listeners
.end(), listener
)
418 == d_listeners
.end())
419 << "listener already subscribed";
420 d_listeners
.push_back(listener
);
423 /** Unsubscribe from NodeManager events */
424 void unsubscribeEvents(NodeManagerListener
* listener
) {
425 std::vector
<NodeManagerListener
*>::iterator elt
= std::find(d_listeners
.begin(), d_listeners
.end(), listener
);
426 Assert(elt
!= d_listeners
.end()) << "listener not subscribed";
427 d_listeners
.erase(elt
);
430 /** register datatype */
431 size_t registerDatatype(std::shared_ptr
<DType
> dt
);
433 * Return the datatype at the given index owned by this class. Type nodes are
434 * associated with datatypes through the DatatypeIndexConstant class. The
435 * argument index is intended to be a value taken from that class.
437 * Type nodes must access their DTypes through a level of indirection to
438 * prevent cycles in the Node AST (as DTypes themselves contain Nodes), which
439 * would lead to memory leaks. Thus TypeNode are given a DatatypeIndexConstant
440 * which is used as an index to retrieve the DType via this call.
442 const DType
& getDTypeForIndex(unsigned index
) const;
444 /** Get a Kind from an operator expression */
445 static inline Kind
operatorToKind(TNode n
);
447 // general expression-builders
449 /** Create a node with one child. */
450 Node
mkNode(Kind kind
, TNode child1
);
451 Node
* mkNodePtr(Kind kind
, TNode child1
);
453 /** Create a node with two children. */
454 Node
mkNode(Kind kind
, TNode child1
, TNode child2
);
455 Node
* mkNodePtr(Kind kind
, TNode child1
, TNode child2
);
457 /** Create a node with three children. */
458 Node
mkNode(Kind kind
, TNode child1
, TNode child2
, TNode child3
);
459 Node
* mkNodePtr(Kind kind
, TNode child1
, TNode child2
, TNode child3
);
461 /** Create a node with four children. */
462 Node
mkNode(Kind kind
, TNode child1
, TNode child2
, TNode child3
,
464 Node
* mkNodePtr(Kind kind
, TNode child1
, TNode child2
, TNode child3
,
467 /** Create a node with five children. */
468 Node
mkNode(Kind kind
, TNode child1
, TNode child2
, TNode child3
,
469 TNode child4
, TNode child5
);
470 Node
* mkNodePtr(Kind kind
, TNode child1
, TNode child2
, TNode child3
,
471 TNode child4
, TNode child5
);
473 /** Create a node with an arbitrary number of children. */
474 template <bool ref_count
>
475 Node
mkNode(Kind kind
, const std::vector
<NodeTemplate
<ref_count
> >& children
);
476 template <bool ref_count
>
477 Node
* mkNodePtr(Kind kind
, const std::vector
<NodeTemplate
<ref_count
> >& children
);
479 /** Create a node (with no children) by operator. */
480 Node
mkNode(TNode opNode
);
481 Node
* mkNodePtr(TNode opNode
);
483 /** Create a node with one child by operator. */
484 Node
mkNode(TNode opNode
, TNode child1
);
485 Node
* mkNodePtr(TNode opNode
, TNode child1
);
487 /** Create a node with two children by operator. */
488 Node
mkNode(TNode opNode
, TNode child1
, TNode child2
);
489 Node
* mkNodePtr(TNode opNode
, TNode child1
, TNode child2
);
491 /** Create a node with three children by operator. */
492 Node
mkNode(TNode opNode
, TNode child1
, TNode child2
, TNode child3
);
493 Node
* mkNodePtr(TNode opNode
, TNode child1
, TNode child2
, TNode child3
);
495 /** Create a node with four children by operator. */
496 Node
mkNode(TNode opNode
, TNode child1
, TNode child2
, TNode child3
,
498 Node
* mkNodePtr(TNode opNode
, TNode child1
, TNode child2
, TNode child3
,
501 /** Create a node with five children by operator. */
502 Node
mkNode(TNode opNode
, TNode child1
, TNode child2
, TNode child3
,
503 TNode child4
, TNode child5
);
504 Node
* mkNodePtr(TNode opNode
, TNode child1
, TNode child2
, TNode child3
,
505 TNode child4
, TNode child5
);
507 /** Create a node by applying an operator to the children. */
508 template <bool ref_count
>
509 Node
mkNode(TNode opNode
, const std::vector
<NodeTemplate
<ref_count
> >& children
);
510 template <bool ref_count
>
511 Node
* mkNodePtr(TNode opNode
, const std::vector
<NodeTemplate
<ref_count
> >& children
);
513 Node
mkBoundVar(const std::string
& name
, const TypeNode
& type
);
514 Node
* mkBoundVarPtr(const std::string
& name
, const TypeNode
& type
);
516 Node
mkBoundVar(const TypeNode
& type
);
517 Node
* mkBoundVarPtr(const TypeNode
& type
);
519 /** get the canonical bound variable list for function type tn */
520 static Node
getBoundVarListForFunctionType( TypeNode tn
);
523 * Optional flags used to control behavior of NodeManager::mkSkolem().
524 * They should be composed with a bitwise OR (e.g.,
525 * "SKOLEM_NO_NOTIFY | SKOLEM_EXACT_NAME"). Of course, SKOLEM_DEFAULT
526 * cannot be composed in such a manner.
529 SKOLEM_DEFAULT
= 0, /**< default behavior */
530 SKOLEM_NO_NOTIFY
= 1, /**< do not notify subscribers */
531 SKOLEM_EXACT_NAME
= 2,/**< do not make the name unique by adding the id */
532 SKOLEM_IS_GLOBAL
= 4 /**< global vars appear in models even after a pop */
533 };/* enum SkolemFlags */
536 * Create a skolem constant with the given name, type, and comment.
538 * @param prefix the name of the new skolem variable is the prefix
539 * appended with a unique ID. This way a family of skolem variables
540 * can be made with unique identifiers, used in dump, tracing, and
541 * debugging output. Use SKOLEM_EXECT_NAME flag if you don't want
542 * a unique ID appended and use prefix as the name.
544 * @param type the type of the skolem variable to create
546 * @param comment a comment for dumping output; if declarations are
547 * being dumped, this is included in a comment before the declaration
548 * and can be quite useful for debugging
550 * @param flags an optional mask of bits from SkolemFlags to control
551 * mkSkolem() behavior
553 Node
mkSkolem(const std::string
& prefix
, const TypeNode
& type
,
554 const std::string
& comment
= "", int flags
= SKOLEM_DEFAULT
);
556 /** Create a instantiation constant with the given type. */
557 Node
mkInstConstant(const TypeNode
& type
);
559 /** Create a boolean term variable. */
560 Node
mkBooleanTermVariable();
562 /** Make a new abstract value with the given type. */
563 Node
mkAbstractValue(const TypeNode
& type
);
565 /** make unique (per Type,Kind) variable. */
566 Node
mkNullaryOperator(const TypeNode
& type
, Kind k
);
569 * Create a constant of type T. It will have the appropriate
570 * CONST_* kind defined for T.
573 Node
mkConst(const T
&);
576 TypeNode
mkTypeConst(const T
&);
578 template <class NodeClass
, class T
>
579 NodeClass
mkConstInternal(const T
&);
581 /** Create a node with children. */
582 TypeNode
mkTypeNode(Kind kind
, TypeNode child1
);
583 TypeNode
mkTypeNode(Kind kind
, TypeNode child1
, TypeNode child2
);
584 TypeNode
mkTypeNode(Kind kind
, TypeNode child1
, TypeNode child2
,
586 TypeNode
mkTypeNode(Kind kind
, const std::vector
<TypeNode
>& children
);
589 * Determine whether Nodes of a particular Kind have operators.
590 * @returns true if Nodes of Kind k have operators.
592 static inline bool hasOperator(Kind k
);
595 * Get the (singleton) operator of an OPERATOR-kinded kind. The
596 * returned node n will have kind BUILTIN, and calling
597 * n.getConst<CVC4::Kind>() will yield k.
599 inline TNode
operatorOf(Kind k
) {
600 AssertArgument( kind::metaKindOf(k
) == kind::metakind::OPERATOR
, k
,
601 "Kind is not an OPERATOR-kinded kind "
602 "in NodeManager::operatorOf()" );
603 return d_operators
[k
];
607 * Retrieve an attribute for a node.
609 * @param nv the node value
610 * @param attr an instance of the attribute kind to retrieve.
611 * @returns the attribute, if set, or a default-constructed
612 * <code>AttrKind::value_type</code> if not.
614 template <class AttrKind
>
615 inline typename
AttrKind::value_type
getAttribute(expr::NodeValue
* nv
,
616 const AttrKind
& attr
) const;
619 * Check whether an attribute is set for a node.
621 * @param nv the node value
622 * @param attr an instance of the attribute kind to check
623 * @returns <code>true</code> iff <code>attr</code> is set for
626 template <class AttrKind
>
627 inline bool hasAttribute(expr::NodeValue
* nv
,
628 const AttrKind
& attr
) const;
631 * Check whether an attribute is set for a node, and, if so,
634 * @param nv the node value
635 * @param attr an instance of the attribute kind to check
636 * @param value a reference to an object of the attribute's value type.
637 * <code>value</code> will be set to the value of the attribute, if it is
638 * set for <code>nv</code>; otherwise, it will be set to the default
639 * value of the attribute.
640 * @returns <code>true</code> iff <code>attr</code> is set for
643 template <class AttrKind
>
644 inline bool getAttribute(expr::NodeValue
* nv
,
645 const AttrKind
& attr
,
646 typename
AttrKind::value_type
& value
) const;
649 * Set an attribute for a node. If the node doesn't have the
650 * attribute, this function assigns one. If the node has one, this
653 * @param nv the node value
654 * @param attr an instance of the attribute kind to set
655 * @param value the value of <code>attr</code> for <code>nv</code>
657 template <class AttrKind
>
658 inline void setAttribute(expr::NodeValue
* nv
,
659 const AttrKind
& attr
,
660 const typename
AttrKind::value_type
& value
);
663 * Retrieve an attribute for a TNode.
666 * @param attr an instance of the attribute kind to retrieve.
667 * @returns the attribute, if set, or a default-constructed
668 * <code>AttrKind::value_type</code> if not.
670 template <class AttrKind
>
671 inline typename
AttrKind::value_type
672 getAttribute(TNode n
, const AttrKind
& attr
) const;
675 * Check whether an attribute is set for a TNode.
678 * @param attr an instance of the attribute kind to check
679 * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
681 template <class AttrKind
>
682 inline bool hasAttribute(TNode n
,
683 const AttrKind
& attr
) const;
686 * Check whether an attribute is set for a TNode and, if so, retieve
690 * @param attr an instance of the attribute kind to check
691 * @param value a reference to an object of the attribute's value type.
692 * <code>value</code> will be set to the value of the attribute, if it is
693 * set for <code>nv</code>; otherwise, it will be set to the default value of
695 * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
697 template <class AttrKind
>
698 inline bool getAttribute(TNode n
,
699 const AttrKind
& attr
,
700 typename
AttrKind::value_type
& value
) const;
703 * Set an attribute for a node. If the node doesn't have the
704 * attribute, this function assigns one. If the node has one, this
708 * @param attr an instance of the attribute kind to set
709 * @param value the value of <code>attr</code> for <code>n</code>
711 template <class AttrKind
>
712 inline void setAttribute(TNode n
,
713 const AttrKind
& attr
,
714 const typename
AttrKind::value_type
& value
);
717 * Retrieve an attribute for a TypeNode.
719 * @param n the type node
720 * @param attr an instance of the attribute kind to retrieve.
721 * @returns the attribute, if set, or a default-constructed
722 * <code>AttrKind::value_type</code> if not.
724 template <class AttrKind
>
725 inline typename
AttrKind::value_type
726 getAttribute(TypeNode n
, const AttrKind
& attr
) const;
729 * Check whether an attribute is set for a TypeNode.
731 * @param n the type node
732 * @param attr an instance of the attribute kind to check
733 * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
735 template <class AttrKind
>
736 inline bool hasAttribute(TypeNode n
,
737 const AttrKind
& attr
) const;
740 * Check whether an attribute is set for a TypeNode and, if so, retieve
743 * @param n the type node
744 * @param attr an instance of the attribute kind to check
745 * @param value a reference to an object of the attribute's value type.
746 * <code>value</code> will be set to the value of the attribute, if it is
747 * set for <code>nv</code>; otherwise, it will be set to the default value of
749 * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
751 template <class AttrKind
>
752 inline bool getAttribute(TypeNode n
,
753 const AttrKind
& attr
,
754 typename
AttrKind::value_type
& value
) const;
757 * Set an attribute for a type node. If the node doesn't have the
758 * attribute, this function assigns one. If the type node has one,
759 * this overwrites it.
761 * @param n the type node
762 * @param attr an instance of the attribute kind to set
763 * @param value the value of <code>attr</code> for <code>n</code>
765 template <class AttrKind
>
766 inline void setAttribute(TypeNode n
,
767 const AttrKind
& attr
,
768 const typename
AttrKind::value_type
& value
);
770 /** Get the (singleton) type for Booleans. */
771 inline TypeNode
booleanType();
773 /** Get the (singleton) type for integers. */
774 inline TypeNode
integerType();
776 /** Get the (singleton) type for reals. */
777 inline TypeNode
realType();
779 /** Get the (singleton) type for strings. */
780 inline TypeNode
stringType();
782 /** Get the (singleton) type for RegExp. */
783 inline TypeNode
regExpType();
785 /** Get the (singleton) type for rounding modes. */
786 inline TypeNode
roundingModeType();
788 /** Get the bound var list type. */
789 inline TypeNode
boundVarListType();
791 /** Get the instantiation pattern type. */
792 inline TypeNode
instPatternType();
794 /** Get the instantiation pattern type. */
795 inline TypeNode
instPatternListType();
798 * Get the (singleton) type for builtin operators (that is, the type
799 * of the Node returned from Node::getOperator() when the operator
800 * is built-in, like EQUAL). */
801 inline TypeNode
builtinOperatorType();
804 * Make a function type from domain to range.
806 * @param domain the domain type
807 * @param range the range type
808 * @returns the functional type domain -> range
810 TypeNode
mkFunctionType(const TypeNode
& domain
, const TypeNode
& range
);
813 * Make a function type with input types from
814 * argTypes. <code>argTypes</code> must have at least one element.
816 * @param argTypes the domain is a tuple (argTypes[0], ..., argTypes[n])
817 * @param range the range type
818 * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range
820 TypeNode
mkFunctionType(const std::vector
<TypeNode
>& argTypes
,
821 const TypeNode
& range
);
824 * Make a function type with input types from
825 * <code>sorts[0..sorts.size()-2]</code> and result type
826 * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
827 * at least 2 elements.
829 TypeNode
mkFunctionType(const std::vector
<TypeNode
>& sorts
);
832 * Make a predicate type with input types from
833 * <code>sorts</code>. The result with be a function type with range
834 * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
837 TypeNode
mkPredicateType(const std::vector
<TypeNode
>& sorts
);
840 * Make a tuple type with types from
841 * <code>types</code>. <code>types</code> must have at least one
844 * @param types a vector of types
845 * @returns the tuple type (types[0], ..., types[n])
847 TypeNode
mkTupleType(const std::vector
<TypeNode
>& types
);
850 * Make a record type with the description from rec.
852 * @param rec a description of the record
853 * @returns the record type
855 TypeNode
mkRecordType(const Record
& rec
);
858 * Make a symbolic expression type with types from
859 * <code>types</code>. <code>types</code> may have any number of
862 * @param types a vector of types
863 * @returns the symbolic expression type (types[0], ..., types[n])
865 inline TypeNode
mkSExprType(const std::vector
<TypeNode
>& types
);
867 /** Make the type of floating-point with <code>exp</code> bit exponent and
868 <code>sig</code> bit significand */
869 inline TypeNode
mkFloatingPointType(unsigned exp
, unsigned sig
);
870 inline TypeNode
mkFloatingPointType(FloatingPointSize fs
);
872 /** Make the type of bitvectors of size <code>size</code> */
873 inline TypeNode
mkBitVectorType(unsigned size
);
875 /** Make the type of arrays with the given parameterization */
876 inline TypeNode
mkArrayType(TypeNode indexType
, TypeNode constituentType
);
878 /** Make the type of arrays with the given parameterization */
879 inline TypeNode
mkSetType(TypeNode elementType
);
881 /** Make a type representing a constructor with the given parameterization */
882 TypeNode
mkConstructorType(const DatatypeConstructor
& constructor
, TypeNode range
);
884 * Make a type representing a constructor with the given argument (subfield)
885 * types and return type range.
887 TypeNode
mkConstructorType(const std::vector
<TypeNode
>& args
, TypeNode range
);
889 /** Make a type representing a selector with the given parameterization */
890 inline TypeNode
mkSelectorType(TypeNode domain
, TypeNode range
);
892 /** Make a type representing a tester with given parameterization */
893 inline TypeNode
mkTesterType(TypeNode domain
);
895 /** Make a new (anonymous) sort of arity 0. */
896 TypeNode
mkSort(uint32_t flags
= ExprManager::SORT_FLAG_NONE
);
898 /** Make a new sort with the given name of arity 0. */
899 TypeNode
mkSort(const std::string
& name
, uint32_t flags
= ExprManager::SORT_FLAG_NONE
);
901 /** Make a new sort by parameterizing the given sort constructor. */
902 TypeNode
mkSort(TypeNode constructor
,
903 const std::vector
<TypeNode
>& children
,
904 uint32_t flags
= ExprManager::SORT_FLAG_NONE
);
906 /** Make a new sort with the given name and arity. */
907 TypeNode
mkSortConstructor(const std::string
& name
,
909 uint32_t flags
= ExprManager::SORT_FLAG_NONE
);
912 * Get the type for the given node and optionally do type checking.
914 * Initial type computation will be near-constant time if
915 * type checking is not requested. Results are memoized, so that
916 * subsequent calls to getType() without type checking will be
919 * Initial type checking is linear in the size of the expression.
920 * Again, the results are memoized, so that subsequent calls to
921 * getType(), with or without type checking, will be constant
924 * NOTE: A TypeCheckingException can be thrown even when type
925 * checking is not requested. getType() will always return a
926 * valid and correct type and, thus, an exception will be thrown
927 * when no valid or correct type can be computed (e.g., if the
928 * arguments to a bit-vector operation aren't bit-vectors). When
929 * type checking is not requested, getType() will do the minimum
930 * amount of checking required to return a valid result.
932 * @param n the Node for which we want a type
933 * @param check whether we should check the type as we compute it
936 TypeNode
getType(TNode n
, bool check
= false);
939 * Convert a node to an expression. Uses the ExprManager
940 * associated to this NodeManager.
942 inline Expr
toExpr(TNode n
);
945 * Convert an expression to a node.
947 static inline Node
fromExpr(const Expr
& e
);
950 * Convert a node manager to an expression manager.
952 inline ExprManager
* toExprManager();
955 * Convert an expression manager to a node manager.
957 static inline NodeManager
* fromExprManager(ExprManager
* exprManager
);
960 * Convert a type node to a type.
962 inline Type
toType(TypeNode tn
);
965 * Convert a type to a type node.
967 static inline TypeNode
fromType(Type t
);
969 /** Reclaim zombies while there are more than k nodes in the pool (if possible).*/
970 void reclaimZombiesUntil(uint32_t k
);
972 /** Reclaims all zombies (if possible).*/
973 void reclaimAllZombies();
975 /** Size of the node pool. */
976 size_t poolSize() const;
978 /** Deletes a list of attributes from the NM's AttributeManager.*/
979 void deleteAttributes(const std::vector
< const expr::attr::AttributeUniqueId
* >& ids
);
982 * This function gives developers a hook into the NodeManager.
983 * This can be changed in node_manager.cpp without recompiling most of cvc4.
985 * debugHook is a debugging only function, and should not be present in
986 * any published code!
988 void debugHook(int debugFlag
);
989 };/* class NodeManager */
992 * This class changes the "current" thread-global
993 * <code>NodeManager</code> when it is created and reinstates the
994 * previous thread-global <code>NodeManager</code> when it is
995 * destroyed, effectively maintaining a set of nested
996 * <code>NodeManager</code> scopes. This is especially useful on
997 * public-interface calls into the CVC4 library, where CVC4's notion
998 * of the "current" <code>NodeManager</code> should be set to match
999 * the calling context. See, for example, the implementations of
1000 * public calls in the <code>ExprManager</code> and
1001 * <code>SmtEngine</code> classes.
1003 * The client must be careful to create and destroy
1004 * <code>NodeManagerScope</code> objects in a well-nested manner (such
1005 * as on the stack). You may create a <code>NodeManagerScope</code>
1006 * with <code>new</code> and destroy it with <code>delete</code>, or
1007 * place it as a data member of an object that is, but if the scope of
1008 * these <code>new</code>/<code>delete</code> pairs isn't properly
1009 * maintained, the incorrect "current" <code>NodeManager</code>
1010 * pointer may be restored after a delete.
1012 class NodeManagerScope
{
1013 /** The old NodeManager, to be restored on destruction. */
1014 NodeManager
* d_oldNodeManager
;
1015 Options::OptionsScope d_optionsScope
;
1018 NodeManagerScope(NodeManager
* nm
)
1019 : d_oldNodeManager(NodeManager::s_current
)
1020 , d_optionsScope(nm
? nm
->d_options
: NULL
) {
1021 // There are corner cases where nm can be NULL and it's ok.
1022 // For example, if you write { Expr e; }, then when the null
1023 // Expr is destructed, there's no active node manager.
1024 //Assert(nm != NULL);
1025 NodeManager::s_current
= nm
;
1026 //Options::s_current = nm ? nm->d_options : NULL;
1027 Debug("current") << "node manager scope: "
1028 << NodeManager::s_current
<< "\n";
1031 ~NodeManagerScope() {
1032 NodeManager::s_current
= d_oldNodeManager
;
1033 //Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL;
1034 Debug("current") << "node manager scope: "
1035 << "returning to " << NodeManager::s_current
<< "\n";
1037 };/* class NodeManagerScope */
1039 /** Get the (singleton) type for booleans. */
1040 inline TypeNode
NodeManager::booleanType() {
1041 return TypeNode(mkTypeConst
<TypeConstant
>(BOOLEAN_TYPE
));
1044 /** Get the (singleton) type for integers. */
1045 inline TypeNode
NodeManager::integerType() {
1046 return TypeNode(mkTypeConst
<TypeConstant
>(INTEGER_TYPE
));
1049 /** Get the (singleton) type for reals. */
1050 inline TypeNode
NodeManager::realType() {
1051 return TypeNode(mkTypeConst
<TypeConstant
>(REAL_TYPE
));
1054 /** Get the (singleton) type for strings. */
1055 inline TypeNode
NodeManager::stringType() {
1056 return TypeNode(mkTypeConst
<TypeConstant
>(STRING_TYPE
));
1059 /** Get the (singleton) type for regexps. */
1060 inline TypeNode
NodeManager::regExpType() {
1061 return TypeNode(mkTypeConst
<TypeConstant
>(REGEXP_TYPE
));
1064 /** Get the (singleton) type for rounding modes. */
1065 inline TypeNode
NodeManager::roundingModeType() {
1066 return TypeNode(mkTypeConst
<TypeConstant
>(ROUNDINGMODE_TYPE
));
1069 /** Get the bound var list type. */
1070 inline TypeNode
NodeManager::boundVarListType() {
1071 return TypeNode(mkTypeConst
<TypeConstant
>(BOUND_VAR_LIST_TYPE
));
1074 /** Get the instantiation pattern type. */
1075 inline TypeNode
NodeManager::instPatternType() {
1076 return TypeNode(mkTypeConst
<TypeConstant
>(INST_PATTERN_TYPE
));
1079 /** Get the instantiation pattern type. */
1080 inline TypeNode
NodeManager::instPatternListType() {
1081 return TypeNode(mkTypeConst
<TypeConstant
>(INST_PATTERN_LIST_TYPE
));
1084 /** Get the (singleton) type for builtin operators. */
1085 inline TypeNode
NodeManager::builtinOperatorType() {
1086 return TypeNode(mkTypeConst
<TypeConstant
>(BUILTIN_OPERATOR_TYPE
));
1089 inline TypeNode
NodeManager::mkSExprType(const std::vector
<TypeNode
>& types
) {
1090 std::vector
<TypeNode
> typeNodes
;
1091 for (unsigned i
= 0; i
< types
.size(); ++ i
) {
1092 typeNodes
.push_back(types
[i
]);
1094 return mkTypeNode(kind::SEXPR_TYPE
, typeNodes
);
1097 inline TypeNode
NodeManager::mkBitVectorType(unsigned size
) {
1098 return TypeNode(mkTypeConst
<BitVectorSize
>(BitVectorSize(size
)));
1101 inline TypeNode
NodeManager::mkFloatingPointType(unsigned exp
, unsigned sig
) {
1102 return TypeNode(mkTypeConst
<FloatingPointSize
>(FloatingPointSize(exp
,sig
)));
1105 inline TypeNode
NodeManager::mkFloatingPointType(FloatingPointSize fs
) {
1106 return TypeNode(mkTypeConst
<FloatingPointSize
>(fs
));
1109 inline TypeNode
NodeManager::mkArrayType(TypeNode indexType
,
1110 TypeNode constituentType
) {
1111 CheckArgument(!indexType
.isNull(), indexType
,
1112 "unexpected NULL index type");
1113 CheckArgument(!constituentType
.isNull(), constituentType
,
1114 "unexpected NULL constituent type");
1115 CheckArgument(indexType
.isFirstClass(),
1117 "cannot index arrays by types that are not first-class. Try "
1119 CheckArgument(constituentType
.isFirstClass(),
1121 "cannot store types that are not first-class in arrays. Try "
1123 Debug("arrays") << "making array type " << indexType
<< " "
1124 << constituentType
<< std::endl
;
1125 return mkTypeNode(kind::ARRAY_TYPE
, indexType
, constituentType
);
1128 inline TypeNode
NodeManager::mkSetType(TypeNode elementType
) {
1129 CheckArgument(!elementType
.isNull(), elementType
,
1130 "unexpected NULL element type");
1131 CheckArgument(elementType
.isFirstClass(),
1133 "cannot store types that are not first-class in sets. Try "
1135 Debug("sets") << "making sets type " << elementType
<< std::endl
;
1136 return mkTypeNode(kind::SET_TYPE
, elementType
);
1139 inline TypeNode
NodeManager::mkSelectorType(TypeNode domain
, TypeNode range
) {
1140 CheckArgument(domain
.isDatatype(), domain
,
1141 "cannot create non-datatype selector type");
1142 CheckArgument(range
.isFirstClass(),
1144 "cannot have selector fields that are not first-class types. "
1145 "Try option --uf-ho.");
1146 return mkTypeNode(kind::SELECTOR_TYPE
, domain
, range
);
1149 inline TypeNode
NodeManager::mkTesterType(TypeNode domain
) {
1150 CheckArgument(domain
.isDatatype(), domain
,
1151 "cannot create non-datatype tester");
1152 return mkTypeNode(kind::TESTER_TYPE
, domain
);
1155 inline expr::NodeValue
* NodeManager::poolLookup(expr::NodeValue
* nv
) const {
1156 NodeValuePool::const_iterator find
= d_nodeValuePool
.find(nv
);
1157 if(find
== d_nodeValuePool
.end()) {
1164 inline void NodeManager::poolInsert(expr::NodeValue
* nv
) {
1165 Assert(d_nodeValuePool
.find(nv
) == d_nodeValuePool
.end())
1166 << "NodeValue already in the pool!";
1167 d_nodeValuePool
.insert(nv
);// FIXME multithreading
1170 inline void NodeManager::poolRemove(expr::NodeValue
* nv
) {
1171 Assert(d_nodeValuePool
.find(nv
) != d_nodeValuePool
.end())
1172 << "NodeValue is not in the pool!";
1174 d_nodeValuePool
.erase(nv
);// FIXME multithreading
1177 inline Expr
NodeManager::toExpr(TNode n
) {
1178 return Expr(d_exprManager
, new Node(n
));
1181 inline Node
NodeManager::fromExpr(const Expr
& e
) {
1185 inline ExprManager
* NodeManager::toExprManager() {
1186 return d_exprManager
;
1189 inline NodeManager
* NodeManager::fromExprManager(ExprManager
* exprManager
) {
1190 return exprManager
->getNodeManager();
1193 inline Type
NodeManager::toType(TypeNode tn
) {
1194 return Type(this, new TypeNode(tn
));
1197 inline TypeNode
NodeManager::fromType(Type t
) {
1198 return *Type::getTypeNode(t
);
1201 }/* CVC4 namespace */
1203 #define CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
1204 #include "expr/metakind.h"
1205 #undef CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
1207 #include "expr/node_builder.h"
1211 // general expression-builders
1213 inline bool NodeManager::hasOperator(Kind k
) {
1214 switch(kind::MetaKind mk
= kind::metaKindOf(k
)) {
1216 case kind::metakind::INVALID
:
1217 case kind::metakind::VARIABLE
:
1218 case kind::metakind::NULLARY_OPERATOR
:
1221 case kind::metakind::OPERATOR
:
1222 case kind::metakind::PARAMETERIZED
:
1225 case kind::metakind::CONSTANT
:
1228 default: Unhandled() << mk
;
1232 inline Kind
NodeManager::operatorToKind(TNode n
) {
1233 return kind::operatorToKind(n
.d_nv
);
1236 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
) {
1237 NodeBuilder
<1> nb(this, kind
);
1239 return nb
.constructNode();
1242 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
) {
1243 NodeBuilder
<1> nb(this, kind
);
1245 return nb
.constructNodePtr();
1248 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
, TNode child2
) {
1249 NodeBuilder
<2> nb(this, kind
);
1250 nb
<< child1
<< child2
;
1251 return nb
.constructNode();
1254 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
, TNode child2
) {
1255 NodeBuilder
<2> nb(this, kind
);
1256 nb
<< child1
<< child2
;
1257 return nb
.constructNodePtr();
1260 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
, TNode child2
,
1262 NodeBuilder
<3> nb(this, kind
);
1263 nb
<< child1
<< child2
<< child3
;
1264 return nb
.constructNode();
1267 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
, TNode child2
,
1269 NodeBuilder
<3> nb(this, kind
);
1270 nb
<< child1
<< child2
<< child3
;
1271 return nb
.constructNodePtr();
1274 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
, TNode child2
,
1275 TNode child3
, TNode child4
) {
1276 NodeBuilder
<4> nb(this, kind
);
1277 nb
<< child1
<< child2
<< child3
<< child4
;
1278 return nb
.constructNode();
1281 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
, TNode child2
,
1282 TNode child3
, TNode child4
) {
1283 NodeBuilder
<4> nb(this, kind
);
1284 nb
<< child1
<< child2
<< child3
<< child4
;
1285 return nb
.constructNodePtr();
1288 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
, TNode child2
,
1289 TNode child3
, TNode child4
, TNode child5
) {
1290 NodeBuilder
<5> nb(this, kind
);
1291 nb
<< child1
<< child2
<< child3
<< child4
<< child5
;
1292 return nb
.constructNode();
1295 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
, TNode child2
,
1296 TNode child3
, TNode child4
, TNode child5
) {
1297 NodeBuilder
<5> nb(this, kind
);
1298 nb
<< child1
<< child2
<< child3
<< child4
<< child5
;
1299 return nb
.constructNodePtr();
1303 template <bool ref_count
>
1304 inline Node
NodeManager::mkNode(Kind kind
,
1305 const std::vector
<NodeTemplate
<ref_count
> >&
1307 NodeBuilder
<> nb(this, kind
);
1308 nb
.append(children
);
1309 return nb
.constructNode();
1312 template <bool ref_count
>
1313 inline Node
* NodeManager::mkNodePtr(Kind kind
,
1314 const std::vector
<NodeTemplate
<ref_count
> >&
1316 NodeBuilder
<> nb(this, kind
);
1317 nb
.append(children
);
1318 return nb
.constructNodePtr();
1322 inline Node
NodeManager::mkNode(TNode opNode
) {
1323 NodeBuilder
<1> nb(this, operatorToKind(opNode
));
1324 if(opNode
.getKind() != kind::BUILTIN
) {
1327 return nb
.constructNode();
1330 inline Node
* NodeManager::mkNodePtr(TNode opNode
) {
1331 NodeBuilder
<1> nb(this, operatorToKind(opNode
));
1332 if(opNode
.getKind() != kind::BUILTIN
) {
1335 return nb
.constructNodePtr();
1338 inline Node
NodeManager::mkNode(TNode opNode
, TNode child1
) {
1339 NodeBuilder
<2> nb(this, operatorToKind(opNode
));
1340 if(opNode
.getKind() != kind::BUILTIN
) {
1344 return nb
.constructNode();
1347 inline Node
* NodeManager::mkNodePtr(TNode opNode
, TNode child1
) {
1348 NodeBuilder
<2> nb(this, operatorToKind(opNode
));
1349 if(opNode
.getKind() != kind::BUILTIN
) {
1353 return nb
.constructNodePtr();
1356 inline Node
NodeManager::mkNode(TNode opNode
, TNode child1
, TNode child2
) {
1357 NodeBuilder
<3> nb(this, operatorToKind(opNode
));
1358 if(opNode
.getKind() != kind::BUILTIN
) {
1361 nb
<< child1
<< child2
;
1362 return nb
.constructNode();
1365 inline Node
* NodeManager::mkNodePtr(TNode opNode
, TNode child1
, TNode child2
) {
1366 NodeBuilder
<3> nb(this, operatorToKind(opNode
));
1367 if(opNode
.getKind() != kind::BUILTIN
) {
1370 nb
<< child1
<< child2
;
1371 return nb
.constructNodePtr();
1374 inline Node
NodeManager::mkNode(TNode opNode
, TNode child1
, TNode child2
,
1376 NodeBuilder
<4> nb(this, operatorToKind(opNode
));
1377 if(opNode
.getKind() != kind::BUILTIN
) {
1380 nb
<< child1
<< child2
<< child3
;
1381 return nb
.constructNode();
1384 inline Node
* NodeManager::mkNodePtr(TNode opNode
, TNode child1
, TNode child2
,
1386 NodeBuilder
<4> nb(this, operatorToKind(opNode
));
1387 if(opNode
.getKind() != kind::BUILTIN
) {
1390 nb
<< child1
<< child2
<< child3
;
1391 return nb
.constructNodePtr();
1394 inline Node
NodeManager::mkNode(TNode opNode
, TNode child1
, TNode child2
,
1395 TNode child3
, TNode child4
) {
1396 NodeBuilder
<5> nb(this, operatorToKind(opNode
));
1397 if(opNode
.getKind() != kind::BUILTIN
) {
1400 nb
<< child1
<< child2
<< child3
<< child4
;
1401 return nb
.constructNode();
1404 inline Node
* NodeManager::mkNodePtr(TNode opNode
, TNode child1
, TNode child2
,
1405 TNode child3
, TNode child4
) {
1406 NodeBuilder
<5> nb(this, operatorToKind(opNode
));
1407 if(opNode
.getKind() != kind::BUILTIN
) {
1410 nb
<< child1
<< child2
<< child3
<< child4
;
1411 return nb
.constructNodePtr();
1414 inline Node
NodeManager::mkNode(TNode opNode
, TNode child1
, TNode child2
,
1415 TNode child3
, TNode child4
, TNode child5
) {
1416 NodeBuilder
<6> nb(this, operatorToKind(opNode
));
1417 if(opNode
.getKind() != kind::BUILTIN
) {
1420 nb
<< child1
<< child2
<< child3
<< child4
<< child5
;
1421 return nb
.constructNode();
1424 inline Node
* NodeManager::mkNodePtr(TNode opNode
, TNode child1
, TNode child2
,
1425 TNode child3
, TNode child4
, TNode child5
) {
1426 NodeBuilder
<6> nb(this, operatorToKind(opNode
));
1427 if(opNode
.getKind() != kind::BUILTIN
) {
1430 nb
<< child1
<< child2
<< child3
<< child4
<< child5
;
1431 return nb
.constructNodePtr();
1434 // N-ary version for operators
1435 template <bool ref_count
>
1436 inline Node
NodeManager::mkNode(TNode opNode
,
1437 const std::vector
<NodeTemplate
<ref_count
> >&
1439 NodeBuilder
<> nb(this, operatorToKind(opNode
));
1440 if(opNode
.getKind() != kind::BUILTIN
) {
1443 nb
.append(children
);
1444 return nb
.constructNode();
1447 template <bool ref_count
>
1448 inline Node
* NodeManager::mkNodePtr(TNode opNode
,
1449 const std::vector
<NodeTemplate
<ref_count
> >&
1451 NodeBuilder
<> nb(this, operatorToKind(opNode
));
1452 if(opNode
.getKind() != kind::BUILTIN
) {
1455 nb
.append(children
);
1456 return nb
.constructNodePtr();
1460 inline TypeNode
NodeManager::mkTypeNode(Kind kind
, TypeNode child1
) {
1461 return (NodeBuilder
<1>(this, kind
) << child1
).constructTypeNode();
1464 inline TypeNode
NodeManager::mkTypeNode(Kind kind
, TypeNode child1
,
1466 return (NodeBuilder
<2>(this, kind
) << child1
<< child2
).constructTypeNode();
1469 inline TypeNode
NodeManager::mkTypeNode(Kind kind
, TypeNode child1
,
1470 TypeNode child2
, TypeNode child3
) {
1471 return (NodeBuilder
<3>(this, kind
) << child1
<< child2
<< child3
).constructTypeNode();
1474 // N-ary version for types
1475 inline TypeNode
NodeManager::mkTypeNode(Kind kind
,
1476 const std::vector
<TypeNode
>& children
) {
1477 return NodeBuilder
<>(this, kind
).append(children
).constructTypeNode();
1481 Node
NodeManager::mkConst(const T
& val
) {
1482 return mkConstInternal
<Node
, T
>(val
);
1486 TypeNode
NodeManager::mkTypeConst(const T
& val
) {
1487 return mkConstInternal
<TypeNode
, T
>(val
);
1490 template <class NodeClass
, class T
>
1491 NodeClass
NodeManager::mkConstInternal(const T
& val
) {
1493 // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
1494 NVStorage
<1> nvStorage
;
1495 expr::NodeValue
& nvStack
= reinterpret_cast<expr::NodeValue
&>(nvStorage
);
1498 nvStack
.d_kind
= kind::metakind::ConstantMap
<T
>::kind
;
1500 nvStack
.d_nchildren
= 1;
1502 #if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6))
1503 #pragma GCC diagnostic push
1504 #pragma GCC diagnostic ignored "-Warray-bounds"
1507 nvStack
.d_children
[0] =
1508 const_cast<expr::NodeValue
*>(reinterpret_cast<const expr::NodeValue
*>(&val
));
1509 expr::NodeValue
* nv
= poolLookup(&nvStack
);
1511 #if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6))
1512 #pragma GCC diagnostic pop
1516 return NodeClass(nv
);
1519 nv
= (expr::NodeValue
*)
1520 std::malloc(sizeof(expr::NodeValue
) + sizeof(T
));
1522 throw std::bad_alloc();
1525 nv
->d_nchildren
= 0;
1526 nv
->d_kind
= kind::metakind::ConstantMap
<T
>::kind
;
1527 nv
->d_id
= next_id
++;// FIXME multithreading
1530 //OwningTheory::mkConst(val);
1531 new (&nv
->d_children
) T(val
);
1534 if(Debug
.isOn("gc")) {
1535 Debug("gc") << "creating node value " << nv
1536 << " [" << nv
->d_id
<< "]: ";
1537 nv
->printAst(Debug("gc"));
1538 Debug("gc") << std::endl
;
1541 return NodeClass(nv
);
1544 }/* CVC4 namespace */
1546 #endif /* CVC4__NODE_MANAGER_H */