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 : : #include "expr/attribute_unique_id.h"
25 : :
26 : : // include supporting templates
27 : : #define CVC5_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
28 : : #include "expr/attribute_internals.h"
29 : : #undef CVC5_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
30 : :
31 : : namespace cvc5::internal {
32 : : namespace expr {
33 : : namespace attr {
34 : :
35 : : /**
36 : : * Attributes are roughly speaking [almost] global hash tables from Nodes
37 : : * (TNodes) to data. Attributes can be thought of as additional fields used to
38 : : * extend NodeValues. Attributes are mutable. Attributes live only as long as
39 : : * the node itself does. If a Node is garbage-collected, Attributes associated
40 : : * with it will automatically be garbage collected. (Being in the domain of an
41 : : * Attribute does not increase a Node's reference count.) To achieve this
42 : : * special relationship with Nodes, Attributes are mapped by hash tables
43 : : * (AttrHash<>) that live in the AttributeManager. The AttributeManager is
44 : : * owned by the NodeManager.
45 : : *
46 : : * Example:
47 : : *
48 : : * Attributes tend to be defined in a fixed pattern:
49 : : *
50 : : * ```
51 : : * struct InstLevelAttributeId {};
52 : : * typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
53 : : * ```
54 : : *
55 : : * To get the value of an Attribute InstLevelAttribute on a Node n, use
56 : : * ```
57 : : * n.getAttribute(InstLevelAttribute());
58 : : * ```
59 : : *
60 : : * To check whether the attribute has been set:
61 : : * ```
62 : : * n.hasAttribute(InstLevelAttribute());
63 : : * ```
64 : : *
65 : : * To separate Attributes of the same type in the same table, each of the
66 : : * structures `struct InstLevelAttributeId {};` is given a different unique
67 : : * value at load time. An example is the empty struct InstLevelAttributeId.
68 : : * These should be unique for each Attribute. Then via some template messiness
69 : : * when InstLevelAttribute() is passed as the argument to getAttribute(...) the
70 : : * load time id is instantiated.
71 : : */
72 : : // ATTRIBUTE MANAGER ===========================================================
73 : :
74 : : /**
75 : : * A container for the main attribute tables of the system. There's a
76 : : * one-to-one NodeManager : AttributeManager correspondence.
77 : : */
78 : : class AttributeManager {
79 : :
80 : : template <class T>
81 : : void deleteFromTable(AttrHash<T>& table, NodeValue* nv);
82 : :
83 : : template <class T>
84 : : void deleteAllFromTable(AttrHash<T>& table);
85 : :
86 : : template <class T>
87 : : void deleteAttributesFromTable(AttrHash<T>& table, const std::vector<uint64_t>& ids);
88 : :
89 : : template <class T>
90 : : void reconstructTable(AttrHash<T>& table);
91 : :
92 : : /**
93 : : * getTable<> is a helper template that gets the right table from an
94 : : * AttributeManager given its type.
95 : : */
96 : : template <class T, class Enable>
97 : : friend struct getTable;
98 : :
99 : : bool d_inGarbageCollection;
100 : :
101 : : void clearDeleteAllAttributesBuffer();
102 : :
103 : : public:
104 : :
105 : : /** Construct an attribute manager. */
106 : : AttributeManager();
107 : :
108 : : // IF YOU ADD ANY TABLES, don't forget to add them also to the
109 : : // implementation of deleteAllAttributes().
110 : :
111 : : /** Underlying hash table for boolean-valued attributes */
112 : : AttrHash<bool> d_bools;
113 : : /** Underlying hash table for integral-valued attributes */
114 : : AttrHash<uint64_t> d_ints;
115 : : /** Underlying hash table for node-valued attributes */
116 : : AttrHash<TNode> d_tnodes;
117 : : /** Underlying hash table for node-valued attributes */
118 : : AttrHash<Node> d_nodes;
119 : : /** Underlying hash table for types attributes */
120 : : AttrHash<TypeNode> d_types;
121 : : /** Underlying hash table for string-valued attributes */
122 : : AttrHash<std::string> d_strings;
123 : :
124 : : /**
125 : : * Get a particular attribute on a particular node.
126 : : *
127 : : * @param nv the node about which to inquire
128 : : * @param attr the attribute kind to get
129 : : * @return the attribute value, if set, or a default-constructed
130 : : * AttrKind::value_type if not.
131 : : */
132 : : template <class AttrKind>
133 : : typename AttrKind::value_type getAttribute(NodeValue* nv,
134 : : const AttrKind& attr) const;
135 : :
136 : : /**
137 : : * Determine if a particular attribute exists for a particular node.
138 : : *
139 : : * @param nv the node about which to inquire
140 : : * @param attr the attribute kind to inquire about
141 : : * @return true if the given node has the given attribute
142 : : */
143 : : template <class AttrKind>
144 : : bool hasAttribute(NodeValue* nv,
145 : : 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 : 201473094 : static inline table_type& get(AttributeManager& am) {
241 : 201473094 : return am.d_bools;
242 : : }
243 : 1895970928 : static inline const table_type& get(const AttributeManager& am) {
244 : 1895970928 : return am.d_bools;
245 : : }
246 : : };
247 : :
248 : : /** Access the "d_ints" member of AttributeManager. */
249 : : template <class T>
250 : : struct getTable<T,
251 : : // Use this specialization only for unsigned integers
252 : : typename std::enable_if<std::is_unsigned<T>::value>::type>
253 : : {
254 : : static const AttrTableId id = AttrTableUInt64;
255 : : typedef AttrHash<uint64_t> table_type;
256 : 879038 : static inline table_type& get(AttributeManager& am) {
257 : 879038 : return am.d_ints;
258 : : }
259 : 56427689 : static inline const table_type& get(const AttributeManager& am) {
260 : 56427689 : return am.d_ints;
261 : : }
262 : : };
263 : :
264 : : /** Access the "d_tnodes" member of AttributeManager. */
265 : : template <>
266 : : struct getTable<TNode>
267 : : {
268 : : static const AttrTableId id = AttrTableTNode;
269 : : typedef AttrHash<TNode> table_type;
270 : 1 : static inline table_type& get(AttributeManager& am) {
271 : 1 : return am.d_tnodes;
272 : : }
273 : 2 : static inline const table_type& get(const AttributeManager& am) {
274 : 2 : return am.d_tnodes;
275 : : }
276 : : };
277 : :
278 : : /** Access the "d_nodes" member of AttributeManager. */
279 : : template <>
280 : : struct getTable<Node>
281 : : {
282 : : static const AttrTableId id = AttrTableNode;
283 : : typedef AttrHash<Node> table_type;
284 : 44876455 : static inline table_type& get(AttributeManager& am) {
285 : 44876455 : return am.d_nodes;
286 : : }
287 : 446460414 : static inline const table_type& get(const AttributeManager& am) {
288 : 446460414 : return am.d_nodes;
289 : : }
290 : : };
291 : :
292 : : /** Access the "d_types" member of AttributeManager. */
293 : : template <>
294 : : struct getTable<TypeNode>
295 : : {
296 : : static const AttrTableId id = AttrTableTypeNode;
297 : : typedef AttrHash<TypeNode> table_type;
298 : 135692388 : static inline table_type& get(AttributeManager& am) {
299 : 135692388 : return am.d_types;
300 : : }
301 : 2622472522 : static inline const table_type& get(const AttributeManager& am) {
302 : 2622472522 : return am.d_types;
303 : : }
304 : : };
305 : :
306 : : /** Access the "d_strings" member of AttributeManager. */
307 : : template <>
308 : : struct getTable<std::string>
309 : : {
310 : : static const AttrTableId id = AttrTableString;
311 : : typedef AttrHash<std::string> table_type;
312 : 21775854 : static inline table_type& get(AttributeManager& am) {
313 : 21775854 : return am.d_strings;
314 : : }
315 : 44240228 : static inline const table_type& get(const AttributeManager& am) {
316 : 44240228 : return am.d_strings;
317 : : }
318 : : };
319 : :
320 : : } // namespace attr
321 : :
322 : : // ATTRIBUTE MANAGER IMPLEMENTATIONS ===========================================
323 : :
324 : : namespace attr {
325 : :
326 : : // implementation for AttributeManager::getAttribute()
327 : : template <class AttrKind>
328 : : typename AttrKind::value_type
329 : 2555306692 : AttributeManager::getAttribute(NodeValue* nv, const AttrKind&) const {
330 : : typedef typename AttrKind::value_type value_type;
331 : : typedef KindValueToTableValueMapping<value_type> mapping;
332 : : typedef typename getTable<value_type>::table_type table_type;
333 : :
334 : 2555306692 : const table_type& ah = getTable<value_type>::get(*this);
335 : : typename table_type::const_iterator i =
336 : 2555306692 : ah.find(std::make_pair(AttrKind::getId(), nv));
337 : :
338 [ + + ]: 2555306692 : if(i == ah.end()) {
339 : 341866547 : return typename AttrKind::value_type();
340 : : }
341 : :
342 : 2612694281 : return mapping::convertBack((*i).second);
343 : : }
344 : :
345 : : /* Helper template class for hasAttribute(), specialized based on
346 : : * whether AttrKind has a "default value" that all Nodes implicitly
347 : : * have or not. */
348 : : template <bool has_default, class AttrKind>
349 : : struct HasAttribute;
350 : :
351 : : /**
352 : : * Specialization of HasAttribute<> helper template for AttrKinds
353 : : * with a default value.
354 : : */
355 : : template <class AttrKind>
356 : : struct HasAttribute<true, AttrKind> {
357 : : /** This implementation is simple; it's always true. */
358 : 20 : static inline bool hasAttribute(CVC5_UNUSED const AttributeManager* am,
359 : : CVC5_UNUSED NodeValue* nv)
360 : : {
361 : 20 : return true;
362 : : }
363 : :
364 : : /**
365 : : * This implementation returns the AttrKind's default value if the
366 : : * Node doesn't have the given attribute.
367 : : */
368 : 22 : static inline bool getAttribute(const AttributeManager* am,
369 : : NodeValue* nv,
370 : : typename AttrKind::value_type& ret) {
371 : : typedef typename AttrKind::value_type value_type;
372 : : typedef KindValueToTableValueMapping<value_type> mapping;
373 : : typedef typename getTable<value_type>::table_type table_type;
374 : :
375 : 22 : const table_type& ah = getTable<value_type>::get(*am);
376 : : typename table_type::const_iterator i =
377 : 22 : ah.find(std::make_pair(AttrKind::getId(), nv));
378 : :
379 [ - + ]: 22 : if(i == ah.end()) {
380 : 0 : ret = AttrKind::default_value;
381 : : } else {
382 : 22 : ret = mapping::convertBack((*i).second);
383 : : }
384 : :
385 : 22 : return true;
386 : : }
387 : : };
388 : :
389 : : /**
390 : : * Specialization of HasAttribute<> helper template for AttrKinds
391 : : * without a default value.
392 : : */
393 : : template <class AttrKind>
394 : : struct HasAttribute<false, AttrKind> {
395 : 426234801 : static inline bool hasAttribute(const AttributeManager* am,
396 : : NodeValue* nv) {
397 : : typedef typename AttrKind::value_type value_type;
398 : : //typedef KindValueToTableValueMapping<value_type> mapping;
399 : : typedef typename getTable<value_type>::table_type table_type;
400 : :
401 : 426234801 : const table_type& ah = getTable<value_type>::get(*am);
402 : : typename table_type::const_iterator i =
403 : 426234801 : ah.find(std::make_pair(AttrKind::getId(), nv));
404 : :
405 [ + + ]: 426234801 : if(i == ah.end()) {
406 : 96483964 : return false;
407 : : }
408 : :
409 : 329750837 : return true;
410 : : }
411 : :
412 : 2084030268 : static inline bool getAttribute(const AttributeManager* am,
413 : : NodeValue* nv,
414 : : typename AttrKind::value_type& ret) {
415 : : typedef typename AttrKind::value_type value_type;
416 : : typedef KindValueToTableValueMapping<value_type> mapping;
417 : : typedef typename getTable<value_type>::table_type table_type;
418 : :
419 : 2084030268 : const table_type& ah = getTable<value_type>::get(*am);
420 : : typename table_type::const_iterator i =
421 : 2084030268 : ah.find(std::make_pair(AttrKind::getId(), nv));
422 : :
423 [ + + ]: 2084030268 : if(i == ah.end()) {
424 : 112855943 : return false;
425 : : }
426 : :
427 : 1971174325 : ret = mapping::convertBack((*i).second);
428 : :
429 : 1971174325 : return true;
430 : : }
431 : : };
432 : :
433 : : template <class AttrKind>
434 : 426234821 : bool AttributeManager::hasAttribute(NodeValue* nv,
435 : : const AttrKind&) const {
436 : : return HasAttribute<AttrKind::has_default_value, AttrKind>::
437 : 426234821 : hasAttribute(this, nv);
438 : : }
439 : :
440 : : template <class AttrKind>
441 : 2084030290 : bool AttributeManager::getAttribute(NodeValue* nv,
442 : : const AttrKind&,
443 : : typename AttrKind::value_type& ret) const {
444 : : return HasAttribute<AttrKind::has_default_value, AttrKind>::
445 : 2084030290 : getAttribute(this, nv, ret);
446 : : }
447 : :
448 : : template <class AttrKind>
449 : : inline void
450 : 404696830 : AttributeManager::setAttribute(NodeValue* nv,
451 : : const AttrKind&,
452 : : const typename AttrKind::value_type& value) {
453 : : typedef typename AttrKind::value_type value_type;
454 : : typedef KindValueToTableValueMapping<value_type> mapping;
455 : : typedef typename getTable<value_type>::table_type table_type;
456 : :
457 : 404696830 : table_type& ah = getTable<value_type>::get(*this);
458 : 404696830 : ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value);
459 : 404696830 : }
460 : :
461 : : /** Search for the NodeValue in all attribute tables and remove it. */
462 : : template <class T>
463 : 797602660 : inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
464 : : NodeValue* nv) {
465 : 797602660 : table.eraseBy(nv);
466 : 797602660 : }
467 : :
468 : : /** Remove all attributes from the table. */
469 : : template <class T>
470 : 362210 : inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
471 [ - + ][ - + ]: 362210 : Assert(!d_inGarbageCollection);
[ - - ]
472 : 362210 : d_inGarbageCollection = true;
473 : 362210 : table.clear();
474 : 362210 : d_inGarbageCollection = false;
475 [ - + ][ - + ]: 362210 : Assert(!d_inGarbageCollection);
[ - - ]
476 : 362210 : }
477 : :
478 : : template <class AttrKind>
479 : : AttributeUniqueId AttributeManager::getAttributeId(const AttrKind& attr){
480 : : typedef typename AttrKind::value_type value_type;
481 : : AttrTableId tableId = getTable<value_type>::id;
482 : : return AttributeUniqueId(tableId, attr.getId());
483 : : }
484 : :
485 : : template <class T>
486 : 0 : void AttributeManager::deleteAttributesFromTable(AttrHash<T>& table, const std::vector<uint64_t>& ids){
487 : 0 : d_inGarbageCollection = true;
488 : : typedef AttrHash<T> hash_t;
489 : :
490 : 0 : typename hash_t::iterator it = table.begin();
491 : 0 : typename hash_t::iterator tmp;
492 : 0 : typename hash_t::iterator it_end = table.end();
493 : :
494 : 0 : std::vector<uint64_t>::const_iterator begin_ids = ids.begin();
495 : 0 : std::vector<uint64_t>::const_iterator end_ids = ids.end();
496 : :
497 : 0 : size_t initialSize = table.size();
498 [ - - ]: 0 : while (it != it_end){
499 : 0 : uint64_t id = (*it).first.first;
500 : :
501 [ - - ]: 0 : if(std::binary_search(begin_ids, end_ids, id)){
502 : 0 : it = table.erase(it);
503 : : }else{
504 : 0 : ++it;
505 : : }
506 : : }
507 : 0 : d_inGarbageCollection = false;
508 : : static const size_t ReconstructShrinkRatio = 8;
509 [ - - ]: 0 : if(initialSize/ReconstructShrinkRatio > table.size()){
510 : 0 : reconstructTable(table);
511 : : }
512 : 0 : }
513 : :
514 : : template <class T>
515 : 0 : void AttributeManager::reconstructTable(AttrHash<T>& table){
516 : 0 : d_inGarbageCollection = true;
517 : : typedef AttrHash<T> hash_t;
518 : 0 : hash_t cpy;
519 : 0 : cpy.insert(table.begin(), table.end());
520 : 0 : cpy.swap(table);
521 : 0 : d_inGarbageCollection = false;
522 : 0 : }
523 : :
524 : : } // namespace attr
525 : : } // namespace expr
526 : :
527 : : template <class AttrKind>
528 : : inline typename AttrKind::value_type
529 : 26522674 : NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&) const {
530 : 26533709 : return d_attrManager->getAttribute(nv, AttrKind());
531 : : }
532 : :
533 : : template <class AttrKind>
534 : 17725262 : inline bool NodeManager::hasAttribute(expr::NodeValue* nv,
535 : : const AttrKind&) const {
536 : 17725262 : return d_attrManager->hasAttribute(nv, AttrKind());
537 : : }
538 : :
539 : : template <class AttrKind>
540 : : inline bool
541 : : NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&,
542 : : typename AttrKind::value_type& ret) const {
543 : : return d_attrManager->getAttribute(nv, AttrKind(), ret);
544 : : }
545 : :
546 : : template <class AttrKind>
547 : : inline void
548 : 168419 : NodeManager::setAttribute(expr::NodeValue* nv, const AttrKind&,
549 : : const typename AttrKind::value_type& value) {
550 : 168419 : d_attrManager->setAttribute(nv, AttrKind(), value);
551 : 168419 : }
552 : :
553 : : template <class AttrKind>
554 : : inline typename AttrKind::value_type
555 : 2527574006 : NodeManager::getAttribute(TNode n, const AttrKind&) const {
556 : 3153404071 : return d_attrManager->getAttribute(n.d_nv, AttrKind());
557 : : }
558 : :
559 : : template <class AttrKind>
560 : : inline bool
561 : 408509559 : NodeManager::hasAttribute(TNode n, const AttrKind&) const {
562 : 408509559 : return d_attrManager->hasAttribute(n.d_nv, AttrKind());
563 : : }
564 : :
565 : : template <class AttrKind>
566 : : inline bool
567 : 2084030290 : NodeManager::getAttribute(TNode n, const AttrKind&,
568 : : typename AttrKind::value_type& ret) const {
569 : 2084030290 : return d_attrManager->getAttribute(n.d_nv, AttrKind(), ret);
570 : : }
571 : :
572 : : template <class AttrKind>
573 : : inline void
574 : 404240952 : NodeManager::setAttribute(TNode n, const AttrKind&,
575 : : const typename AttrKind::value_type& value) {
576 : 404240952 : d_attrManager->setAttribute(n.d_nv, AttrKind(), value);
577 : 404240952 : }
578 : :
579 : : template <class AttrKind>
580 : : inline typename AttrKind::value_type
581 : 1210012 : NodeManager::getAttribute(TypeNode n, const AttrKind&) const {
582 : 2420024 : return d_attrManager->getAttribute(n.d_nv, AttrKind());
583 : : }
584 : :
585 : : template <class AttrKind>
586 : : inline bool
587 : : NodeManager::hasAttribute(TypeNode n, const AttrKind&) const {
588 : : return d_attrManager->hasAttribute(n.d_nv, AttrKind());
589 : : }
590 : :
591 : : template <class AttrKind>
592 : : inline bool
593 : : NodeManager::getAttribute(TypeNode n, const AttrKind&,
594 : : typename AttrKind::value_type& ret) const {
595 : : return d_attrManager->getAttribute(n.d_nv, AttrKind(), ret);
596 : : }
597 : :
598 : : template <class AttrKind>
599 : : inline void
600 : 287459 : NodeManager::setAttribute(TypeNode n, const AttrKind&,
601 : : const typename AttrKind::value_type& value) {
602 : 287459 : d_attrManager->setAttribute(n.d_nv, AttrKind(), value);
603 : 287459 : }
604 : :
605 : : } // namespace cvc5::internal
606 : :
607 : : #endif /* CVC5__EXPR__ATTRIBUTE_H */
|
