1 /********************* */
4 ** Original author: Morgan Deters
5 ** Major contributors: Tim King
6 ** Minor contributors (to current version): Christopher L. Conway, Dejan Jovanovic
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Node attributes.
17 #include "cvc4_private.h"
19 /* There are strong constraints on ordering of declarations of
20 * attributes and nodes due to template use */
21 #include "expr/node.h"
22 #include "expr/type_node.h"
23 #include "context/context.h"
25 #ifndef __CVC4__EXPR__ATTRIBUTE_H
26 #define __CVC4__EXPR__ATTRIBUTE_H
30 #include "expr/attribute_unique_id.h"
32 // include supporting templates
33 #define CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
34 #include "expr/attribute_internals.h"
35 #undef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
42 extern CVC4_THREADLOCAL(SmtEngine
*) s_smtEngine_current
;
43 }/* CVC4::smt namespace */
48 // ATTRIBUTE MANAGER ===========================================================
50 struct SmtAttributes
{
51 SmtAttributes(context::Context
*);
53 // IF YOU ADD ANY TABLES, don't forget to add them also to the
54 // implementation of deleteAllAttributes().
56 /** Underlying hash table for context-dependent boolean-valued attributes */
57 CDAttrHash
<bool> d_cdbools
;
58 /** Underlying hash table for context-dependent integral-valued attributes */
59 CDAttrHash
<uint64_t> d_cdints
;
60 /** Underlying hash table for context-dependent node-valued attributes */
61 CDAttrHash
<TNode
> d_cdtnodes
;
62 /** Underlying hash table for context-dependent node-valued attributes */
63 CDAttrHash
<Node
> d_cdnodes
;
64 /** Underlying hash table for context-dependent string-valued attributes */
65 CDAttrHash
<std::string
> d_cdstrings
;
66 /** Underlying hash table for context-dependent pointer-valued attributes */
67 CDAttrHash
<void*> d_cdptrs
;
69 /** Delete all attributes of given node */
70 void deleteAllAttributes(TNode n
);
73 void deleteFromTable(CDAttrHash
<T
>& table
, NodeValue
* nv
);
75 };/* struct SmtAttributes */
78 * A container for the main attribute tables of the system. There's a
79 * one-to-one NodeManager : AttributeManager correspondence.
81 class AttributeManager
{
84 void deleteFromTable(AttrHash
<T
>& table
, NodeValue
* nv
);
87 void deleteAllFromTable(AttrHash
<T
>& table
);
90 void deleteAttributesFromTable(AttrHash
<T
>& table
, const std::vector
<uint64_t>& ids
);
93 void reconstructTable(AttrHash
<T
>& table
);
96 * getTable<> is a helper template that gets the right table from an
97 * AttributeManager given its type.
99 template <class T
, bool context_dep
>
100 friend struct getTable
;
102 bool d_inGarbageCollection
;
104 void clearDeleteAllAttributesBuffer();
106 SmtAttributes
& getSmtAttributes(SmtEngine
*);
107 const SmtAttributes
& getSmtAttributes(SmtEngine
*) const;
111 /** Construct an attribute manager. */
114 // IF YOU ADD ANY TABLES, don't forget to add them also to the
115 // implementation of deleteAllAttributes().
117 /** Underlying hash table for boolean-valued attributes */
118 AttrHash
<bool> d_bools
;
119 /** Underlying hash table for integral-valued attributes */
120 AttrHash
<uint64_t> d_ints
;
121 /** Underlying hash table for node-valued attributes */
122 AttrHash
<TNode
> d_tnodes
;
123 /** Underlying hash table for node-valued attributes */
124 AttrHash
<Node
> d_nodes
;
125 /** Underlying hash table for types attributes */
126 AttrHash
<TypeNode
> d_types
;
127 /** Underlying hash table for string-valued attributes */
128 AttrHash
<std::string
> d_strings
;
129 /** Underlying hash table for pointer-valued attributes */
130 AttrHash
<void*> d_ptrs
;
133 * Get a particular attribute on a particular node.
135 * @param nv the node about which to inquire
136 * @param attr the attribute kind to get
137 * @return the attribute value, if set, or a default-constructed
138 * AttrKind::value_type if not.
140 template <class AttrKind
>
141 typename
AttrKind::value_type
getAttribute(NodeValue
* nv
,
142 const AttrKind
& attr
) const;
145 * Determine if a particular attribute exists for a particular node.
147 * @param nv the node about which to inquire
148 * @param attr the attribute kind to inquire about
149 * @return true if the given node has the given attribute
151 template <class AttrKind
>
152 bool hasAttribute(NodeValue
* nv
,
153 const AttrKind
& attr
) const;
156 * Determine if a particular attribute exists for a particular node,
157 * and get it if it does.
159 * @param nv the node about which to inquire
160 * @param attr the attribute kind to inquire about
161 * @param ret a pointer to a return value, set in case the node has
163 * @return true if the given node has the given attribute
165 template <class AttrKind
>
166 bool getAttribute(NodeValue
* nv
,
167 const AttrKind
& attr
,
168 typename
AttrKind::value_type
& ret
) const;
171 * Set a particular attribute on a particular node.
173 * @param nv the node for which to set the attribute
174 * @param attr the attribute kind to set
175 * @param value a pointer to a return value, set in case the node has
177 * @return true if the given node has the given attribute
179 template <class AttrKind
>
180 void setAttribute(NodeValue
* nv
,
181 const AttrKind
& attr
,
182 const typename
AttrKind::value_type
& value
);
185 * Remove all attributes associated to the given node.
187 * @param nv the node from which to delete attributes
189 void deleteAllAttributes(NodeValue
* nv
);
192 * Remove all attributes from the tables.
194 void deleteAllAttributes();
197 * Returns true if a table is currently being deleted.
199 bool inGarbageCollection() const ;
202 * Determines the AttrTableId of an attribute.
204 * @param attr the attribute
205 * @return the id of the attribute table.
207 template <class AttrKind
>
208 static AttributeUniqueId
getAttributeId(const AttrKind
& attr
);
210 /** A list of attributes. */
211 typedef std::vector
< const AttributeUniqueId
* > AttrIdVec
;
213 /** Deletes a list of attributes. */
214 void deleteAttributes(const AttrIdVec
& attributeIds
);
217 * debugHook() is an empty function for the purpose of debugging
218 * the AttributeManager without recompiling all of CVC4.
219 * Formally this is a nop.
221 void debugHook(int debugFlag
);
224 }/* CVC4::expr::attr namespace */
226 // MAPPING OF ATTRIBUTE KINDS TO TABLES IN THE ATTRIBUTE MANAGER ===============
231 * The getTable<> template provides (static) access to the
232 * AttributeManager field holding the table.
234 template <class T
, bool context_dep
>
237 /** Access the "d_bools" member of AttributeManager. */
239 struct getTable
<bool, false> {
240 static const AttrTableId id
= AttrTableBool
;
241 typedef AttrHash
<bool> table_type
;
242 static inline table_type
& get(AttributeManager
& am
, SmtEngine
* smt
) {
245 static inline const table_type
& get(const AttributeManager
& am
, SmtEngine
* smt
) {
250 /** Access the "d_ints" member of AttributeManager. */
252 struct getTable
<uint64_t, false> {
253 static const AttrTableId id
= AttrTableUInt64
;
254 typedef AttrHash
<uint64_t> table_type
;
255 static inline table_type
& get(AttributeManager
& am
, SmtEngine
* smt
) {
258 static inline const table_type
& get(const AttributeManager
& am
, SmtEngine
* smt
) {
263 /** Access the "d_tnodes" member of AttributeManager. */
265 struct getTable
<TNode
, false> {
266 static const AttrTableId id
= AttrTableTNode
;
267 typedef AttrHash
<TNode
> table_type
;
268 static inline table_type
& get(AttributeManager
& am
, SmtEngine
* smt
) {
271 static inline const table_type
& get(const AttributeManager
& am
, SmtEngine
* smt
) {
276 /** Access the "d_nodes" member of AttributeManager. */
278 struct getTable
<Node
, false> {
279 static const AttrTableId id
= AttrTableNode
;
280 typedef AttrHash
<Node
> table_type
;
281 static inline table_type
& get(AttributeManager
& am
, SmtEngine
* smt
) {
284 static inline const table_type
& get(const AttributeManager
& am
, SmtEngine
* smt
) {
289 /** Access the "d_types" member of AttributeManager. */
291 struct getTable
<TypeNode
, false> {
292 static const AttrTableId id
= AttrTableTypeNode
;
293 typedef AttrHash
<TypeNode
> table_type
;
294 static inline table_type
& get(AttributeManager
& am
, SmtEngine
* smt
) {
297 static inline const table_type
& get(const AttributeManager
& am
, SmtEngine
* smt
) {
302 /** Access the "d_strings" member of AttributeManager. */
304 struct getTable
<std::string
, false> {
305 static const AttrTableId id
= AttrTableString
;
306 typedef AttrHash
<std::string
> table_type
;
307 static inline table_type
& get(AttributeManager
& am
, SmtEngine
* smt
) {
310 static inline const table_type
& get(const AttributeManager
& am
, SmtEngine
* smt
) {
315 /** Access the "d_ptrs" member of AttributeManager. */
317 struct getTable
<T
*, false> {
318 static const AttrTableId id
= AttrTablePointer
;
319 typedef AttrHash
<void*> table_type
;
320 static inline table_type
& get(AttributeManager
& am
, SmtEngine
* smt
) {
323 static inline const table_type
& get(const AttributeManager
& am
, SmtEngine
* smt
) {
328 /** Access the "d_ptrs" member of AttributeManager. */
330 struct getTable
<const T
*, false> {
331 static const AttrTableId id
= AttrTablePointer
;
332 typedef AttrHash
<void*> table_type
;
333 static inline table_type
& get(AttributeManager
& am
, SmtEngine
* smt
) {
336 static inline const table_type
& get(const AttributeManager
& am
, SmtEngine
* smt
) {
341 /** Access the "d_cdbools" member of AttributeManager. */
343 struct getTable
<bool, true> {
344 static const AttrTableId id
= AttrTableCDBool
;
345 typedef CDAttrHash
<bool> table_type
;
346 static inline table_type
& get(AttributeManager
& am
, SmtEngine
* smt
) {
347 return am
.getSmtAttributes(smt
).d_cdbools
;
349 static inline const table_type
& get(const AttributeManager
& am
, SmtEngine
* smt
) {
350 return am
.getSmtAttributes(smt
).d_cdbools
;
354 /** Access the "d_cdints" member of AttributeManager. */
356 struct getTable
<uint64_t, true> {
357 static const AttrTableId id
= AttrTableCDUInt64
;
358 typedef CDAttrHash
<uint64_t> table_type
;
359 static inline table_type
& get(AttributeManager
& am
, SmtEngine
* smt
) {
360 return am
.getSmtAttributes(smt
).d_cdints
;
362 static inline const table_type
& get(const AttributeManager
& am
, SmtEngine
* smt
) {
363 return am
.getSmtAttributes(smt
).d_cdints
;
367 /** Access the "d_tnodes" member of AttributeManager. */
369 struct getTable
<TNode
, true> {
370 static const AttrTableId id
= AttrTableCDTNode
;
371 typedef CDAttrHash
<TNode
> table_type
;
372 static inline table_type
& get(AttributeManager
& am
, SmtEngine
* smt
) {
373 return am
.getSmtAttributes(smt
).d_cdtnodes
;
375 static inline const table_type
& get(const AttributeManager
& am
, SmtEngine
* smt
) {
376 return am
.getSmtAttributes(smt
).d_cdtnodes
;
380 /** Access the "d_cdnodes" member of AttributeManager. */
382 struct getTable
<Node
, true> {
383 static const AttrTableId id
= AttrTableCDNode
;
384 typedef CDAttrHash
<Node
> table_type
;
385 static inline table_type
& get(AttributeManager
& am
, SmtEngine
* smt
) {
386 return am
.getSmtAttributes(smt
).d_cdnodes
;
388 static inline const table_type
& get(const AttributeManager
& am
, SmtEngine
* smt
) {
389 return am
.getSmtAttributes(smt
).d_cdnodes
;
393 /** Access the "d_cdstrings" member of AttributeManager. */
395 struct getTable
<std::string
, true> {
396 static const AttrTableId id
= AttrTableCDString
;
397 typedef CDAttrHash
<std::string
> table_type
;
398 static inline table_type
& get(AttributeManager
& am
, SmtEngine
* smt
) {
399 return am
.getSmtAttributes(smt
).d_cdstrings
;
401 static inline const table_type
& get(const AttributeManager
& am
, SmtEngine
* smt
) {
402 return am
.getSmtAttributes(smt
).d_cdstrings
;
406 /** Access the "d_cdptrs" member of AttributeManager. */
408 struct getTable
<T
*, true> {
409 static const AttrTableId id
= AttrTableCDPointer
;
410 typedef CDAttrHash
<void*> table_type
;
411 static inline table_type
& get(AttributeManager
& am
, SmtEngine
* smt
) {
412 return am
.getSmtAttributes(smt
).d_cdptrs
;
414 static inline const table_type
& get(const AttributeManager
& am
, SmtEngine
* smt
) {
415 return am
.getSmtAttributes(smt
).d_cdptrs
;
419 /** Access the "d_cdptrs" member of AttributeManager. */
421 struct getTable
<const T
*, true> {
422 static const AttrTableId id
= AttrTableCDPointer
;
423 typedef CDAttrHash
<void*> table_type
;
424 static inline table_type
& get(AttributeManager
& am
, SmtEngine
* smt
) {
425 return am
.getSmtAttributes(smt
).d_cdptrs
;
427 static inline const table_type
& get(const AttributeManager
& am
, SmtEngine
* smt
) {
428 return am
.getSmtAttributes(smt
).d_cdptrs
;
432 }/* CVC4::expr::attr namespace */
434 // ATTRIBUTE MANAGER IMPLEMENTATIONS ===========================================
438 // implementation for AttributeManager::getAttribute()
439 template <class AttrKind
>
440 typename
AttrKind::value_type
441 AttributeManager::getAttribute(NodeValue
* nv
, const AttrKind
&) const {
442 typedef typename
AttrKind::value_type value_type
;
443 typedef KindValueToTableValueMapping
<value_type
> mapping
;
444 typedef typename getTable
<value_type
, AttrKind::context_dependent
>::
445 table_type table_type
;
447 const table_type
& ah
=
448 getTable
<value_type
, AttrKind::context_dependent
>::get(*this, smt::s_smtEngine_current
);
449 typename
table_type::const_iterator i
=
450 ah
.find(std::make_pair(AttrKind::getId(), nv
));
453 return typename
AttrKind::value_type();
456 return mapping::convertBack((*i
).second
);
459 /* Helper template class for hasAttribute(), specialized based on
460 * whether AttrKind has a "default value" that all Nodes implicitly
462 template <bool has_default
, class AttrKind
>
466 * Specialization of HasAttribute<> helper template for AttrKinds
467 * with a default value.
469 template <class AttrKind
>
470 struct HasAttribute
<true, AttrKind
> {
471 /** This implementation is simple; it's always true. */
472 static inline bool hasAttribute(const AttributeManager
* am
,
478 * This implementation returns the AttrKind's default value if the
479 * Node doesn't have the given attribute.
481 static inline bool getAttribute(const AttributeManager
* am
,
483 typename
AttrKind::value_type
& ret
) {
484 typedef typename
AttrKind::value_type value_type
;
485 typedef KindValueToTableValueMapping
<value_type
> mapping
;
486 typedef typename getTable
<value_type
,
487 AttrKind::context_dependent
>::table_type
490 const table_type
& ah
=
491 getTable
<value_type
, AttrKind::context_dependent
>::get(*am
, smt::s_smtEngine_current
);
492 typename
table_type::const_iterator i
=
493 ah
.find(std::make_pair(AttrKind::getId(), nv
));
496 ret
= AttrKind::default_value
;
498 ret
= mapping::convertBack((*i
).second
);
506 * Specialization of HasAttribute<> helper template for AttrKinds
507 * without a default value.
509 template <class AttrKind
>
510 struct HasAttribute
<false, AttrKind
> {
511 static inline bool hasAttribute(const AttributeManager
* am
,
513 typedef typename
AttrKind::value_type value_type
;
514 //typedef KindValueToTableValueMapping<value_type> mapping;
515 typedef typename getTable
<value_type
, AttrKind::context_dependent
>::
516 table_type table_type
;
518 const table_type
& ah
=
519 getTable
<value_type
, AttrKind::context_dependent
>::get(*am
, smt::s_smtEngine_current
);
520 typename
table_type::const_iterator i
=
521 ah
.find(std::make_pair(AttrKind::getId(), nv
));
530 static inline bool getAttribute(const AttributeManager
* am
,
532 typename
AttrKind::value_type
& ret
) {
533 typedef typename
AttrKind::value_type value_type
;
534 typedef KindValueToTableValueMapping
<value_type
> mapping
;
535 typedef typename getTable
<value_type
, AttrKind::context_dependent
>::
536 table_type table_type
;
538 const table_type
& ah
=
539 getTable
<value_type
, AttrKind::context_dependent
>::get(*am
, smt::s_smtEngine_current
);
540 typename
table_type::const_iterator i
=
541 ah
.find(std::make_pair(AttrKind::getId(), nv
));
547 ret
= mapping::convertBack((*i
).second
);
553 template <class AttrKind
>
554 bool AttributeManager::hasAttribute(NodeValue
* nv
,
555 const AttrKind
&) const {
556 return HasAttribute
<AttrKind::has_default_value
, AttrKind
>::
557 hasAttribute(this, nv
);
560 template <class AttrKind
>
561 bool AttributeManager::getAttribute(NodeValue
* nv
,
563 typename
AttrKind::value_type
& ret
) const {
564 return HasAttribute
<AttrKind::has_default_value
, AttrKind
>::
565 getAttribute(this, nv
, ret
);
568 template <class AttrKind
>
570 AttributeManager::setAttribute(NodeValue
* nv
,
572 const typename
AttrKind::value_type
& value
) {
573 typedef typename
AttrKind::value_type value_type
;
574 typedef KindValueToTableValueMapping
<value_type
> mapping
;
575 typedef typename getTable
<value_type
, AttrKind::context_dependent
>::
576 table_type table_type
;
579 getTable
<value_type
, AttrKind::context_dependent
>::get(*this, smt::s_smtEngine_current
);
580 ah
[std::make_pair(AttrKind::getId(), nv
)] = mapping::convert(value
);
584 * Search for the NodeValue in all attribute tables and remove it,
585 * calling the cleanup function if one is defined.
587 * This cannot use nv as anything other than a pointer!
590 inline void AttributeManager::deleteFromTable(AttrHash
<T
>& table
,
592 for(uint64_t id
= 0; id
< attr::LastAttributeId
<T
, false>::getId(); ++id
) {
593 typedef AttributeTraits
<T
, false> traits_t
;
594 typedef AttrHash
<T
> hash_t
;
595 std::pair
<uint64_t, NodeValue
*> pr
= std::make_pair(id
, nv
);
596 if(traits_t::getCleanup()[id
] != NULL
) {
597 typename
hash_t::iterator i
= table
.find(pr
);
598 if(i
!= table
.end()) {
599 traits_t::getCleanup()[id
]((*i
).second
);
609 * Obliterate a NodeValue from a (context-dependent) attribute table.
612 inline void SmtAttributes::deleteFromTable(CDAttrHash
<T
>& table
,
614 for(unsigned id
= 0; id
< attr::LastAttributeId
<T
, true>::getId(); ++id
) {
615 table
.obliterate(std::make_pair(id
, nv
));
620 * Remove all attributes from the table calling the cleanup function
624 inline void AttributeManager::deleteAllFromTable(AttrHash
<T
>& table
) {
625 Assert(!d_inGarbageCollection
);
626 d_inGarbageCollection
= true;
628 bool anyRequireClearing
= false;
629 typedef AttributeTraits
<T
, false> traits_t
;
630 typedef AttrHash
<T
> hash_t
;
631 for(uint64_t id
= 0; id
< attr::LastAttributeId
<T
, false>::getId(); ++id
) {
632 if(traits_t::getCleanup()[id
] != NULL
) {
633 anyRequireClearing
= true;
637 if(anyRequireClearing
) {
638 typename
hash_t::iterator it
= table
.begin();
639 typename
hash_t::iterator it_end
= table
.end();
641 while (it
!= it_end
){
642 uint64_t id
= (*it
).first
.first
;
644 Debug("attrgc") << "id " << id
645 << " node_value: " << ((*it).first.second)
648 if(traits_t::getCleanup()[id
] != NULL
) {
649 traits_t::getCleanup()[id
]((*it
).second
);
655 d_inGarbageCollection
= false;
656 Assert(!d_inGarbageCollection
);
659 template <class AttrKind
>
660 AttributeUniqueId
AttributeManager::getAttributeId(const AttrKind
& attr
){
661 typedef typename
AttrKind::value_type value_type
;
662 AttrTableId tableId
= getTable
<value_type
,
663 AttrKind::context_dependent
>::id
;
664 return AttributeUniqueId(tableId
, attr
.getId());
668 void AttributeManager::deleteAttributesFromTable(AttrHash
<T
>& table
, const std::vector
<uint64_t>& ids
){
669 d_inGarbageCollection
= true;
670 typedef AttributeTraits
<T
, false> traits_t
;
671 typedef AttrHash
<T
> hash_t
;
673 typename
hash_t::iterator it
= table
.begin();
674 typename
hash_t::iterator tmp
;
675 typename
hash_t::iterator it_end
= table
.end();
677 std::vector
<uint64_t>::const_iterator begin_ids
= ids
.begin();
678 std::vector
<uint64_t>::const_iterator end_ids
= ids
.end();
680 size_t initialSize
= table
.size();
681 while (it
!= it_end
){
682 uint64_t id
= (*it
).first
.first
;
684 if(std::binary_search(begin_ids
, end_ids
, id
)){
687 if(traits_t::getCleanup()[id
] != NULL
) {
688 traits_t::getCleanup()[id
]((*tmp
).second
);
695 d_inGarbageCollection
= false;
696 static const size_t ReconstructShrinkRatio
= 8;
697 if(initialSize
/ReconstructShrinkRatio
> table
.size()){
698 reconstructTable(table
);
703 void AttributeManager::reconstructTable(AttrHash
<T
>& table
){
704 d_inGarbageCollection
= true;
705 typedef AttrHash
<T
> hash_t
;
707 cpy
.insert(table
.begin(), table
.end());
709 d_inGarbageCollection
= false;
713 }/* CVC4::expr::attr namespace */
714 }/* CVC4::expr namespace */
716 template <class AttrKind
>
717 inline typename
AttrKind::value_type
718 NodeManager::getAttribute(expr::NodeValue
* nv
, const AttrKind
&) const {
719 return d_attrManager
->getAttribute(nv
, AttrKind());
722 template <class AttrKind
>
723 inline bool NodeManager::hasAttribute(expr::NodeValue
* nv
,
724 const AttrKind
&) const {
725 return d_attrManager
->hasAttribute(nv
, AttrKind());
728 template <class AttrKind
>
730 NodeManager::getAttribute(expr::NodeValue
* nv
, const AttrKind
&,
731 typename
AttrKind::value_type
& ret
) const {
732 return d_attrManager
->getAttribute(nv
, AttrKind(), ret
);
735 template <class AttrKind
>
737 NodeManager::setAttribute(expr::NodeValue
* nv
, const AttrKind
&,
738 const typename
AttrKind::value_type
& value
) {
739 d_attrManager
->setAttribute(nv
, AttrKind(), value
);
742 template <class AttrKind
>
743 inline typename
AttrKind::value_type
744 NodeManager::getAttribute(TNode n
, const AttrKind
&) const {
745 return d_attrManager
->getAttribute(n
.d_nv
, AttrKind());
748 template <class AttrKind
>
750 NodeManager::hasAttribute(TNode n
, const AttrKind
&) const {
751 return d_attrManager
->hasAttribute(n
.d_nv
, AttrKind());
754 template <class AttrKind
>
756 NodeManager::getAttribute(TNode n
, const AttrKind
&,
757 typename
AttrKind::value_type
& ret
) const {
758 return d_attrManager
->getAttribute(n
.d_nv
, AttrKind(), ret
);
761 template <class AttrKind
>
763 NodeManager::setAttribute(TNode n
, const AttrKind
&,
764 const typename
AttrKind::value_type
& value
) {
765 d_attrManager
->setAttribute(n
.d_nv
, AttrKind(), value
);
768 template <class AttrKind
>
769 inline typename
AttrKind::value_type
770 NodeManager::getAttribute(TypeNode n
, const AttrKind
&) const {
771 return d_attrManager
->getAttribute(n
.d_nv
, AttrKind());
774 template <class AttrKind
>
776 NodeManager::hasAttribute(TypeNode n
, const AttrKind
&) const {
777 return d_attrManager
->hasAttribute(n
.d_nv
, AttrKind());
780 template <class AttrKind
>
782 NodeManager::getAttribute(TypeNode n
, const AttrKind
&,
783 typename
AttrKind::value_type
& ret
) const {
784 return d_attrManager
->getAttribute(n
.d_nv
, AttrKind(), ret
);
787 template <class AttrKind
>
789 NodeManager::setAttribute(TypeNode n
, const AttrKind
&,
790 const typename
AttrKind::value_type
& value
) {
791 d_attrManager
->setAttribute(n
.d_nv
, AttrKind(), value
);
794 }/* CVC4 namespace */
796 #endif /* __CVC4__EXPR__ATTRIBUTE_H */