Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Node attributes.
11 : : */
12 : :
13 : : #include "cvc5_private.h"
14 : :
15 : : /* There are strong constraints on ordering of declarations of
16 : : * attributes and nodes due to template use */
17 : : #include "expr/node.h"
18 : : #include "expr/type_node.h"
19 : :
20 : : #ifndef CVC5__EXPR__ATTRIBUTE_H
21 : : #define CVC5__EXPR__ATTRIBUTE_H
22 : :
23 : : #include <string>
24 : :
25 : : #include "expr/attribute_unique_id.h"
26 : :
27 : : // include supporting templates
28 : : #define CVC5_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
29 : : #include "expr/attribute_internals.h"
30 : : #undef CVC5_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
31 : :
32 : : namespace cvc5::internal {
33 : : namespace expr {
34 : : namespace attr {
35 : :
36 : : /**
37 : : * Attributes are roughly speaking [almost] global hash tables from Nodes
38 : : * (TNodes) to data. Attributes can be thought of as additional fields used to
39 : : * extend NodeValues. Attributes are mutable. Attributes live only as long as
40 : : * the node itself does. If a Node is garbage-collected, Attributes associated
41 : : * with it will automatically be garbage collected. (Being in the domain of an
42 : : * Attribute does not increase a Node's reference count.) To achieve this
43 : : * special relationship with Nodes, Attributes are mapped by hash tables
44 : : * (AttrHash<>) that live in the AttributeManager. The AttributeManager is
45 : : * owned by the NodeManager.
46 : : *
47 : : * Example:
48 : : *
49 : : * Attributes tend to be defined in a fixed pattern:
50 : : *
51 : : * ```
52 : : * struct InstLevelAttributeId {};
53 : : * typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
54 : : * ```
55 : : *
56 : : * To get the value of an Attribute InstLevelAttribute on a Node n, use
57 : : * ```
58 : : * n.getAttribute(InstLevelAttribute());
59 : : * ```
60 : : *
61 : : * To check whether the attribute has been set:
62 : : * ```
63 : : * n.hasAttribute(InstLevelAttribute());
64 : : * ```
65 : : *
66 : : * To separate Attributes of the same type in the same table, each of the
67 : : * structures `struct InstLevelAttributeId {};` is given a different unique
68 : : * value at load time. An example is the empty struct InstLevelAttributeId.
69 : : * These should be unique for each Attribute. Then via some template messiness
70 : : * when InstLevelAttribute() is passed as the argument to getAttribute(...) the
71 : : * load time id is instantiated.
72 : : */
73 : : // ATTRIBUTE MANAGER ===========================================================
74 : :
75 : : /**
76 : : * A container for the main attribute tables of the system. There's a
77 : : * one-to-one NodeManager : AttributeManager correspondence.
78 : : */
79 : : class AttributeManager
80 : : {
81 : : template <class T>
82 : : void deleteFromTable(AttrHash<T>& table, NodeValue* nv);
83 : :
84 : : template <class T>
85 : : void deleteAllFromTable(AttrHash<T>& table);
86 : :
87 : : template <class T>
88 : : void deleteAttributesFromTable(AttrHash<T>& table,
89 : : const std::vector<uint64_t>& ids);
90 : :
91 : : template <class T>
92 : : void reconstructTable(AttrHash<T>& table);
93 : :
94 : : /**
95 : : * getTable<> is a helper template that gets the right table from an
96 : : * AttributeManager given its type.
97 : : */
98 : : template <class T, class Enable>
99 : : friend struct getTable;
100 : :
101 : : bool d_inGarbageCollection;
102 : :
103 : : void clearDeleteAllAttributesBuffer();
104 : :
105 : : public:
106 : : /** Construct an attribute manager. */
107 : : AttributeManager();
108 : :
109 : : // IF YOU ADD ANY TABLES, don't forget to add them also to the
110 : : // implementation of deleteAllAttributes().
111 : :
112 : : /** Underlying hash table for boolean-valued attributes */
113 : : AttrHash<bool> d_bools;
114 : : /** Underlying hash table for integral-valued attributes */
115 : : AttrHash<uint64_t> d_ints;
116 : : /** Underlying hash table for node-valued attributes */
117 : : AttrHash<TNode> d_tnodes;
118 : : /** Underlying hash table for node-valued attributes */
119 : : AttrHash<Node> d_nodes;
120 : : /** Underlying hash table for types attributes */
121 : : AttrHash<TypeNode> d_types;
122 : : /** Underlying hash table for string-valued attributes */
123 : : AttrHash<std::string> d_strings;
124 : :
125 : : /**
126 : : * Get a particular attribute on a particular node.
127 : : *
128 : : * @param nv the node about which to inquire
129 : : * @param attr the attribute kind to get
130 : : * @return the attribute value, if set, or a default-constructed
131 : : * AttrKind::value_type if not.
132 : : */
133 : : template <class AttrKind>
134 : : typename AttrKind::value_type getAttribute(NodeValue* nv,
135 : : const AttrKind& attr) const;
136 : :
137 : : /**
138 : : * Determine if a particular attribute exists for a particular node.
139 : : *
140 : : * @param nv the node about which to inquire
141 : : * @param attr the attribute kind to inquire about
142 : : * @return true if the given node has the given attribute
143 : : */
144 : : template <class AttrKind>
145 : : bool hasAttribute(NodeValue* nv, const AttrKind& attr) const;
146 : :
147 : : /**
148 : : * Determine if a particular attribute exists for a particular node,
149 : : * and get it if it does.
150 : : *
151 : : * @param nv the node about which to inquire
152 : : * @param attr the attribute kind to inquire about
153 : : * @param ret a pointer to a return value, set in case the node has
154 : : * the attribute
155 : : * @return true if the given node has the given attribute
156 : : */
157 : : template <class AttrKind>
158 : : bool getAttribute(NodeValue* nv,
159 : : const AttrKind& attr,
160 : : typename AttrKind::value_type& ret) const;
161 : :
162 : : /**
163 : : * Set a particular attribute on a particular node.
164 : : *
165 : : * @param nv the node for which to set the attribute
166 : : * @param attr the attribute kind to set
167 : : * @param value a pointer to a return value, set in case the node has
168 : : * the attribute
169 : : * @return true if the given node has the given attribute
170 : : */
171 : : template <class AttrKind>
172 : : void setAttribute(NodeValue* nv,
173 : : const AttrKind& attr,
174 : : const typename AttrKind::value_type& value);
175 : :
176 : : /**
177 : : * Remove all attributes associated to the given node.
178 : : *
179 : : * @param nv the node from which to delete attributes
180 : : */
181 : : void deleteAllAttributes(NodeValue* nv);
182 : :
183 : : /**
184 : : * Remove all attributes from the tables.
185 : : */
186 : : void deleteAllAttributes();
187 : :
188 : : /**
189 : : * Returns true if a table is currently being deleted.
190 : : */
191 : : bool inGarbageCollection() const;
192 : :
193 : : /**
194 : : * Determines the AttrTableId of an attribute.
195 : : *
196 : : * @param attr the attribute
197 : : * @return the id of the attribute table.
198 : : */
199 : : template <class AttrKind>
200 : : static AttributeUniqueId getAttributeId(const AttrKind& attr);
201 : :
202 : : /** A list of attributes. */
203 : : typedef std::vector<const AttributeUniqueId*> AttrIdVec;
204 : :
205 : : /** Deletes a list of attributes. */
206 : : void deleteAttributes(const AttrIdVec& attributeIds);
207 : :
208 : : /**
209 : : * debugHook() is an empty function for the purpose of debugging
210 : : * the AttributeManager without recompiling all of cvc5.
211 : : * Formally this is a nop.
212 : : */
213 : : void debugHook(int debugFlag);
214 : : };
215 : :
216 : : } // namespace attr
217 : :
218 : : // MAPPING OF ATTRIBUTE KINDS TO TABLES IN THE ATTRIBUTE MANAGER ===============
219 : :
220 : : namespace attr {
221 : :
222 : : /**
223 : : * The getTable<> template provides (static) access to the
224 : : * AttributeManager field holding the table.
225 : : *
226 : : * The `Enable` template parameter is used to instantiate the template
227 : : * conditionally: If the template substitution of Enable fails (e.g. when using
228 : : * `std::enable_if` in the template parameter and the condition is false), the
229 : : * instantiation is ignored due to the SFINAE rule.
230 : : */
231 : : template <class T, class Enable = void>
232 : : struct getTable;
233 : :
234 : : /** Access the "d_bools" member of AttributeManager. */
235 : : template <>
236 : : struct getTable<bool>
237 : : {
238 : : static const AttrTableId id = AttrTableBool;
239 : : typedef AttrHash<bool> table_type;
240 : 211914452 : static inline table_type& get(AttributeManager& am) { return am.d_bools; }
241 : 2026967264 : static inline const table_type& get(const AttributeManager& am)
242 : : {
243 : 2026967264 : return am.d_bools;
244 : : }
245 : : };
246 : :
247 : : /** Access the "d_ints" member of AttributeManager. */
248 : : template <class T>
249 : : struct getTable<T,
250 : : // Use this specialization only for unsigned integers
251 : : typename std::enable_if<std::is_unsigned<T>::value>::type>
252 : : {
253 : : static const AttrTableId id = AttrTableUInt64;
254 : : typedef AttrHash<uint64_t> table_type;
255 : 898535 : static inline table_type& get(AttributeManager& am) { return am.d_ints; }
256 : 65916914 : static inline const table_type& get(const AttributeManager& am)
257 : : {
258 : 65916914 : return am.d_ints;
259 : : }
260 : : };
261 : :
262 : : /** Access the "d_tnodes" member of AttributeManager. */
263 : : template <>
264 : : struct getTable<TNode>
265 : : {
266 : : static const AttrTableId id = AttrTableTNode;
267 : : typedef AttrHash<TNode> table_type;
268 : 1 : static inline table_type& get(AttributeManager& am) { return am.d_tnodes; }
269 : 2 : static inline const table_type& get(const AttributeManager& am)
270 : : {
271 : 2 : return am.d_tnodes;
272 : : }
273 : : };
274 : :
275 : : /** Access the "d_nodes" member of AttributeManager. */
276 : : template <>
277 : : struct getTable<Node>
278 : : {
279 : : static const AttrTableId id = AttrTableNode;
280 : : typedef AttrHash<Node> table_type;
281 : 47718999 : static inline table_type& get(AttributeManager& am) { return am.d_nodes; }
282 : 474773947 : static inline const table_type& get(const AttributeManager& am)
283 : : {
284 : 474773947 : return am.d_nodes;
285 : : }
286 : : };
287 : :
288 : : /** Access the "d_types" member of AttributeManager. */
289 : : template <>
290 : : struct getTable<TypeNode>
291 : : {
292 : : static const AttrTableId id = AttrTableTypeNode;
293 : : typedef AttrHash<TypeNode> table_type;
294 : 143561558 : static inline table_type& get(AttributeManager& am) { return am.d_types; }
295 : 2754479524 : static inline const table_type& get(const AttributeManager& am)
296 : : {
297 : 2754479524 : return am.d_types;
298 : : }
299 : : };
300 : :
301 : : /** Access the "d_strings" member of AttributeManager. */
302 : : template <>
303 : : struct getTable<std::string>
304 : : {
305 : : static const AttrTableId id = AttrTableString;
306 : : typedef AttrHash<std::string> table_type;
307 : 22442535 : static inline table_type& get(AttributeManager& am) { return am.d_strings; }
308 : 44483224 : static inline const table_type& get(const AttributeManager& am)
309 : : {
310 : 44483224 : return am.d_strings;
311 : : }
312 : : };
313 : :
314 : : } // namespace attr
315 : :
316 : : // ATTRIBUTE MANAGER IMPLEMENTATIONS ===========================================
317 : :
318 : : namespace attr {
319 : :
320 : : // implementation for AttributeManager::getAttribute()
321 : : template <class AttrKind>
322 : 2726234495 : typename AttrKind::value_type AttributeManager::getAttribute(
323 : : NodeValue* nv, const AttrKind&) const
324 : : {
325 : : typedef typename AttrKind::value_type value_type;
326 : : typedef KindValueToTableValueMapping<value_type> mapping;
327 : : typedef typename getTable<value_type>::table_type table_type;
328 : :
329 : 2726234495 : const table_type& ah = getTable<value_type>::get(*this);
330 : : typename table_type::const_iterator i =
331 : 2726234495 : ah.find(std::make_pair(AttrKind::getId(), nv));
332 : :
333 [ + + ]: 2726234495 : if (i == ah.end())
334 : : {
335 : 363368880 : return typename AttrKind::value_type();
336 : : }
337 : :
338 : 2782792533 : return mapping::convertBack((*i).second);
339 : : }
340 : :
341 : : /* Helper template class for hasAttribute(), specialized based on
342 : : * whether AttrKind has a "default value" that all Nodes implicitly
343 : : * have or not. */
344 : : template <bool has_default, class AttrKind>
345 : : struct HasAttribute;
346 : :
347 : : /**
348 : : * Specialization of HasAttribute<> helper template for AttrKinds
349 : : * with a default value.
350 : : */
351 : : template <class AttrKind>
352 : : struct HasAttribute<true, AttrKind>
353 : : {
354 : : /** This implementation is simple; it's always true. */
355 : 20 : static inline bool hasAttribute(CVC5_UNUSED const AttributeManager* am,
356 : : CVC5_UNUSED NodeValue* nv)
357 : : {
358 : 20 : return true;
359 : : }
360 : :
361 : : /**
362 : : * This implementation returns the AttrKind's default value if the
363 : : * Node doesn't have the given attribute.
364 : : */
365 : 22 : static inline bool getAttribute(const AttributeManager* am,
366 : : NodeValue* nv,
367 : : typename AttrKind::value_type& ret)
368 : : {
369 : : typedef typename AttrKind::value_type value_type;
370 : : typedef KindValueToTableValueMapping<value_type> mapping;
371 : : typedef typename getTable<value_type>::table_type table_type;
372 : :
373 : 22 : const table_type& ah = getTable<value_type>::get(*am);
374 : : typename table_type::const_iterator i =
375 : 22 : ah.find(std::make_pair(AttrKind::getId(), nv));
376 : :
377 [ - + ]: 22 : if (i == ah.end())
378 : : {
379 : 0 : ret = AttrKind::default_value;
380 : : }
381 : : else
382 : : {
383 : 22 : ret = mapping::convertBack((*i).second);
384 : : }
385 : :
386 : 22 : return true;
387 : : }
388 : : };
389 : :
390 : : /**
391 : : * Specialization of HasAttribute<> helper template for AttrKinds
392 : : * without a default value.
393 : : */
394 : : template <class AttrKind>
395 : : struct HasAttribute<false, AttrKind>
396 : : {
397 : 455531016 : static inline bool hasAttribute(const AttributeManager* am, NodeValue* nv)
398 : : {
399 : : typedef typename AttrKind::value_type value_type;
400 : : // typedef KindValueToTableValueMapping<value_type> mapping;
401 : : typedef typename getTable<value_type>::table_type table_type;
402 : :
403 : 455531016 : const table_type& ah = getTable<value_type>::get(*am);
404 : : typename table_type::const_iterator i =
405 : 455531016 : ah.find(std::make_pair(AttrKind::getId(), nv));
406 : :
407 [ + + ]: 455531016 : if (i == ah.end())
408 : : {
409 : 103089782 : return false;
410 : : }
411 : :
412 : 352441234 : return true;
413 : : }
414 : :
415 : 2184855342 : static inline bool getAttribute(const AttributeManager* am,
416 : : NodeValue* nv,
417 : : typename AttrKind::value_type& ret)
418 : : {
419 : : typedef typename AttrKind::value_type value_type;
420 : : typedef KindValueToTableValueMapping<value_type> mapping;
421 : : typedef typename getTable<value_type>::table_type table_type;
422 : :
423 : 2184855342 : const table_type& ah = getTable<value_type>::get(*am);
424 : : typename table_type::const_iterator i =
425 : 2184855342 : ah.find(std::make_pair(AttrKind::getId(), nv));
426 : :
427 [ + + ]: 2184855342 : if (i == ah.end())
428 : : {
429 : 120041902 : return false;
430 : : }
431 : :
432 : 2064813440 : ret = mapping::convertBack((*i).second);
433 : :
434 : 2064813440 : return true;
435 : : }
436 : : };
437 : :
438 : : template <class AttrKind>
439 : 455531036 : bool AttributeManager::hasAttribute(NodeValue* nv, const AttrKind&) const
440 : : {
441 : 455531036 : return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this,
442 : 455531036 : nv);
443 : : }
444 : :
445 : : template <class AttrKind>
446 : 2184855364 : bool AttributeManager::getAttribute(NodeValue* nv,
447 : : const AttrKind&,
448 : : typename AttrKind::value_type& ret) const
449 : : {
450 : 2184855364 : return HasAttribute<AttrKind::has_default_value, AttrKind>::getAttribute(
451 : 2184855364 : this, nv, ret);
452 : : }
453 : :
454 : : template <class AttrKind>
455 : 426536080 : inline void AttributeManager::setAttribute(
456 : : NodeValue* nv, const AttrKind&, const typename AttrKind::value_type& value)
457 : : {
458 : : typedef typename AttrKind::value_type value_type;
459 : : typedef KindValueToTableValueMapping<value_type> mapping;
460 : : typedef typename getTable<value_type>::table_type table_type;
461 : :
462 : 426536080 : table_type& ah = getTable<value_type>::get(*this);
463 : 426536080 : ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value);
464 : 426536080 : }
465 : :
466 : : /** Search for the NodeValue in all attribute tables and remove it. */
467 : : template <class T>
468 : 837460385 : inline void AttributeManager::deleteFromTable(AttrHash<T>& table, NodeValue* nv)
469 : : {
470 : 837460385 : table.eraseBy(nv);
471 : 837460385 : }
472 : :
473 : : /** Remove all attributes from the table. */
474 : : template <class T>
475 : 363600 : inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table)
476 : : {
477 [ - + ][ - + ]: 363600 : Assert(!d_inGarbageCollection);
[ - - ]
478 : 363600 : d_inGarbageCollection = true;
479 : 363600 : table.clear();
480 : 363600 : d_inGarbageCollection = false;
481 [ - + ][ - + ]: 363600 : Assert(!d_inGarbageCollection);
[ - - ]
482 : 363600 : }
483 : :
484 : : template <class AttrKind>
485 : : AttributeUniqueId AttributeManager::getAttributeId(const AttrKind& attr)
486 : : {
487 : : typedef typename AttrKind::value_type value_type;
488 : : AttrTableId tableId = getTable<value_type>::id;
489 : : return AttributeUniqueId(tableId, attr.getId());
490 : : }
491 : :
492 : : template <class T>
493 : 0 : void AttributeManager::deleteAttributesFromTable(
494 : : AttrHash<T>& table, const std::vector<uint64_t>& ids)
495 : : {
496 : 0 : d_inGarbageCollection = true;
497 : : typedef AttrHash<T> hash_t;
498 : :
499 : 0 : typename hash_t::iterator it = table.begin();
500 : 0 : typename hash_t::iterator tmp;
501 : 0 : typename hash_t::iterator it_end = table.end();
502 : :
503 : 0 : std::vector<uint64_t>::const_iterator begin_ids = ids.begin();
504 : 0 : std::vector<uint64_t>::const_iterator end_ids = ids.end();
505 : :
506 : 0 : size_t initialSize = table.size();
507 [ - - ]: 0 : while (it != it_end)
508 : : {
509 : 0 : uint64_t id = (*it).first.first;
510 : :
511 [ - - ]: 0 : if (std::binary_search(begin_ids, end_ids, id))
512 : : {
513 : 0 : it = table.erase(it);
514 : : }
515 : : else
516 : : {
517 : 0 : ++it;
518 : : }
519 : : }
520 : 0 : d_inGarbageCollection = false;
521 : : static const size_t ReconstructShrinkRatio = 8;
522 [ - - ]: 0 : if (initialSize / ReconstructShrinkRatio > table.size())
523 : : {
524 : 0 : reconstructTable(table);
525 : : }
526 : 0 : }
527 : :
528 : : template <class T>
529 : 0 : void AttributeManager::reconstructTable(AttrHash<T>& table)
530 : : {
531 : 0 : d_inGarbageCollection = true;
532 : : typedef AttrHash<T> hash_t;
533 : 0 : hash_t cpy;
534 : 0 : cpy.insert(table.begin(), table.end());
535 : 0 : cpy.swap(table);
536 : 0 : d_inGarbageCollection = false;
537 : 0 : }
538 : :
539 : : } // namespace attr
540 : : } // namespace expr
541 : :
542 : : template <class AttrKind>
543 : 27621427 : inline typename AttrKind::value_type NodeManager::getAttribute(
544 : : expr::NodeValue* nv, const AttrKind&) const
545 : : {
546 : 27632902 : return d_attrManager->getAttribute(nv, AttrKind());
547 : : }
548 : :
549 : : template <class AttrKind>
550 : 18436880 : inline bool NodeManager::hasAttribute(expr::NodeValue* nv,
551 : : const AttrKind&) const
552 : : {
553 : 18436880 : return d_attrManager->hasAttribute(nv, AttrKind());
554 : : }
555 : :
556 : : template <class AttrKind>
557 : : inline bool NodeManager::getAttribute(expr::NodeValue* nv,
558 : : const AttrKind&,
559 : : typename AttrKind::value_type& ret) const
560 : : {
561 : : return d_attrManager->getAttribute(nv, AttrKind(), ret);
562 : : }
563 : :
564 : : template <class AttrKind>
565 : 170979 : inline void NodeManager::setAttribute(
566 : : expr::NodeValue* nv,
567 : : const AttrKind&,
568 : : const typename AttrKind::value_type& value)
569 : : {
570 : 170979 : d_attrManager->setAttribute(nv, AttrKind(), value);
571 : 170979 : }
572 : :
573 : : template <class AttrKind>
574 : 2697395556 : inline typename AttrKind::value_type NodeManager::getAttribute(
575 : : TNode n, const AttrKind&) const
576 : : {
577 : 3358288630 : return d_attrManager->getAttribute(n.d_nv, AttrKind());
578 : : }
579 : :
580 : : template <class AttrKind>
581 : 437094156 : inline bool NodeManager::hasAttribute(TNode n, const AttrKind&) const
582 : : {
583 : 437094156 : return d_attrManager->hasAttribute(n.d_nv, AttrKind());
584 : : }
585 : :
586 : : template <class AttrKind>
587 : 2184855364 : inline bool NodeManager::getAttribute(TNode n,
588 : : const AttrKind&,
589 : : typename AttrKind::value_type& ret) const
590 : : {
591 : 2184855364 : return d_attrManager->getAttribute(n.d_nv, AttrKind(), ret);
592 : : }
593 : :
594 : : template <class AttrKind>
595 : 426072122 : inline void NodeManager::setAttribute(
596 : : TNode n, const AttrKind&, const typename AttrKind::value_type& value)
597 : : {
598 : 426072122 : d_attrManager->setAttribute(n.d_nv, AttrKind(), value);
599 : 426072122 : }
600 : :
601 : : template <class AttrKind>
602 : 1217512 : inline typename AttrKind::value_type NodeManager::getAttribute(
603 : : TypeNode n, const AttrKind&) const
604 : : {
605 : 2435024 : return d_attrManager->getAttribute(n.d_nv, AttrKind());
606 : : }
607 : :
608 : : template <class AttrKind>
609 : : inline bool NodeManager::hasAttribute(TypeNode n, const AttrKind&) const
610 : : {
611 : : return d_attrManager->hasAttribute(n.d_nv, AttrKind());
612 : : }
613 : :
614 : : template <class AttrKind>
615 : : inline bool NodeManager::getAttribute(TypeNode n,
616 : : const AttrKind&,
617 : : typename AttrKind::value_type& ret) const
618 : : {
619 : : return d_attrManager->getAttribute(n.d_nv, AttrKind(), ret);
620 : : }
621 : :
622 : : template <class AttrKind>
623 : 292979 : inline void NodeManager::setAttribute(
624 : : TypeNode n, const AttrKind&, const typename AttrKind::value_type& value)
625 : : {
626 : 292979 : d_attrManager->setAttribute(n.d_nv, AttrKind(), value);
627 : 292979 : }
628 : :
629 : : } // namespace cvc5::internal
630 : :
631 : : #endif /* CVC5__EXPR__ATTRIBUTE_H */
|
