1 /********************* */
2 /*! \file node_manager.h
4 ** Top contributors (to current version):
5 ** Morgan Deters, Christopher L. Conway, Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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
;
51 class AttributeUniqueId
;
52 class AttributeManager
;
53 }/* CVC4::expr::attr namespace */
56 }/* CVC4::expr namespace */
59 * An interface that an interested party can implement and then subscribe
60 * to NodeManager events via NodeManager::subscribeEvents(this).
62 class NodeManagerListener
{
64 virtual ~NodeManagerListener() {}
65 virtual void nmNotifyNewSort(TypeNode tn
, uint32_t flags
) {}
66 virtual void nmNotifyNewSortConstructor(TypeNode tn
, uint32_t flags
) {}
67 virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor
, TypeNode sort
,
69 virtual void nmNotifyNewDatatypes(const std::vector
<TypeNode
>& datatypes
,
73 virtual void nmNotifyNewVar(TNode n
, uint32_t flags
) {}
74 virtual void nmNotifyNewSkolem(TNode n
, const std::string
& comment
,
77 * Notify a listener of a Node that's being GCed. If this function stores a
79 * to the Node somewhere, very bad things will happen.
81 virtual void nmNotifyDeleteNode(TNode n
) {}
82 }; /* class NodeManagerListener */
85 template <unsigned nchild_thresh
> friend class CVC4::NodeBuilder
;
86 friend class NodeManagerScope
;
87 friend class expr::NodeValue
;
88 friend class expr::TypeChecker
;
90 // friends so they can access mkVar() here, which is private
91 friend Expr
ExprManager::mkVar(const std::string
&, Type
, uint32_t flags
);
92 friend Expr
ExprManager::mkVar(Type
, uint32_t flags
);
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
;
108 StatisticsRegistry
* d_statisticsRegistry
;
110 /** The skolem manager */
111 std::shared_ptr
<SkolemManager
> d_skManager
;
113 NodeValuePool d_nodeValuePool
;
117 expr::attr::AttributeManager
* d_attrManager
;
119 /** The associated ExprManager */
120 ExprManager
* d_exprManager
;
123 * The node value we're currently freeing. This unique node value
124 * is permitted to have outstanding TNodes to it (in "soft"
125 * contexts, like as a key in attribute tables), even though
126 * normally it's an error to have a TNode to a node value with a
127 * reference count of 0. Being "under deletion" also enables
128 * assertions that inc() is not called on it.
130 expr::NodeValue
* d_nodeUnderDeletion
;
133 * True iff we are in reclaimZombies(). This avoids unnecessary
134 * recursion; a NodeValue being deleted might zombify other
135 * NodeValues, but these shouldn't trigger a (recursive) call to
138 bool d_inReclaimZombies
;
141 * The set of zombie nodes. We may want to revisit this design, as
142 * we might like to delete nodes in least-recently-used order. But
143 * we also need to avoid processing a zombie twice.
145 NodeValueIDSet d_zombies
;
148 * NodeValues with maxed out reference counts. These live as long as the
149 * NodeManager. They have a custom deallocation procedure at the very end.
151 std::vector
<expr::NodeValue
*> d_maxedOut
;
154 * A set of operator singletons (w.r.t. to this NodeManager
155 * instance) for operators. Conceptually, Nodes with kind, say,
156 * PLUS, are APPLYs of a PLUS operator to arguments. This array
157 * holds the set of operators for these things. A PLUS operator is
158 * a Node with kind "BUILTIN", and if you call
159 * plusOperator->getConst<CVC4::Kind>(), you get kind::PLUS back.
161 Node d_operators
[kind::LAST_KIND
];
163 /** unique vars per (Kind,Type) */
164 std::map
< Kind
, std::map
< TypeNode
, Node
> > d_unique_vars
;
167 * A list of subscribers for NodeManager events.
169 std::vector
<NodeManagerListener
*> d_listeners
;
171 /** A list of datatypes registered by its corresponding expr manager.
172 * !!! this member should be deleted when the Expr-layer is deleted.
174 std::vector
<std::shared_ptr
<DType
> > d_registeredDTypes
;
175 /** A list of datatypes owned by this node manager */
176 std::vector
<std::unique_ptr
<DType
> > d_ownedDTypes
;
179 * A map of tuple and record types to their corresponding datatype.
181 class TupleTypeCache
{
183 std::map
< TypeNode
, TupleTypeCache
> d_children
;
185 TypeNode
getTupleType( NodeManager
* nm
, std::vector
< TypeNode
>& types
, unsigned index
= 0 );
189 std::map
< TypeNode
, std::map
< std::string
, RecTypeCache
> > d_children
;
191 TypeNode
getRecordType( NodeManager
* nm
, const Record
& rec
, unsigned index
= 0 );
193 TupleTypeCache d_tt_cache
;
194 RecTypeCache d_rt_cache
;
197 * Keep a count of all abstract values produced by this NodeManager.
198 * Abstract values have a type attribute, so if multiple SmtEngines
199 * are attached to this NodeManager, we don't want their abstract
202 unsigned d_abstractValueCount
;
205 * A counter used to produce unique skolem names.
207 * Note that it is NOT incremented when skolems are created using
208 * SKOLEM_EXACT_NAME, so it is NOT a count of the skolems produced
209 * by this node manager.
211 unsigned d_skolemCounter
;
214 * Look up a NodeValue in the pool associated to this NodeManager.
215 * The NodeValue argument need not be a "completely-constructed"
216 * NodeValue. In particular, "non-inlined" constants are permitted
219 * For non-CONSTANT metakinds, nv's d_kind and d_nchildren should be
220 * correctly set, and d_children[0..n-1] should be valid (extant)
221 * NodeValues for lookup.
223 * For CONSTANT metakinds, nv's d_kind should be set correctly.
224 * Normally a CONSTANT would have d_nchildren == 0 and the constant
225 * value inlined in the d_children space. However, here we permit
226 * "non-inlined" NodeValues to avoid unnecessary copying. For
227 * these, d_nchildren == 1, and d_nchildren is a pointer to the
230 * The point of this complex design is to permit efficient lookups
231 * (without fully constructing a NodeValue). In the case that the
232 * argument is not fully constructed, and this function returns
233 * NULL, the caller should fully construct an equivalent one before
234 * calling poolInsert(). NON-FULLY-CONSTRUCTED NODEVALUES are not
235 * permitted in the pool!
237 inline expr::NodeValue
* poolLookup(expr::NodeValue
* nv
) const;
240 * Insert a NodeValue into the NodeManager's pool.
242 * It is an error to insert a NodeValue already in the pool.
243 * Enquire first with poolLookup().
245 inline void poolInsert(expr::NodeValue
* nv
);
248 * Remove a NodeValue from the NodeManager's pool.
250 * It is an error to request the removal of a NodeValue from the
251 * pool that is not in the pool.
253 inline void poolRemove(expr::NodeValue
* nv
);
256 * Determine if nv is currently being deleted by the NodeManager.
258 inline bool isCurrentlyDeleting(const expr::NodeValue
* nv
) const {
259 return d_nodeUnderDeletion
== nv
;
263 * Register a NodeValue as a zombie.
265 inline void markForDeletion(expr::NodeValue
* nv
) {
266 Assert(nv
->d_rc
== 0);
268 // if d_reclaiming is set, make sure we don't call
269 // reclaimZombies(), because it's already running.
270 if(Debug
.isOn("gc")) {
271 Debug("gc") << "zombifying node value " << nv
272 << " [" << nv
->d_id
<< "]: ";
273 nv
->printAst(Debug("gc"));
274 Debug("gc") << (d_inReclaimZombies
? " [CURRENTLY-RECLAIMING]" : "")
278 // `d_zombies` uses the node id to hash and compare nodes. If `d_zombies`
279 // already contains a node value with the same id as `nv`, but the pointers
280 // are different, then the wrong `NodeManager` was in scope for one of the
281 // two nodes when it reached refcount zero. This can happen for example if
282 // you create a node with a `NodeManager` n1 and then call `Node::toExpr()`
283 // on that node while a different `NodeManager` n2 is in scope. When that
284 // `Expr` is deleted and the node reaches refcount zero in the `Expr`'s
285 // destructor, then `markForDeletion()` will be called on n2.
286 Assert(d_zombies
.find(nv
) == d_zombies
.end() || *d_zombies
.find(nv
) == nv
);
288 d_zombies
.insert(nv
); // FIXME multithreading
290 if(safeToReclaimZombies()) {
291 if(d_zombies
.size() > 5000) {
298 * Register a NodeValue as having a maxed out reference count. This NodeValue
299 * will live as long as its containing NodeManager.
301 inline void markRefCountMaxedOut(expr::NodeValue
* nv
) {
302 Assert(nv
->HasMaximizedReferenceCount());
303 if(Debug
.isOn("gc")) {
304 Debug("gc") << "marking node value " << nv
305 << " [" << nv
->d_id
<< "]: as maxed out" << std::endl
;
307 d_maxedOut
.push_back(nv
);
311 * Reclaim all zombies.
313 void reclaimZombies();
316 * It is safe to collect zombies.
318 bool safeToReclaimZombies() const;
321 * Returns a reverse topological sort of a list of NodeValues. The NodeValues
322 * must be valid and have ids. The NodeValues are not modified (including ref
325 static std::vector
<expr::NodeValue
*> TopologicalSort(
326 const std::vector
<expr::NodeValue
*>& roots
);
329 * This template gives a mechanism to stack-allocate a NodeValue
330 * with enough space for N children (where N is a compile-time
331 * constant). You use it like this:
333 * NVStorage<4> nvStorage;
334 * NodeValue& nvStack = reinterpret_cast<NodeValue&>(nvStorage);
336 * ...and then you can use nvStack as a NodeValue that you know has
337 * room for 4 children.
342 expr::NodeValue
* child
[N
];
343 };/* struct NodeManager::NVStorage<N> */
345 /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
347 * It has been decided for now to hold off on implementations of
348 * these functions, as they may only be needed in CNF conversion,
349 * where it's pointless to do a lazy isAtomic determination by
350 * searching through the DAG, and storing it, since the result will
351 * only be used once. For more details see the 4/27/2010 CVC4
352 * developer's meeting notes at:
354 * http://cvc4.cs.stanford.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
356 // bool containsDecision(TNode); // is "atomic"
357 // bool properlyContainsDecision(TNode); // all children are atomic
359 // undefined private copy constructor (disallow copy)
360 NodeManager(const NodeManager
&) = delete;
362 NodeManager
& operator=(const NodeManager
&) = delete;
367 * Create a variable with the given name and type. NOTE that no
368 * lookup is done on the name. If you mkVar("a", type) and then
369 * mkVar("a", type) again, you have two variables. The NodeManager
370 * version of this is private to avoid internal uses of mkVar() from
371 * within CVC4. Such uses should employ mkSkolem() instead.
373 Node
mkVar(const std::string
& name
, const TypeNode
& type
, uint32_t flags
= ExprManager::VAR_FLAG_NONE
);
374 Node
* mkVarPtr(const std::string
& name
, const TypeNode
& type
, uint32_t flags
= ExprManager::VAR_FLAG_NONE
);
376 /** Create a variable with the given type. */
377 Node
mkVar(const TypeNode
& type
, uint32_t flags
= ExprManager::VAR_FLAG_NONE
);
378 Node
* mkVarPtr(const TypeNode
& type
, uint32_t flags
= ExprManager::VAR_FLAG_NONE
);
382 explicit NodeManager(ExprManager
* exprManager
);
385 /** The node manager in the current public-facing CVC4 library context */
386 static NodeManager
* currentNM() { return s_current
; }
387 /** Get this node manager's skolem manager */
388 SkolemManager
* getSkolemManager() { return d_skManager
.get(); }
390 /** Get this node manager's statistics registry */
391 StatisticsRegistry
* getStatisticsRegistry() const
393 return d_statisticsRegistry
;
396 /** Subscribe to NodeManager events */
397 void subscribeEvents(NodeManagerListener
* listener
) {
398 Assert(std::find(d_listeners
.begin(), d_listeners
.end(), listener
)
399 == d_listeners
.end())
400 << "listener already subscribed";
401 d_listeners
.push_back(listener
);
404 /** Unsubscribe from NodeManager events */
405 void unsubscribeEvents(NodeManagerListener
* listener
) {
406 std::vector
<NodeManagerListener
*>::iterator elt
= std::find(d_listeners
.begin(), d_listeners
.end(), listener
);
407 Assert(elt
!= d_listeners
.end()) << "listener not subscribed";
408 d_listeners
.erase(elt
);
411 /** register that datatype dt was constructed by the expression manager
412 * !!! this interface should be deleted when the Expr-layer is deleted.
414 size_t registerDatatype(std::shared_ptr
<DType
> dt
);
416 * Return the datatype at the given index owned by this class. Type nodes are
417 * associated with datatypes through the DatatypeIndexConstant class. The
418 * argument index is intended to be a value taken from that class.
420 * Type nodes must access their DTypes through a level of indirection to
421 * prevent cycles in the Node AST (as DTypes themselves contain Nodes), which
422 * would lead to memory leaks. Thus TypeNode are given a DatatypeIndexConstant
423 * which is used as an index to retrieve the DType via this call.
425 const DType
& getDTypeForIndex(size_t index
) const;
427 /** Get a Kind from an operator expression */
428 static inline Kind
operatorToKind(TNode n
);
430 /** Get corresponding application kind for function
432 * Different functional nodes are applied differently, according to their
433 * type. For example, uninterpreted functions (of FUNCTION_TYPE) are applied
434 * via APPLY_UF, while constructors (of CONSTRUCTOR_TYPE) via
435 * APPLY_CONSTRUCTOR. This method provides the correct application according
436 * to which functional type fun has.
438 * @param fun The functional node
439 * @return the correct application kind for fun. If fun's type is not function
440 * like (see TypeNode::isFunctionLike), then UNDEFINED_KIND is returned.
442 static Kind
getKindForFunction(TNode fun
);
444 // general expression-builders
446 /** Create a node with one child. */
447 Node
mkNode(Kind kind
, TNode child1
);
448 Node
* mkNodePtr(Kind kind
, TNode child1
);
450 /** Create a node with two children. */
451 Node
mkNode(Kind kind
, TNode child1
, TNode child2
);
452 Node
* mkNodePtr(Kind kind
, TNode child1
, TNode child2
);
454 /** Create a node with three children. */
455 Node
mkNode(Kind kind
, TNode child1
, TNode child2
, TNode child3
);
456 Node
* mkNodePtr(Kind kind
, TNode child1
, TNode child2
, TNode child3
);
458 /** Create a node with four children. */
459 Node
mkNode(Kind kind
, TNode child1
, TNode child2
, TNode child3
,
461 Node
* mkNodePtr(Kind kind
, TNode child1
, TNode child2
, TNode child3
,
464 /** Create a node with five children. */
465 Node
mkNode(Kind kind
, TNode child1
, TNode child2
, TNode child3
,
466 TNode child4
, TNode child5
);
467 Node
* mkNodePtr(Kind kind
, TNode child1
, TNode child2
, TNode child3
,
468 TNode child4
, TNode child5
);
470 /** Create a node with an arbitrary number of children. */
471 template <bool ref_count
>
472 Node
mkNode(Kind kind
, const std::vector
<NodeTemplate
<ref_count
> >& children
);
473 template <bool ref_count
>
474 Node
* mkNodePtr(Kind kind
, const std::vector
<NodeTemplate
<ref_count
> >& children
);
477 * Create an AND node with arbitrary number of children. This returns the
478 * true node if children is empty, or the single node in children if
479 * it contains only one node.
481 * We define construction of AND as a special case here since it is widely
482 * used for e.g. constructing explanations.
484 template <bool ref_count
>
485 Node
mkAnd(const std::vector
<NodeTemplate
<ref_count
> >& children
);
487 /** Create a node (with no children) by operator. */
488 Node
mkNode(TNode opNode
);
489 Node
* mkNodePtr(TNode opNode
);
491 /** Create a node with one child by operator. */
492 Node
mkNode(TNode opNode
, TNode child1
);
493 Node
* mkNodePtr(TNode opNode
, TNode child1
);
495 /** Create a node with two children by operator. */
496 Node
mkNode(TNode opNode
, TNode child1
, TNode child2
);
497 Node
* mkNodePtr(TNode opNode
, TNode child1
, TNode child2
);
499 /** Create a node with three children by operator. */
500 Node
mkNode(TNode opNode
, TNode child1
, TNode child2
, TNode child3
);
501 Node
* mkNodePtr(TNode opNode
, TNode child1
, TNode child2
, TNode child3
);
503 /** Create a node with four children by operator. */
504 Node
mkNode(TNode opNode
, TNode child1
, TNode child2
, TNode child3
,
506 Node
* mkNodePtr(TNode opNode
, TNode child1
, TNode child2
, TNode child3
,
509 /** Create a node with five children by operator. */
510 Node
mkNode(TNode opNode
, TNode child1
, TNode child2
, TNode child3
,
511 TNode child4
, TNode child5
);
512 Node
* mkNodePtr(TNode opNode
, TNode child1
, TNode child2
, TNode child3
,
513 TNode child4
, TNode child5
);
515 /** Create a node by applying an operator to the children. */
516 template <bool ref_count
>
517 Node
mkNode(TNode opNode
, const std::vector
<NodeTemplate
<ref_count
> >& children
);
518 template <bool ref_count
>
519 Node
* mkNodePtr(TNode opNode
, const std::vector
<NodeTemplate
<ref_count
> >& children
);
521 Node
mkBoundVar(const std::string
& name
, const TypeNode
& type
);
522 Node
* mkBoundVarPtr(const std::string
& name
, const TypeNode
& type
);
524 Node
mkBoundVar(const TypeNode
& type
);
525 Node
* mkBoundVarPtr(const TypeNode
& type
);
527 /** get the canonical bound variable list for function type tn */
528 Node
getBoundVarListForFunctionType( TypeNode tn
);
531 * Optional flags used to control behavior of NodeManager::mkSkolem().
532 * They should be composed with a bitwise OR (e.g.,
533 * "SKOLEM_NO_NOTIFY | SKOLEM_EXACT_NAME"). Of course, SKOLEM_DEFAULT
534 * cannot be composed in such a manner.
538 SKOLEM_DEFAULT
= 0, /**< default behavior */
539 SKOLEM_NO_NOTIFY
= 1, /**< do not notify subscribers */
540 SKOLEM_EXACT_NAME
= 2, /**< do not make the name unique by adding the id */
541 SKOLEM_IS_GLOBAL
= 4, /**< global vars appear in models even after a pop */
542 SKOLEM_BOOL_TERM_VAR
= 8 /**< vars requiring kind BOOLEAN_TERM_VARIABLE */
543 }; /* enum SkolemFlags */
546 * Create a skolem constant with the given name, type, and comment.
548 * @param prefix the name of the new skolem variable is the prefix
549 * appended with a unique ID. This way a family of skolem variables
550 * can be made with unique identifiers, used in dump, tracing, and
551 * debugging output. Use SKOLEM_EXECT_NAME flag if you don't want
552 * a unique ID appended and use prefix as the name.
554 * @param type the type of the skolem variable to create
556 * @param comment a comment for dumping output; if declarations are
557 * being dumped, this is included in a comment before the declaration
558 * and can be quite useful for debugging
560 * @param flags an optional mask of bits from SkolemFlags to control
561 * mkSkolem() behavior
563 Node
mkSkolem(const std::string
& prefix
, const TypeNode
& type
,
564 const std::string
& comment
= "", int flags
= SKOLEM_DEFAULT
);
566 /** Create a instantiation constant with the given type. */
567 Node
mkInstConstant(const TypeNode
& type
);
569 /** Create a boolean term variable. */
570 Node
mkBooleanTermVariable();
572 /** Make a new abstract value with the given type. */
573 Node
mkAbstractValue(const TypeNode
& type
);
575 /** make unique (per Type,Kind) variable. */
576 Node
mkNullaryOperator(const TypeNode
& type
, Kind k
);
579 * Create a singleton set from the given element n.
580 * @param t the element type of the returned set.
581 * Note that the type of n needs to be a subtype of t.
582 * @param n the single element in the singleton.
583 * @return a singleton set constructed from the element n.
585 Node
mkSingleton(const TypeNode
& t
, const TNode n
);
588 * Create a bag from the given element n along with its multiplicity m.
589 * @param t the element type of the returned bag.
590 * Note that the type of n needs to be a subtype of t.
591 * @param n the element that is used to to construct the bag
592 * @param m the multiplicity of the element n
593 * @return a bag that contains m occurrences of n.
595 Node
mkBag(const TypeNode
& t
, const TNode n
, const TNode m
);
598 * Create a constant of type T. It will have the appropriate
599 * CONST_* kind defined for T.
602 Node
mkConst(const T
&);
605 TypeNode
mkTypeConst(const T
&);
607 template <class NodeClass
, class T
>
608 NodeClass
mkConstInternal(const T
&);
610 /** Create a node with children. */
611 TypeNode
mkTypeNode(Kind kind
, TypeNode child1
);
612 TypeNode
mkTypeNode(Kind kind
, TypeNode child1
, TypeNode child2
);
613 TypeNode
mkTypeNode(Kind kind
, TypeNode child1
, TypeNode child2
,
615 TypeNode
mkTypeNode(Kind kind
, const std::vector
<TypeNode
>& children
);
618 * Determine whether Nodes of a particular Kind have operators.
619 * @returns true if Nodes of Kind k have operators.
621 static inline bool hasOperator(Kind k
);
624 * Get the (singleton) operator of an OPERATOR-kinded kind. The
625 * returned node n will have kind BUILTIN, and calling
626 * n.getConst<CVC4::Kind>() will yield k.
628 inline TNode
operatorOf(Kind k
) {
629 AssertArgument( kind::metaKindOf(k
) == kind::metakind::OPERATOR
, k
,
630 "Kind is not an OPERATOR-kinded kind "
631 "in NodeManager::operatorOf()" );
632 return d_operators
[k
];
636 * Retrieve an attribute for a node.
638 * @param nv the node value
639 * @param attr an instance of the attribute kind to retrieve.
640 * @returns the attribute, if set, or a default-constructed
641 * <code>AttrKind::value_type</code> if not.
643 template <class AttrKind
>
644 inline typename
AttrKind::value_type
getAttribute(expr::NodeValue
* nv
,
645 const AttrKind
& attr
) const;
648 * Check whether an attribute is set for a node.
650 * @param nv the node value
651 * @param attr an instance of the attribute kind to check
652 * @returns <code>true</code> iff <code>attr</code> is set for
655 template <class AttrKind
>
656 inline bool hasAttribute(expr::NodeValue
* nv
,
657 const AttrKind
& attr
) const;
660 * Check whether an attribute is set for a node, and, if so,
663 * @param nv the node value
664 * @param attr an instance of the attribute kind to check
665 * @param value a reference to an object of the attribute's value type.
666 * <code>value</code> will be set to the value of the attribute, if it is
667 * set for <code>nv</code>; otherwise, it will be set to the default
668 * value of the attribute.
669 * @returns <code>true</code> iff <code>attr</code> is set for
672 template <class AttrKind
>
673 inline bool getAttribute(expr::NodeValue
* nv
,
674 const AttrKind
& attr
,
675 typename
AttrKind::value_type
& value
) const;
678 * Set an attribute for a node. If the node doesn't have the
679 * attribute, this function assigns one. If the node has one, this
682 * @param nv the node value
683 * @param attr an instance of the attribute kind to set
684 * @param value the value of <code>attr</code> for <code>nv</code>
686 template <class AttrKind
>
687 inline void setAttribute(expr::NodeValue
* nv
,
688 const AttrKind
& attr
,
689 const typename
AttrKind::value_type
& value
);
692 * Retrieve an attribute for a TNode.
695 * @param attr an instance of the attribute kind to retrieve.
696 * @returns the attribute, if set, or a default-constructed
697 * <code>AttrKind::value_type</code> if not.
699 template <class AttrKind
>
700 inline typename
AttrKind::value_type
701 getAttribute(TNode n
, const AttrKind
& attr
) const;
704 * Check whether an attribute is set for a TNode.
707 * @param attr an instance of the attribute kind to check
708 * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
710 template <class AttrKind
>
711 inline bool hasAttribute(TNode n
,
712 const AttrKind
& attr
) const;
715 * Check whether an attribute is set for a TNode and, if so, retieve
719 * @param attr an instance of the attribute kind to check
720 * @param value a reference to an object of the attribute's value type.
721 * <code>value</code> will be set to the value of the attribute, if it is
722 * set for <code>nv</code>; otherwise, it will be set to the default value of
724 * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
726 template <class AttrKind
>
727 inline bool getAttribute(TNode n
,
728 const AttrKind
& attr
,
729 typename
AttrKind::value_type
& value
) const;
732 * Set an attribute for a node. If the node doesn't have the
733 * attribute, this function assigns one. If the node has one, this
737 * @param attr an instance of the attribute kind to set
738 * @param value the value of <code>attr</code> for <code>n</code>
740 template <class AttrKind
>
741 inline void setAttribute(TNode n
,
742 const AttrKind
& attr
,
743 const typename
AttrKind::value_type
& value
);
746 * Retrieve an attribute for a TypeNode.
748 * @param n the type node
749 * @param attr an instance of the attribute kind to retrieve.
750 * @returns the attribute, if set, or a default-constructed
751 * <code>AttrKind::value_type</code> if not.
753 template <class AttrKind
>
754 inline typename
AttrKind::value_type
755 getAttribute(TypeNode n
, const AttrKind
& attr
) const;
758 * Check whether an attribute is set for a TypeNode.
760 * @param n the type node
761 * @param attr an instance of the attribute kind to check
762 * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
764 template <class AttrKind
>
765 inline bool hasAttribute(TypeNode n
,
766 const AttrKind
& attr
) const;
769 * Check whether an attribute is set for a TypeNode and, if so, retieve
772 * @param n the type node
773 * @param attr an instance of the attribute kind to check
774 * @param value a reference to an object of the attribute's value type.
775 * <code>value</code> will be set to the value of the attribute, if it is
776 * set for <code>nv</code>; otherwise, it will be set to the default value of
778 * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
780 template <class AttrKind
>
781 inline bool getAttribute(TypeNode n
,
782 const AttrKind
& attr
,
783 typename
AttrKind::value_type
& value
) const;
786 * Set an attribute for a type node. If the node doesn't have the
787 * attribute, this function assigns one. If the type node has one,
788 * this overwrites it.
790 * @param n the type node
791 * @param attr an instance of the attribute kind to set
792 * @param value the value of <code>attr</code> for <code>n</code>
794 template <class AttrKind
>
795 inline void setAttribute(TypeNode n
,
796 const AttrKind
& attr
,
797 const typename
AttrKind::value_type
& value
);
799 /** Get the (singleton) type for Booleans. */
800 inline TypeNode
booleanType();
802 /** Get the (singleton) type for integers. */
803 inline TypeNode
integerType();
805 /** Get the (singleton) type for reals. */
806 inline TypeNode
realType();
808 /** Get the (singleton) type for strings. */
809 inline TypeNode
stringType();
811 /** Get the (singleton) type for RegExp. */
812 inline TypeNode
regExpType();
814 /** Get the (singleton) type for rounding modes. */
815 inline TypeNode
roundingModeType();
817 /** Get the bound var list type. */
818 inline TypeNode
boundVarListType();
820 /** Get the instantiation pattern type. */
821 inline TypeNode
instPatternType();
823 /** Get the instantiation pattern type. */
824 inline TypeNode
instPatternListType();
827 * Get the (singleton) type for builtin operators (that is, the type
828 * of the Node returned from Node::getOperator() when the operator
829 * is built-in, like EQUAL). */
830 inline TypeNode
builtinOperatorType();
833 * Make a function type from domain to range.
835 * @param domain the domain type
836 * @param range the range type
837 * @returns the functional type domain -> range
839 TypeNode
mkFunctionType(const TypeNode
& domain
, const TypeNode
& range
);
842 * Make a function type with input types from
843 * argTypes. <code>argTypes</code> must have at least one element.
845 * @param argTypes the domain is a tuple (argTypes[0], ..., argTypes[n])
846 * @param range the range type
847 * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range
849 TypeNode
mkFunctionType(const std::vector
<TypeNode
>& argTypes
,
850 const TypeNode
& range
);
853 * Make a function type with input types from
854 * <code>sorts[0..sorts.size()-2]</code> and result type
855 * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
856 * at least 2 elements.
858 TypeNode
mkFunctionType(const std::vector
<TypeNode
>& sorts
);
861 * Make a predicate type with input types from
862 * <code>sorts</code>. The result with be a function type with range
863 * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
866 TypeNode
mkPredicateType(const std::vector
<TypeNode
>& sorts
);
869 * Make a tuple type with types from
870 * <code>types</code>. <code>types</code> must have at least one
873 * @param types a vector of types
874 * @returns the tuple type (types[0], ..., types[n])
876 TypeNode
mkTupleType(const std::vector
<TypeNode
>& types
);
879 * Make a record type with the description from rec.
881 * @param rec a description of the record
882 * @returns the record type
884 TypeNode
mkRecordType(const Record
& rec
);
887 * Make a symbolic expression type with types from
888 * <code>types</code>. <code>types</code> may have any number of
891 * @param types a vector of types
892 * @returns the symbolic expression type (types[0], ..., types[n])
894 inline TypeNode
mkSExprType(const std::vector
<TypeNode
>& types
);
896 /** Make the type of floating-point with <code>exp</code> bit exponent and
897 <code>sig</code> bit significand */
898 inline TypeNode
mkFloatingPointType(unsigned exp
, unsigned sig
);
899 inline TypeNode
mkFloatingPointType(FloatingPointSize fs
);
901 /** Make the type of bitvectors of size <code>size</code> */
902 inline TypeNode
mkBitVectorType(unsigned size
);
904 /** Make the type of arrays with the given parameterization */
905 inline TypeNode
mkArrayType(TypeNode indexType
, TypeNode constituentType
);
907 /** Make the type of set with the given parameterization */
908 inline TypeNode
mkSetType(TypeNode elementType
);
910 /** Make the type of bags with the given parameterization */
911 TypeNode
mkBagType(TypeNode elementType
);
913 /** Make the type of sequences with the given parameterization */
914 TypeNode
mkSequenceType(TypeNode elementType
);
916 /** Bits for use in mkDatatypeType() flags.
918 * DATATYPE_FLAG_PLACEHOLDER indicates that the type should not be printed
919 * out as a definition, for example, in models or during dumping.
923 DATATYPE_FLAG_NONE
= 0,
924 DATATYPE_FLAG_PLACEHOLDER
= 1
927 /** Make a type representing the given datatype. */
928 TypeNode
mkDatatypeType(DType
& datatype
, uint32_t flags
= DATATYPE_FLAG_NONE
);
931 * Make a set of types representing the given datatypes, which may be
932 * mutually recursive.
934 std::vector
<TypeNode
> mkMutualDatatypeTypes(
935 const std::vector
<DType
>& datatypes
, uint32_t flags
= DATATYPE_FLAG_NONE
);
938 * Make a set of types representing the given datatypes, which may
939 * be mutually recursive. unresolvedTypes is a set of SortTypes
940 * that were used as placeholders in the Datatypes for the Datatypes
941 * of the same name. This is just a more complicated version of the
942 * above mkMutualDatatypeTypes() function, but is required to handle
945 * For example, unresolvedTypes might contain the single sort "list"
946 * (with that name reported from SortType::getName()). The
947 * datatypes list might have the single datatype
950 * list = cons(car:ARRAY INT OF list, cdr:list) | nil;
953 * To represent the Type of the array, the user had to create a
954 * placeholder type (an uninterpreted sort) to stand for "list" in
955 * the type of "car". It is this placeholder sort that should be
956 * passed in unresolvedTypes. If the datatype was of the simpler
960 * list = cons(car:list, cdr:list) | nil;
963 * then no complicated Type needs to be created, and the above,
964 * simpler form of mkMutualDatatypeTypes() is enough.
966 std::vector
<TypeNode
> mkMutualDatatypeTypes(
967 const std::vector
<DType
>& datatypes
,
968 const std::set
<TypeNode
>& unresolvedTypes
,
969 uint32_t flags
= DATATYPE_FLAG_NONE
);
972 * Make a type representing a constructor with the given argument (subfield)
973 * types and return type range.
975 TypeNode
mkConstructorType(const std::vector
<TypeNode
>& args
, TypeNode range
);
977 /** Make a type representing a selector with the given parameterization */
978 inline TypeNode
mkSelectorType(TypeNode domain
, TypeNode range
);
980 /** Make a type representing a tester with given parameterization */
981 inline TypeNode
mkTesterType(TypeNode domain
);
983 /** Make a new (anonymous) sort of arity 0. */
984 TypeNode
mkSort(uint32_t flags
= ExprManager::SORT_FLAG_NONE
);
986 /** Make a new sort with the given name of arity 0. */
987 TypeNode
mkSort(const std::string
& name
, uint32_t flags
= ExprManager::SORT_FLAG_NONE
);
989 /** Make a new sort by parameterizing the given sort constructor. */
990 TypeNode
mkSort(TypeNode constructor
,
991 const std::vector
<TypeNode
>& children
,
992 uint32_t flags
= ExprManager::SORT_FLAG_NONE
);
994 /** Make a new sort with the given name and arity. */
995 TypeNode
mkSortConstructor(const std::string
& name
,
997 uint32_t flags
= ExprManager::SORT_FLAG_NONE
);
1000 * Get the type for the given node and optionally do type checking.
1002 * Initial type computation will be near-constant time if
1003 * type checking is not requested. Results are memoized, so that
1004 * subsequent calls to getType() without type checking will be
1007 * Initial type checking is linear in the size of the expression.
1008 * Again, the results are memoized, so that subsequent calls to
1009 * getType(), with or without type checking, will be constant
1012 * NOTE: A TypeCheckingException can be thrown even when type
1013 * checking is not requested. getType() will always return a
1014 * valid and correct type and, thus, an exception will be thrown
1015 * when no valid or correct type can be computed (e.g., if the
1016 * arguments to a bit-vector operation aren't bit-vectors). When
1017 * type checking is not requested, getType() will do the minimum
1018 * amount of checking required to return a valid result.
1020 * @param n the Node for which we want a type
1021 * @param check whether we should check the type as we compute it
1024 TypeNode
getType(TNode n
, bool check
= false);
1027 * Convert a node to an expression. Uses the ExprManager
1028 * associated to this NodeManager.
1030 inline Expr
toExpr(TNode n
);
1033 * Convert an expression to a node.
1035 static inline Node
fromExpr(const Expr
& e
);
1038 * Convert a node manager to an expression manager.
1040 inline ExprManager
* toExprManager();
1043 * Convert an expression manager to a node manager.
1045 static inline NodeManager
* fromExprManager(ExprManager
* exprManager
);
1048 * Convert a type node to a type.
1050 inline Type
toType(const TypeNode
& tn
);
1053 * Convert a type to a type node.
1055 static inline TypeNode
fromType(Type t
);
1057 /** Reclaim zombies while there are more than k nodes in the pool (if possible).*/
1058 void reclaimZombiesUntil(uint32_t k
);
1060 /** Reclaims all zombies (if possible).*/
1061 void reclaimAllZombies();
1063 /** Size of the node pool. */
1064 size_t poolSize() const;
1066 /** Deletes a list of attributes from the NM's AttributeManager.*/
1067 void deleteAttributes(const std::vector
< const expr::attr::AttributeUniqueId
* >& ids
);
1070 * This function gives developers a hook into the NodeManager.
1071 * This can be changed in node_manager.cpp without recompiling most of cvc4.
1073 * debugHook is a debugging only function, and should not be present in
1074 * any published code!
1076 void debugHook(int debugFlag
);
1077 };/* class NodeManager */
1080 * This class changes the "current" thread-global
1081 * <code>NodeManager</code> when it is created and reinstates the
1082 * previous thread-global <code>NodeManager</code> when it is
1083 * destroyed, effectively maintaining a set of nested
1084 * <code>NodeManager</code> scopes. This is especially useful on
1085 * public-interface calls into the CVC4 library, where CVC4's notion
1086 * of the "current" <code>NodeManager</code> should be set to match
1087 * the calling context. See, for example, the implementations of
1088 * public calls in the <code>ExprManager</code> and
1089 * <code>SmtEngine</code> classes.
1091 * The client must be careful to create and destroy
1092 * <code>NodeManagerScope</code> objects in a well-nested manner (such
1093 * as on the stack). You may create a <code>NodeManagerScope</code>
1094 * with <code>new</code> and destroy it with <code>delete</code>, or
1095 * place it as a data member of an object that is, but if the scope of
1096 * these <code>new</code>/<code>delete</code> pairs isn't properly
1097 * maintained, the incorrect "current" <code>NodeManager</code>
1098 * pointer may be restored after a delete.
1100 class NodeManagerScope
{
1101 /** The old NodeManager, to be restored on destruction. */
1102 NodeManager
* d_oldNodeManager
;
1104 NodeManagerScope(NodeManager
* nm
) : d_oldNodeManager(NodeManager::s_current
)
1106 // There are corner cases where nm can be NULL and it's ok.
1107 // For example, if you write { Expr e; }, then when the null
1108 // Expr is destructed, there's no active node manager.
1109 // Assert(nm != NULL);
1110 NodeManager::s_current
= nm
;
1111 Debug("current") << "node manager scope: " << NodeManager::s_current
<< "\n";
1114 ~NodeManagerScope() {
1115 NodeManager::s_current
= d_oldNodeManager
;
1116 Debug("current") << "node manager scope: "
1117 << "returning to " << NodeManager::s_current
<< "\n";
1119 };/* class NodeManagerScope */
1121 /** Get the (singleton) type for booleans. */
1122 inline TypeNode
NodeManager::booleanType() {
1123 return TypeNode(mkTypeConst
<TypeConstant
>(BOOLEAN_TYPE
));
1126 /** Get the (singleton) type for integers. */
1127 inline TypeNode
NodeManager::integerType() {
1128 return TypeNode(mkTypeConst
<TypeConstant
>(INTEGER_TYPE
));
1131 /** Get the (singleton) type for reals. */
1132 inline TypeNode
NodeManager::realType() {
1133 return TypeNode(mkTypeConst
<TypeConstant
>(REAL_TYPE
));
1136 /** Get the (singleton) type for strings. */
1137 inline TypeNode
NodeManager::stringType() {
1138 return TypeNode(mkTypeConst
<TypeConstant
>(STRING_TYPE
));
1141 /** Get the (singleton) type for regexps. */
1142 inline TypeNode
NodeManager::regExpType() {
1143 return TypeNode(mkTypeConst
<TypeConstant
>(REGEXP_TYPE
));
1146 /** Get the (singleton) type for rounding modes. */
1147 inline TypeNode
NodeManager::roundingModeType() {
1148 return TypeNode(mkTypeConst
<TypeConstant
>(ROUNDINGMODE_TYPE
));
1151 /** Get the bound var list type. */
1152 inline TypeNode
NodeManager::boundVarListType() {
1153 return TypeNode(mkTypeConst
<TypeConstant
>(BOUND_VAR_LIST_TYPE
));
1156 /** Get the instantiation pattern type. */
1157 inline TypeNode
NodeManager::instPatternType() {
1158 return TypeNode(mkTypeConst
<TypeConstant
>(INST_PATTERN_TYPE
));
1161 /** Get the instantiation pattern type. */
1162 inline TypeNode
NodeManager::instPatternListType() {
1163 return TypeNode(mkTypeConst
<TypeConstant
>(INST_PATTERN_LIST_TYPE
));
1166 /** Get the (singleton) type for builtin operators. */
1167 inline TypeNode
NodeManager::builtinOperatorType() {
1168 return TypeNode(mkTypeConst
<TypeConstant
>(BUILTIN_OPERATOR_TYPE
));
1171 inline TypeNode
NodeManager::mkSExprType(const std::vector
<TypeNode
>& types
) {
1172 std::vector
<TypeNode
> typeNodes
;
1173 for (unsigned i
= 0; i
< types
.size(); ++ i
) {
1174 typeNodes
.push_back(types
[i
]);
1176 return mkTypeNode(kind::SEXPR_TYPE
, typeNodes
);
1179 inline TypeNode
NodeManager::mkBitVectorType(unsigned size
) {
1180 return TypeNode(mkTypeConst
<BitVectorSize
>(BitVectorSize(size
)));
1183 inline TypeNode
NodeManager::mkFloatingPointType(unsigned exp
, unsigned sig
) {
1184 return TypeNode(mkTypeConst
<FloatingPointSize
>(FloatingPointSize(exp
,sig
)));
1187 inline TypeNode
NodeManager::mkFloatingPointType(FloatingPointSize fs
) {
1188 return TypeNode(mkTypeConst
<FloatingPointSize
>(fs
));
1191 inline TypeNode
NodeManager::mkArrayType(TypeNode indexType
,
1192 TypeNode constituentType
) {
1193 CheckArgument(!indexType
.isNull(), indexType
,
1194 "unexpected NULL index type");
1195 CheckArgument(!constituentType
.isNull(), constituentType
,
1196 "unexpected NULL constituent type");
1197 CheckArgument(indexType
.isFirstClass(),
1199 "cannot index arrays by types that are not first-class. Try "
1201 CheckArgument(constituentType
.isFirstClass(),
1203 "cannot store types that are not first-class in arrays. Try "
1205 Debug("arrays") << "making array type " << indexType
<< " "
1206 << constituentType
<< std::endl
;
1207 return mkTypeNode(kind::ARRAY_TYPE
, indexType
, constituentType
);
1210 inline TypeNode
NodeManager::mkSetType(TypeNode elementType
) {
1211 CheckArgument(!elementType
.isNull(), elementType
,
1212 "unexpected NULL element type");
1213 CheckArgument(elementType
.isFirstClass(),
1215 "cannot store types that are not first-class in sets. Try "
1217 Debug("sets") << "making sets type " << elementType
<< std::endl
;
1218 return mkTypeNode(kind::SET_TYPE
, elementType
);
1221 inline TypeNode
NodeManager::mkSelectorType(TypeNode domain
, TypeNode range
) {
1222 CheckArgument(domain
.isDatatype(), domain
,
1223 "cannot create non-datatype selector type");
1224 CheckArgument(range
.isFirstClass(),
1226 "cannot have selector fields that are not first-class types. "
1227 "Try option --uf-ho.");
1228 return mkTypeNode(kind::SELECTOR_TYPE
, domain
, range
);
1231 inline TypeNode
NodeManager::mkTesterType(TypeNode domain
) {
1232 CheckArgument(domain
.isDatatype(), domain
,
1233 "cannot create non-datatype tester");
1234 return mkTypeNode(kind::TESTER_TYPE
, domain
);
1237 inline expr::NodeValue
* NodeManager::poolLookup(expr::NodeValue
* nv
) const {
1238 NodeValuePool::const_iterator find
= d_nodeValuePool
.find(nv
);
1239 if(find
== d_nodeValuePool
.end()) {
1246 inline void NodeManager::poolInsert(expr::NodeValue
* nv
) {
1247 Assert(d_nodeValuePool
.find(nv
) == d_nodeValuePool
.end())
1248 << "NodeValue already in the pool!";
1249 d_nodeValuePool
.insert(nv
);// FIXME multithreading
1252 inline void NodeManager::poolRemove(expr::NodeValue
* nv
) {
1253 Assert(d_nodeValuePool
.find(nv
) != d_nodeValuePool
.end())
1254 << "NodeValue is not in the pool!";
1256 d_nodeValuePool
.erase(nv
);// FIXME multithreading
1259 inline Expr
NodeManager::toExpr(TNode n
) {
1260 return Expr(d_exprManager
, new Node(n
));
1263 inline Node
NodeManager::fromExpr(const Expr
& e
) {
1267 inline ExprManager
* NodeManager::toExprManager() {
1268 return d_exprManager
;
1271 inline NodeManager
* NodeManager::fromExprManager(ExprManager
* exprManager
) {
1272 return exprManager
->getNodeManager();
1275 inline Type
NodeManager::toType(const TypeNode
& tn
)
1277 return Type(this, new TypeNode(tn
));
1280 inline TypeNode
NodeManager::fromType(Type t
) {
1281 return *Type::getTypeNode(t
);
1284 }/* CVC4 namespace */
1286 #define CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
1287 #include "expr/metakind.h"
1288 #undef CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
1290 #include "expr/node_builder.h"
1294 // general expression-builders
1296 inline bool NodeManager::hasOperator(Kind k
) {
1297 switch(kind::MetaKind mk
= kind::metaKindOf(k
)) {
1299 case kind::metakind::INVALID
:
1300 case kind::metakind::VARIABLE
:
1301 case kind::metakind::NULLARY_OPERATOR
:
1304 case kind::metakind::OPERATOR
:
1305 case kind::metakind::PARAMETERIZED
:
1308 case kind::metakind::CONSTANT
:
1311 default: Unhandled() << mk
;
1315 inline Kind
NodeManager::operatorToKind(TNode n
) {
1316 return kind::operatorToKind(n
.d_nv
);
1319 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
) {
1320 NodeBuilder
<1> nb(this, kind
);
1322 return nb
.constructNode();
1325 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
) {
1326 NodeBuilder
<1> nb(this, kind
);
1328 return nb
.constructNodePtr();
1331 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
, TNode child2
) {
1332 NodeBuilder
<2> nb(this, kind
);
1333 nb
<< child1
<< child2
;
1334 return nb
.constructNode();
1337 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
, TNode child2
) {
1338 NodeBuilder
<2> nb(this, kind
);
1339 nb
<< child1
<< child2
;
1340 return nb
.constructNodePtr();
1343 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
, TNode child2
,
1345 NodeBuilder
<3> nb(this, kind
);
1346 nb
<< child1
<< child2
<< child3
;
1347 return nb
.constructNode();
1350 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
, TNode child2
,
1352 NodeBuilder
<3> nb(this, kind
);
1353 nb
<< child1
<< child2
<< child3
;
1354 return nb
.constructNodePtr();
1357 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
, TNode child2
,
1358 TNode child3
, TNode child4
) {
1359 NodeBuilder
<4> nb(this, kind
);
1360 nb
<< child1
<< child2
<< child3
<< child4
;
1361 return nb
.constructNode();
1364 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
, TNode child2
,
1365 TNode child3
, TNode child4
) {
1366 NodeBuilder
<4> nb(this, kind
);
1367 nb
<< child1
<< child2
<< child3
<< child4
;
1368 return nb
.constructNodePtr();
1371 inline Node
NodeManager::mkNode(Kind kind
, TNode child1
, TNode child2
,
1372 TNode child3
, TNode child4
, TNode child5
) {
1373 NodeBuilder
<5> nb(this, kind
);
1374 nb
<< child1
<< child2
<< child3
<< child4
<< child5
;
1375 return nb
.constructNode();
1378 inline Node
* NodeManager::mkNodePtr(Kind kind
, TNode child1
, TNode child2
,
1379 TNode child3
, TNode child4
, TNode child5
) {
1380 NodeBuilder
<5> nb(this, kind
);
1381 nb
<< child1
<< child2
<< child3
<< child4
<< child5
;
1382 return nb
.constructNodePtr();
1386 template <bool ref_count
>
1387 inline Node
NodeManager::mkNode(Kind kind
,
1388 const std::vector
<NodeTemplate
<ref_count
> >&
1390 NodeBuilder
<> nb(this, kind
);
1391 nb
.append(children
);
1392 return nb
.constructNode();
1395 template <bool ref_count
>
1396 Node
NodeManager::mkAnd(const std::vector
<NodeTemplate
<ref_count
> >& children
)
1398 if (children
.empty())
1400 return mkConst(true);
1402 else if (children
.size() == 1)
1406 return mkNode(kind::AND
, children
);
1409 template <bool ref_count
>
1410 inline Node
* NodeManager::mkNodePtr(Kind kind
,
1411 const std::vector
<NodeTemplate
<ref_count
> >&
1413 NodeBuilder
<> nb(this, kind
);
1414 nb
.append(children
);
1415 return nb
.constructNodePtr();
1419 inline Node
NodeManager::mkNode(TNode opNode
) {
1420 NodeBuilder
<1> nb(this, operatorToKind(opNode
));
1421 if(opNode
.getKind() != kind::BUILTIN
) {
1424 return nb
.constructNode();
1427 inline Node
* NodeManager::mkNodePtr(TNode opNode
) {
1428 NodeBuilder
<1> nb(this, operatorToKind(opNode
));
1429 if(opNode
.getKind() != kind::BUILTIN
) {
1432 return nb
.constructNodePtr();
1435 inline Node
NodeManager::mkNode(TNode opNode
, TNode child1
) {
1436 NodeBuilder
<2> nb(this, operatorToKind(opNode
));
1437 if(opNode
.getKind() != kind::BUILTIN
) {
1441 return nb
.constructNode();
1444 inline Node
* NodeManager::mkNodePtr(TNode opNode
, TNode child1
) {
1445 NodeBuilder
<2> nb(this, operatorToKind(opNode
));
1446 if(opNode
.getKind() != kind::BUILTIN
) {
1450 return nb
.constructNodePtr();
1453 inline Node
NodeManager::mkNode(TNode opNode
, TNode child1
, TNode child2
) {
1454 NodeBuilder
<3> nb(this, operatorToKind(opNode
));
1455 if(opNode
.getKind() != kind::BUILTIN
) {
1458 nb
<< child1
<< child2
;
1459 return nb
.constructNode();
1462 inline Node
* NodeManager::mkNodePtr(TNode opNode
, TNode child1
, TNode child2
) {
1463 NodeBuilder
<3> nb(this, operatorToKind(opNode
));
1464 if(opNode
.getKind() != kind::BUILTIN
) {
1467 nb
<< child1
<< child2
;
1468 return nb
.constructNodePtr();
1471 inline Node
NodeManager::mkNode(TNode opNode
, TNode child1
, TNode child2
,
1473 NodeBuilder
<4> nb(this, operatorToKind(opNode
));
1474 if(opNode
.getKind() != kind::BUILTIN
) {
1477 nb
<< child1
<< child2
<< child3
;
1478 return nb
.constructNode();
1481 inline Node
* NodeManager::mkNodePtr(TNode opNode
, TNode child1
, TNode child2
,
1483 NodeBuilder
<4> nb(this, operatorToKind(opNode
));
1484 if(opNode
.getKind() != kind::BUILTIN
) {
1487 nb
<< child1
<< child2
<< child3
;
1488 return nb
.constructNodePtr();
1491 inline Node
NodeManager::mkNode(TNode opNode
, TNode child1
, TNode child2
,
1492 TNode child3
, TNode child4
) {
1493 NodeBuilder
<5> nb(this, operatorToKind(opNode
));
1494 if(opNode
.getKind() != kind::BUILTIN
) {
1497 nb
<< child1
<< child2
<< child3
<< child4
;
1498 return nb
.constructNode();
1501 inline Node
* NodeManager::mkNodePtr(TNode opNode
, TNode child1
, TNode child2
,
1502 TNode child3
, TNode child4
) {
1503 NodeBuilder
<5> nb(this, operatorToKind(opNode
));
1504 if(opNode
.getKind() != kind::BUILTIN
) {
1507 nb
<< child1
<< child2
<< child3
<< child4
;
1508 return nb
.constructNodePtr();
1511 inline Node
NodeManager::mkNode(TNode opNode
, TNode child1
, TNode child2
,
1512 TNode child3
, TNode child4
, TNode child5
) {
1513 NodeBuilder
<6> nb(this, operatorToKind(opNode
));
1514 if(opNode
.getKind() != kind::BUILTIN
) {
1517 nb
<< child1
<< child2
<< child3
<< child4
<< child5
;
1518 return nb
.constructNode();
1521 inline Node
* NodeManager::mkNodePtr(TNode opNode
, TNode child1
, TNode child2
,
1522 TNode child3
, TNode child4
, TNode child5
) {
1523 NodeBuilder
<6> nb(this, operatorToKind(opNode
));
1524 if(opNode
.getKind() != kind::BUILTIN
) {
1527 nb
<< child1
<< child2
<< child3
<< child4
<< child5
;
1528 return nb
.constructNodePtr();
1531 // N-ary version for operators
1532 template <bool ref_count
>
1533 inline Node
NodeManager::mkNode(TNode opNode
,
1534 const std::vector
<NodeTemplate
<ref_count
> >&
1536 NodeBuilder
<> nb(this, operatorToKind(opNode
));
1537 if(opNode
.getKind() != kind::BUILTIN
) {
1540 nb
.append(children
);
1541 return nb
.constructNode();
1544 template <bool ref_count
>
1545 inline Node
* NodeManager::mkNodePtr(TNode opNode
,
1546 const std::vector
<NodeTemplate
<ref_count
> >&
1548 NodeBuilder
<> nb(this, operatorToKind(opNode
));
1549 if(opNode
.getKind() != kind::BUILTIN
) {
1552 nb
.append(children
);
1553 return nb
.constructNodePtr();
1557 inline TypeNode
NodeManager::mkTypeNode(Kind kind
, TypeNode child1
) {
1558 return (NodeBuilder
<1>(this, kind
) << child1
).constructTypeNode();
1561 inline TypeNode
NodeManager::mkTypeNode(Kind kind
, TypeNode child1
,
1563 return (NodeBuilder
<2>(this, kind
) << child1
<< child2
).constructTypeNode();
1566 inline TypeNode
NodeManager::mkTypeNode(Kind kind
, TypeNode child1
,
1567 TypeNode child2
, TypeNode child3
) {
1568 return (NodeBuilder
<3>(this, kind
) << child1
<< child2
<< child3
).constructTypeNode();
1571 // N-ary version for types
1572 inline TypeNode
NodeManager::mkTypeNode(Kind kind
,
1573 const std::vector
<TypeNode
>& children
) {
1574 return NodeBuilder
<>(this, kind
).append(children
).constructTypeNode();
1578 Node
NodeManager::mkConst(const T
& val
) {
1579 return mkConstInternal
<Node
, T
>(val
);
1583 TypeNode
NodeManager::mkTypeConst(const T
& val
) {
1584 return mkConstInternal
<TypeNode
, T
>(val
);
1587 template <class NodeClass
, class T
>
1588 NodeClass
NodeManager::mkConstInternal(const T
& val
) {
1589 // This method indirectly calls `NodeValue::inc()`, which relies on having
1590 // the correct `NodeManager` in scope.
1591 NodeManagerScope
nms(this);
1593 // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
1594 NVStorage
<1> nvStorage
;
1595 expr::NodeValue
& nvStack
= reinterpret_cast<expr::NodeValue
&>(nvStorage
);
1598 nvStack
.d_kind
= kind::metakind::ConstantMap
<T
>::kind
;
1600 nvStack
.d_nchildren
= 1;
1602 #if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6))
1603 #pragma GCC diagnostic push
1604 #pragma GCC diagnostic ignored "-Warray-bounds"
1607 nvStack
.d_children
[0] =
1608 const_cast<expr::NodeValue
*>(reinterpret_cast<const expr::NodeValue
*>(&val
));
1609 expr::NodeValue
* nv
= poolLookup(&nvStack
);
1611 #if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6))
1612 #pragma GCC diagnostic pop
1616 return NodeClass(nv
);
1619 nv
= (expr::NodeValue
*)
1620 std::malloc(sizeof(expr::NodeValue
) + sizeof(T
));
1622 throw std::bad_alloc();
1625 nv
->d_nchildren
= 0;
1626 nv
->d_kind
= kind::metakind::ConstantMap
<T
>::kind
;
1627 nv
->d_id
= next_id
++;// FIXME multithreading
1630 //OwningTheory::mkConst(val);
1631 new (&nv
->d_children
) T(val
);
1634 if(Debug
.isOn("gc")) {
1635 Debug("gc") << "creating node value " << nv
1636 << " [" << nv
->d_id
<< "]: ";
1637 nv
->printAst(Debug("gc"));
1638 Debug("gc") << std::endl
;
1641 return NodeClass(nv
);
1644 }/* CVC4 namespace */
1646 #endif /* CVC4__NODE_MANAGER_H */