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' internals.
11 : : */
12 : :
13 : : #include <stdint.h>
14 : :
15 : : #include <algorithm>
16 : : #include <numeric>
17 : :
18 : : #include "cvc5_private.h"
19 : :
20 : : #ifndef CVC5_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
21 : : #error expr/attribute_internals.h should only be included by expr/attribute.h
22 : : #endif /* CVC5_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H */
23 : :
24 : : #ifndef CVC5__EXPR__ATTRIBUTE_INTERNALS_H
25 : : #define CVC5__EXPR__ATTRIBUTE_INTERNALS_H
26 : :
27 : : #include <unordered_map>
28 : :
29 : : namespace cvc5::internal {
30 : : namespace expr {
31 : :
32 : : // ATTRIBUTE HASH FUNCTIONS ====================================================
33 : :
34 : : namespace attr {
35 : :
36 : : /**
37 : : * A hash function for attribute table keys. Attribute table keys are
38 : : * pairs, (unique-attribute-id, Node).
39 : : */
40 : : struct AttrHashFunction
41 : : {
42 : : enum
43 : : {
44 : : LARGE_PRIME = 32452843ul
45 : : };
46 : : std::size_t operator()(const std::pair<uint64_t, NodeValue*>& p) const
47 : : {
48 : : return p.first * LARGE_PRIME + p.second->getId();
49 : : }
50 : : }; /* struct AttrHashFunction */
51 : :
52 : : /**
53 : : * A hash function for boolean-valued attribute table keys; here we
54 : : * don't have to store a pair as the key, because we use a known bit
55 : : * in [0..63] for each attribute
56 : : */
57 : : struct AttrBoolHashFunction
58 : : {
59 : 6771113282 : std::size_t operator()(NodeValue* nv) const { return (size_t)nv->getId(); }
60 : : }; /* struct AttrBoolHashFunction */
61 : :
62 : : } // namespace attr
63 : :
64 : : // ATTRIBUTE TYPE MAPPINGS =====================================================
65 : :
66 : : namespace attr {
67 : :
68 : : /**
69 : : * KindValueToTableValueMapping is a compile-time-only mechanism to
70 : : * convert "attribute value types" into "table value types" and back
71 : : * again.
72 : : *
73 : : * Each instantiation < T > is expected to have three members:
74 : : *
75 : : * typename table_value_type
76 : : *
77 : : * A type representing the underlying table's value_type for
78 : : * attribute value type (T). It may be different from T, e.g. T
79 : : * could be a pointer-to-Foo, but the underlying table value_type
80 : : * might be pointer-to-void.
81 : : *
82 : : * static [convertible-to-table_value_type] convert([convertible-from-T])
83 : : *
84 : : * Converts a T into a table_value_type. Used to convert an
85 : : * attribute value on setting it (and assigning it into the
86 : : * underlying table). See notes on specializations of
87 : : * KindValueToTableValueMapping, below.
88 : : *
89 : : * static [convertible-to-T] convertBack([convertible-from-table_value_type])
90 : : *
91 : : * Converts a table_value_type back into a T. Used to convert an
92 : : * underlying table value back into the attribute's expected type
93 : : * when retrieving it from the table. See notes on
94 : : * specializations of KindValueToTableValueMapping, below.
95 : : *
96 : : * This general (non-specialized) implementation of the template does
97 : : * nothing.
98 : : *
99 : : * The `Enable` template parameter is used to instantiate the template
100 : : * conditionally: If the template substitution of Enable fails (e.g. when using
101 : : * `std::enable_if` in the template parameter and the condition is false), the
102 : : * instantiation is ignored due to the SFINAE rule.
103 : : */
104 : : template <class T, class Enable = void>
105 : : struct KindValueToTableValueMapping
106 : : {
107 : : /** Simple case: T == table_value_type */
108 : : typedef T table_value_type;
109 : : /** No conversion necessary */
110 : 213278834 : inline static T convert(const T& t) { return t; }
111 : : /** No conversion necessary */
112 : 2478710598 : inline static T convertBack(const T& t) { return t; }
113 : : };
114 : :
115 : : /**
116 : : * This converts arbitrary unsigned integers (up to 64-bit) to and from 64-bit
117 : : * integers s.t. they can be stored in the hash table for integral-valued
118 : : * attributes.
119 : : */
120 : : template <class T>
121 : : struct KindValueToTableValueMapping<
122 : : T,
123 : : // Use this specialization only for unsigned integers
124 : : typename std::enable_if<std::is_unsigned<T>::value>::type>
125 : : {
126 : : typedef uint64_t table_value_type;
127 : : /** Convert from unsigned integer to uint64_t */
128 : 212292485 : static uint64_t convert(const T& t)
129 : : {
130 : : static_assert(sizeof(T) <= sizeof(uint64_t),
131 : : "Cannot store integer attributes of a bit-width that is "
132 : : "greater than 64-bits");
133 : 212292485 : return static_cast<uint64_t>(t);
134 : : }
135 : : /** Convert from uint64_t to unsigned integer */
136 : 1927837697 : static T convertBack(const uint64_t& t) { return static_cast<T>(t); }
137 : : };
138 : :
139 : : } // namespace attr
140 : :
141 : : // ATTRIBUTE HASH TABLES =======================================================
142 : :
143 : : namespace attr {
144 : :
145 : : // Returns a 64 bit integer with a single `bit` set when `bit` < 64.
146 : : // Avoids problems in (1 << x) when sizeof(x) <= sizeof(uint64_t).
147 : 2102351456 : inline uint64_t GetBitSet(uint64_t bit)
148 : : {
149 : 2102351456 : constexpr uint64_t kOne = 1;
150 : 2102351456 : return kOne << bit;
151 : : }
152 : :
153 : : /**
154 : : * An "AttrHash<V>"---the hash table underlying
155 : : * attributes---is a mapping of pair<unique-attribute-id, Node>
156 : : * to V using a two-level hash+flat_map structure. The top level
157 : : * uses NodeValue* as its key, allowing rapid deletion of matching
158 : : * collections of entries, while the second level, keyed on Ids
159 : : * and implemented with a sorted vector, optimizes for size and
160 : : * speed for small collections.
161 : : */
162 : : template <class V>
163 : : class AttrHash
164 : : {
165 : : // Second level flat map uint64_t -> V
166 : : class IdMap
167 : : {
168 : : public:
169 : : using value_type = std::pair<uint64_t, V>;
170 : : using Container = std::vector<value_type>;
171 : : using iterator = typename Container::iterator;
172 : : using const_iterator = typename Container::const_iterator;
173 : :
174 : : // only the methods required by AttrHash<V>:
175 : :
176 : 3 : const_iterator begin() const { return d_contents.begin(); }
177 : 2932718087 : const_iterator end() const { return d_contents.end(); }
178 : :
179 : 21 : iterator begin() { return d_contents.begin(); }
180 : 82 : iterator end() { return d_contents.end(); }
181 : :
182 : 36 : std::size_t size() const { return d_contents.size(); }
183 : :
184 : 5 : bool empty() const { return d_contents.empty(); }
185 : :
186 : 11 : void reserve(std::size_t sz) { d_contents.reserve(sz); }
187 : :
188 : 20 : std::pair<iterator, bool> emplace(uint64_t k, V v)
189 : : {
190 : 20 : value_type p = std::make_pair(k, std::move(v));
191 : : auto range =
192 : 20 : std::equal_range(d_contents.begin(),
193 : : d_contents.end(),
194 : : p,
195 : 15 : [](const value_type& a, const value_type& b) {
196 : 15 : return a.first < b.first;
197 : : });
198 [ + + ]: 20 : if (range.first != range.second)
199 : : {
200 : : // key already present, don't insert
201 : 2 : return std::make_pair(iterator{}, false);
202 : : }
203 : :
204 : 18 : return std::make_pair(d_contents.insert(range.first, std::move(p)), true);
205 : 0 : }
206 : :
207 : 2932718081 : const_iterator find(uint64_t key) const
208 : : {
209 : : auto range =
210 : 2932718081 : std::equal_range(d_contents.begin(),
211 : : d_contents.end(),
212 : 5800672512 : std::make_pair(key, V{}),
213 : 6312458875 : [](const value_type& a, const value_type& b) {
214 : 6312458875 : return a.first < b.first;
215 : : });
216 [ + + ]: 2932718081 : if (range.first == range.second)
217 : : {
218 : : // not in map
219 : 66213705 : return d_contents.end();
220 : : }
221 : 2866504376 : return range.first;
222 : : }
223 : :
224 : 31 : iterator find(uint64_t key)
225 : : {
226 : : auto range =
227 : 31 : std::equal_range(d_contents.begin(),
228 : : d_contents.end(),
229 : 31 : std::make_pair(key, V{}),
230 : 94 : [](const value_type& a, const value_type& b) {
231 : 94 : return a.first < b.first;
232 : : });
233 [ + + ]: 31 : if (range.first == range.second)
234 : : {
235 : 2 : return d_contents.end();
236 : : }
237 : 29 : return range.first;
238 : : }
239 : :
240 : 5 : iterator erase(iterator pos) { return d_contents.erase(pos); }
241 : :
242 : 214176790 : V& operator[](uint64_t key)
243 : : {
244 : : iterator it =
245 : 214176790 : std::lower_bound(d_contents.begin(),
246 : : d_contents.end(),
247 : 427455624 : std::make_pair(key, V{}),
248 : 29732493 : [](const value_type& a, const value_type& b) {
249 : 29732493 : return a.first < b.first;
250 : : });
251 [ + + ][ + + ]: 214176790 : if ((it == d_contents.end()) || (it->first != key))
[ + + ]
252 : : {
253 : : // not in map
254 : 209340728 : it = d_contents.insert(it, std::make_pair(key, V{}));
255 : : }
256 : 214176790 : return (*it).second;
257 : : }
258 : :
259 : : // range insert
260 : : template <typename Iter>
261 : : void insert(Iter beg, Iter end)
262 : : {
263 : : for (Iter it = beg; it != end; ++it)
264 : : {
265 : : iterator found_it =
266 : : std::lower_bound(d_contents.begin(),
267 : : d_contents.end(),
268 : : it->first,
269 : : [](const value_type& a, const value_type& b) {
270 : : return a.first < b.first;
271 : : });
272 : : if ((found_it != d_contents.end()) && (it->first == found_it->first))
273 : : {
274 : : // this key is already present in the map. replace it:
275 : : found_it->second = it->second;
276 : : }
277 : : else
278 : : {
279 : : d_contents.insert(found_it, *it);
280 : : }
281 : : }
282 : : }
283 : :
284 : : private:
285 : : Container d_contents;
286 : : };
287 : :
288 : : // a composite iterator combining a top-level (std::unordered_map)
289 : : // iterator with a lower-level (IdMap) iterator to preserve the
290 : : // illusion of a single map. Together they identify a virtual
291 : : // element pair<pair<uint64_t, NodeValue*>, V> expected by
292 : : // users of AttrHash<V>.
293 : : template <typename Parent, typename L1It, typename L2It>
294 : : class Iterator
295 : : {
296 : : // access for AttrHash to implement erase(Iterator)
297 : : using NonConstParent = typename std::remove_const_t<Parent>;
298 : : using NonConstIterator = typename NonConstParent::iterator;
299 : : friend NonConstIterator Parent::erase(NonConstIterator);
300 : :
301 : : public:
302 : : // requirements for ForwardIterator
303 : : using iterator_category = std::forward_iterator_tag;
304 : : using value_type = std::pair<std::pair<uint64_t, NodeValue*>, V>;
305 : : using reference = value_type; // we don't supply a true reference
306 : : using pointer = value_type*;
307 : : using difference_type = std::ptrdiff_t;
308 : :
309 : : // default constructor
310 : 3794956435 : Iterator() : d_atEnd{true} {}
311 : :
312 : 13 : Iterator(Parent* parent)
313 : 13 : : d_parent{parent}, d_l1It(parent->d_storage.begin())
314 : : {
315 : 13 : d_atEnd = (d_l1It == parent->d_storage.end());
316 [ + + ]: 13 : if (!d_atEnd)
317 : : {
318 : 12 : d_l2It = d_l1It->second.begin();
319 : 12 : legalize(); // L2 map may be empty
320 : : }
321 : 13 : }
322 : :
323 : : // prerequisite: l1_it and l2_it are valid iterators
324 : 2866504410 : Iterator(Parent* parent, L1It l1_it, L2It l2_it)
325 : 2866504410 : : d_atEnd(l1_it == parent->d_storage.end()),
326 : 2866504410 : d_parent(parent),
327 : 2866504410 : d_l1It(l1_it),
328 : 2866504410 : d_l2It(l2_it)
329 : : {
330 : 2866504410 : }
331 : :
332 : : // increment
333 : 28 : Iterator& operator++() // pre
334 : : {
335 : 28 : increment();
336 : 28 : return *this;
337 : : }
338 : :
339 : : Iterator operator++(int) // post
340 : : {
341 : : Iterator tmp = *this;
342 : : increment();
343 : : return tmp;
344 : : }
345 : :
346 : : // dereference
347 : 2515591395 : value_type operator*() const
348 : : {
349 : 5031182790 : return std::make_pair(std::make_pair(d_l2It->first, d_l1It->first),
350 : 7546774185 : d_l2It->second);
351 : : }
352 : :
353 : : // comparison
354 : 3330730451 : bool operator==(Iterator const& other) const
355 : : {
356 [ - + ]: 464226022 : return (d_atEnd && other.d_atEnd)
357 [ + + ][ + - ]: 3794956475 : || (!d_atEnd && !other.d_atEnd && (d_l1It == other.d_l1It)
[ + + ][ + - ]
358 [ + - ]: 3330730453 : && (d_l2It == other.d_l2It));
359 : : }
360 : 57 : bool operator!=(Iterator const& other) const { return !(*this == other); }
361 : :
362 : : private:
363 : 28 : void increment()
364 : : {
365 : 28 : ++d_l2It;
366 : :
367 : 28 : legalize(); // we may be at the end of the current L2 map
368 : 28 : }
369 : :
370 : : // if necessary, adjust L1/L2 iterators so they point at a real element
371 : : // called whenever a change may cause the L2 iterator to point to the end
372 : : // of the current L2 map, e.g.:
373 : : // initialization: the first L2 map is empty
374 : : // increment: the L2 iterator was pointing at the last element
375 : : // erase: the L2 iterator was pointing at the erased element and there are
376 : : // no more
377 : 45 : void legalize()
378 : : {
379 : : // move forward to next valid entry
380 [ + + ]: 57 : while (d_l2It == d_l1It->second.end())
381 : : {
382 : 20 : ++d_l1It;
383 [ + + ]: 20 : if (d_l1It == d_parent->d_storage.end())
384 : : {
385 : 8 : d_atEnd = true;
386 : 8 : return;
387 : : }
388 : 12 : d_l2It = d_l1It->second.begin();
389 : : }
390 : : }
391 : :
392 : : /** Whether at the end of all entries (matches only other end sentinels) */
393 : : bool d_atEnd;
394 : :
395 : : /** The AttrHash this iterator belongs to */
396 : : Parent* d_parent;
397 : :
398 : : /** Iterator within the top-level std::unordered_map */
399 : : L1It d_l1It;
400 : :
401 : : /** Iterator within the second level IdMap (sorted vector) */
402 : : L2It d_l2It;
403 : : };
404 : :
405 : : using Storage = std::unordered_map<NodeValue*, IdMap, AttrBoolHashFunction>;
406 : :
407 : : public:
408 : : using iterator = Iterator<AttrHash<V>,
409 : : typename Storage::iterator,
410 : : typename IdMap::iterator>;
411 : : using const_iterator = Iterator<const AttrHash<V>,
412 : : typename Storage::const_iterator,
413 : : typename IdMap::const_iterator>;
414 : :
415 : 15 : std::size_t size() const
416 : : {
417 : 15 : return std::accumulate(
418 : : d_storage.begin(),
419 : : d_storage.end(),
420 : : 0u,
421 : 25 : [](std::size_t sum, const std::pair<NodeValue*, IdMap>& l2) {
422 : 25 : return sum + l2.second.size();
423 : 15 : });
424 : : }
425 : :
426 : 11 : iterator begin() { return iterator(this); }
427 : 33 : iterator end() { return iterator(); }
428 : :
429 : 2 : const_iterator begin() const
430 : : {
431 : 2 : return const_iterator(const_cast<AttrHash<V>*>(this));
432 : : }
433 : 3330730388 : const_iterator end() const { return const_iterator(); }
434 : :
435 : 5 : iterator erase(iterator it)
436 : : {
437 : : // reach inside the iterator to get L1/L2 positions
438 : 5 : auto nextL2It = it.d_l1It->second.erase(it.d_l2It);
439 : :
440 : 5 : iterator nextIt(this, it.d_l1It, nextL2It);
441 : 5 : nextIt.legalize();
442 : :
443 [ + + ]: 5 : if (it.d_l1It->second.empty())
444 : : {
445 : : // this erase has made the L2 map empty. delete it:
446 : 2 : d_storage.erase(it.d_l1It);
447 : : }
448 : :
449 : 10 : return nextIt;
450 : : }
451 : :
452 : : template <typename Iter>
453 : 5 : void insert(Iter beg, Iter end)
454 : : {
455 : : using Entry = typename std::iterator_traits<Iter>::value_type;
456 : : using Entries = std::vector<Entry>;
457 : : using EntryIt = typename Entries::iterator;
458 : 5 : Entries entries(beg, end);
459 : :
460 : : // sort by second (NodeValue*) then first (uint64_t)
461 : 5 : std::sort(
462 : 36 : entries.begin(), entries.end(), [](const Entry& a, const Entry& b) {
463 : 36 : return (a.first.second < b.first.second)
464 [ + + ][ + + ]: 50 : || ((a.first.second == b.first.second)
[ - - ][ - - ]
[ - - ][ - - ]
[ - - ][ - - ]
[ - - ][ - - ]
465 [ - + ][ - - ]: 50 : && (a.first.first < b.first.first));
[ - - ][ - - ]
[ - - ]
466 : : });
467 : :
468 : 11 : auto find_different_nv = [](NodeValue* nv, EntryIt first, EntryIt last) {
469 : 11 : return std::find_if(
470 : 37 : first, last, [nv](const Entry& a) { return a.first.second != nv; });
471 : : };
472 : :
473 : : // determine number of new L1 entries required (count unique NodeValue*s)
474 : 5 : std::size_t l1_unique_count = 0;
475 : 5 : auto last = entries.end();
476 [ + + ]: 16 : for (EntryIt it = entries.begin(); it != last;
477 : 11 : it = find_different_nv(it->first.second, it, entries.end()))
478 : : {
479 : 11 : ++l1_unique_count;
480 : : }
481 : : // pre-allocate enough space for the new L1 entries (for speed)
482 : 5 : d_storage.reserve(d_storage.size() + l1_unique_count);
483 : :
484 : : // add new entries one (same NodeValue*) chunk at a time
485 [ + + ]: 16 : for (EntryIt it = entries.begin(); it != last;)
486 : : {
487 : : // identify range of entries with the same NodeValue* (a "chunk")
488 : 11 : EntryIt chunk_end = std::find_if(it, entries.end(), [it](const Entry& v) {
489 : 26 : return v.first.second != it->first.second;
490 : : });
491 : : // add to corresponding l2 map
492 : 11 : auto& l2 = d_storage[it->first.second];
493 : 11 : l2.reserve(l2.size() + std::distance(it, chunk_end));
494 [ + + ]: 31 : for (; it != chunk_end; ++it)
495 : : {
496 : 20 : l2.emplace(it->first.first, it->second);
497 : : }
498 : : }
499 : 5 : }
500 : :
501 : 0 : void swap(AttrHash& other) { std::swap(d_storage, other.d_storage); }
502 : :
503 : 214176790 : V& operator[](std::pair<uint64_t, NodeValue*> p)
504 : : {
505 : 214176790 : return d_storage[p.second][p.first];
506 : : }
507 : :
508 : 363491 : void clear() { d_storage.clear(); }
509 : :
510 : 3330730386 : const_iterator find(std::pair<uint64_t, NodeValue*> p) const
511 : : {
512 : 3330730386 : typename Storage::const_iterator it1 = d_storage.find(p.second);
513 [ + + ]: 3330730386 : if (it1 == d_storage.end()) return const_iterator();
514 : :
515 : 2932718081 : typename IdMap::const_iterator it2 = it1->second.find(p.first);
516 [ + + ]: 2932718081 : if (it2 == it1->second.end()) return const_iterator();
517 : :
518 : 2866504376 : return const_iterator(this, it1, it2);
519 : : }
520 : :
521 : 33 : iterator find(std::pair<uint64_t, NodeValue*> p)
522 : : {
523 : 33 : typename Storage::iterator it1 = d_storage.find(p.second);
524 [ + + ]: 33 : if (it1 == d_storage.end()) return iterator();
525 : :
526 : 31 : typename IdMap::iterator it2 = it1->second.find(p.first);
527 [ + + ]: 31 : if (it2 == it1->second.end()) return iterator();
528 : :
529 : 29 : return iterator(this, it1, it2);
530 : : }
531 : :
532 : 835815912 : void eraseBy(NodeValue* nv) { d_storage.erase(nv); }
533 : :
534 : : private:
535 : : Storage d_storage;
536 : : }; /* class AttrHash<> */
537 : :
538 : : /**
539 : : * In the case of Boolean-valued attributes we have a special
540 : : * "AttrHash<bool>" to pack bits together in words.
541 : : */
542 : : template <>
543 : : class AttrHash<bool>
544 : : : protected std::unordered_map<NodeValue*, uint64_t, AttrBoolHashFunction>
545 : : {
546 : : /** A "super" type, like in Java, for easy reference below. */
547 : : typedef std::unordered_map<NodeValue*, uint64_t, AttrBoolHashFunction> super;
548 : :
549 : : /**
550 : : * BitAccessor allows us to return a bit "by reference." Of course,
551 : : * we don't require bit-addressibility supported by the system, we
552 : : * do it with a complex type.
553 : : */
554 : : class BitAccessor
555 : : {
556 : : uint64_t& d_word;
557 : :
558 : : uint64_t d_bit;
559 : :
560 : : public:
561 : 211394549 : BitAccessor(uint64_t& word, uint64_t bit) : d_word(word), d_bit(bit) {}
562 : :
563 : 211394549 : BitAccessor& operator=(bool b)
564 : : {
565 [ + + ]: 211394549 : if (b)
566 : : {
567 : : // set the bit
568 : 189397239 : d_word |= GetBitSet(d_bit);
569 : : }
570 : : else
571 : : {
572 : : // clear the bit
573 : 21997310 : d_word &= ~GetBitSet(d_bit);
574 : : }
575 : :
576 : 211394549 : return *this;
577 : : }
578 : :
579 : : operator bool() const { return (d_word & GetBitSet(d_bit)) ? true : false; }
580 : : }; /* class AttrHash<bool>::BitAccessor */
581 : :
582 : : /**
583 : : * A (somewhat degenerate) iterator over boolean-valued attributes.
584 : : * This iterator doesn't support anything except comparison and
585 : : * dereference. It's intended just for the result of find() on the
586 : : * table.
587 : : */
588 : : class BitIterator
589 : : {
590 : : std::pair<NodeValue* const, uint64_t>* d_entry;
591 : :
592 : : uint64_t d_bit;
593 : :
594 : : public:
595 : : BitIterator() : d_entry(nullptr), d_bit(0) {}
596 : :
597 : : BitIterator(std::pair<NodeValue* const, uint64_t>& entry, uint64_t bit)
598 : : : d_entry(&entry), d_bit(bit)
599 : : {
600 : : }
601 : :
602 : : std::pair<NodeValue* const, BitAccessor> operator*()
603 : : {
604 : : return std::make_pair(d_entry->first,
605 : : BitAccessor(d_entry->second, d_bit));
606 : : }
607 : :
608 : : bool operator==(const BitIterator& b)
609 : : {
610 : : return d_entry == b.d_entry && d_bit == b.d_bit;
611 : : }
612 : : }; /* class AttrHash<bool>::BitIterator */
613 : :
614 : : /**
615 : : * A (somewhat degenerate) const_iterator over boolean-valued
616 : : * attributes. This const_iterator doesn't support anything except
617 : : * comparison and dereference. It's intended just for the result of
618 : : * find() on the table.
619 : : */
620 : : class ConstBitIterator
621 : : {
622 : : const std::pair<NodeValue* const, uint64_t>* d_entry;
623 : :
624 : : uint64_t d_bit;
625 : :
626 : : public:
627 : 2132707931 : ConstBitIterator() : d_entry(nullptr), d_bit(0) {}
628 : :
629 : 1890956907 : ConstBitIterator(const std::pair<NodeValue* const, uint64_t>& entry,
630 : : uint64_t bit)
631 : 1890956907 : : d_entry(&entry), d_bit(bit)
632 : : {
633 : 1890956907 : }
634 : :
635 : 1890956907 : std::pair<NodeValue* const, bool> operator*()
636 : : {
637 : 3781913814 : return std::make_pair(
638 : 1890956907 : d_entry->first, (d_entry->second & GetBitSet(d_bit)) ? true : false);
639 : : }
640 : :
641 : 2011832419 : bool operator==(const ConstBitIterator& b)
642 : : {
643 [ + + ][ + - ]: 2011832419 : return d_entry == b.d_entry && d_bit == b.d_bit;
644 : : }
645 : : }; /* class AttrHash<bool>::ConstBitIterator */
646 : :
647 : : public:
648 : : typedef std::pair<uint64_t, NodeValue*> key_type;
649 : : typedef bool data_type;
650 : : typedef std::pair<const key_type, data_type> value_type;
651 : :
652 : : /** an iterator type; see above for limitations */
653 : : typedef BitIterator iterator;
654 : : /** a const_iterator type; see above for limitations */
655 : : typedef ConstBitIterator const_iterator;
656 : :
657 : : /**
658 : : * Find the boolean value in the hash table. Returns something ==
659 : : * end() if not found.
660 : : */
661 : : BitIterator find(const std::pair<uint64_t, NodeValue*>& k)
662 : : {
663 : : super::iterator i = super::find(k.second);
664 : : if (i == super::end())
665 : : {
666 : : return BitIterator();
667 : : }
668 : : /*
669 : : Trace.printf("boolattr",
670 : : "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
671 : : &(*i).second,
672 : : (uint64_t)((*i).second),
673 : : uint64_t(k.first));
674 : : */
675 : : return BitIterator(*i, k.first);
676 : : }
677 : :
678 : : /** The "off the end" iterator */
679 : : BitIterator end() { return BitIterator(); }
680 : :
681 : : /**
682 : : * Find the boolean value in the hash table. Returns something ==
683 : : * end() if not found.
684 : : */
685 : 2011832419 : ConstBitIterator find(const std::pair<uint64_t, NodeValue*>& k) const
686 : : {
687 : 2011832419 : super::const_iterator i = super::find(k.second);
688 [ + + ]: 2011832419 : if (i == super::end())
689 : : {
690 : 120875512 : return ConstBitIterator();
691 : : }
692 : : /*
693 : : Trace.printf("boolattr",
694 : : "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
695 : : &(*i).second,
696 : : (uint64_t)((*i).second),
697 : : uint64_t(k.first));
698 : : */
699 : 1890956907 : return ConstBitIterator(*i, k.first);
700 : : }
701 : :
702 : : /** The "off the end" const_iterator */
703 : 2011832419 : ConstBitIterator end() const { return ConstBitIterator(); }
704 : :
705 : : /**
706 : : * Access the hash table using the underlying operator[]. Inserts
707 : : * the key into the table (associated to default value) if it's not
708 : : * already there.
709 : : */
710 : 211394549 : BitAccessor operator[](const std::pair<uint64_t, NodeValue*>& k)
711 : : {
712 : 211394549 : uint64_t& word = super::operator[](k.second);
713 : 211394549 : return BitAccessor(word, k.first);
714 : : }
715 : :
716 : : /**
717 : : * Delete all flags from the given node.
718 : : */
719 : 167163182 : void erase(NodeValue* nv) { super::erase(nv); }
720 : :
721 : : /**
722 : : * Clear the hash table.
723 : : */
724 : 72698 : void clear() { super::clear(); }
725 : :
726 : : /** Is the hash table empty? */
727 : : bool empty() const { return super::empty(); }
728 : :
729 : : /** This is currently very misleading! */
730 : : size_t size() const { return super::size(); }
731 : : }; /* class AttrHash<bool> */
732 : :
733 : : } // namespace attr
734 : :
735 : : // ATTRIBUTE IDENTIFIER ASSIGNMENT TEMPLATE ====================================
736 : :
737 : : namespace attr {
738 : :
739 : : /**
740 : : * This is the last-attribute-assigner. IDs are not globally
741 : : * unique; rather, they are unique for each table_value_type.
742 : : */
743 : : template <class T>
744 : : struct LastAttributeId
745 : : {
746 : : public:
747 : 3370991 : static uint64_t getNextId()
748 : : {
749 : 3370991 : uint64_t* id = raw_id();
750 : 3370991 : const uint64_t next_id = *id;
751 : 3370991 : ++(*id);
752 : 3370991 : return next_id;
753 : : }
754 : 3 : static uint64_t getId() { return *raw_id(); }
755 : :
756 : : private:
757 : 3370994 : static uint64_t* raw_id()
758 : : {
759 : : static uint64_t s_id = 0;
760 : 3370994 : return &s_id;
761 : : }
762 : : };
763 : :
764 : : } // namespace attr
765 : :
766 : : // ATTRIBUTE DEFINITION ========================================================
767 : :
768 : : /**
769 : : * An "attribute type" structure.
770 : : *
771 : : * @param T the tag for the attribute kind.
772 : : *
773 : : * @param value_t the underlying value_type for the attribute kind
774 : : */
775 : : template <class T, class value_t>
776 : : class Attribute
777 : : {
778 : : /**
779 : : * The unique ID associated to this attribute. Assigned statically,
780 : : * at load time.
781 : : */
782 : : static const uint64_t s_id;
783 : :
784 : : public:
785 : : /** The value type for this attribute. */
786 : : typedef value_t value_type;
787 : :
788 : : /** Get the unique ID associated to this attribute. */
789 : 3544907156 : static inline uint64_t getId() { return s_id; }
790 : :
791 : : /**
792 : : * This attribute does not have a default value: calling
793 : : * hasAttribute() for a Node that hasn't had this attribute set will
794 : : * return false, and getAttribute() for the Node will return a
795 : : * default-constructed value_type.
796 : : */
797 : : static const bool has_default_value = false;
798 : :
799 : : /**
800 : : * Register this attribute kind and check that the ID is a valid ID
801 : : * for bool-valued attributes. Fail an assert if not. Otherwise
802 : : * return the id.
803 : : */
804 : 2365605 : static inline uint64_t registerAttribute()
805 : : {
806 : : typedef
807 : : typename attr::KindValueToTableValueMapping<value_t>::table_value_type
808 : : table_value_type;
809 : 2365605 : return attr::LastAttributeId<table_value_type>::getNextId();
810 : : }
811 : : }; /* class Attribute<> */
812 : :
813 : : /**
814 : : * An "attribute type" structure for boolean flags (special).
815 : : */
816 : : template <class T>
817 : : class Attribute<T, bool>
818 : : {
819 : : /** IDs for bool-valued attributes are actually bit assignments. */
820 : : static const uint64_t s_id;
821 : :
822 : : public:
823 : : /** The value type for this attribute; here, bool. */
824 : : typedef bool value_type;
825 : :
826 : : /** Get the unique ID associated to this attribute. */
827 : 2223226968 : static inline uint64_t getId() { return s_id; }
828 : :
829 : : /**
830 : : * Such bool-valued attributes ("flags") have a default value: they
831 : : * are false for all nodes on entry. Calling hasAttribute() for a
832 : : * Node that hasn't had this attribute set will return true, and
833 : : * getAttribute() for the Node will return the default_value below.
834 : : */
835 : : static const bool has_default_value = true;
836 : :
837 : : /**
838 : : * Default value of the attribute for Nodes without one explicitly
839 : : * set.
840 : : */
841 : : static const bool default_value = false;
842 : :
843 : : /**
844 : : * Register this attribute kind and check that the ID is a valid ID
845 : : * for bool-valued attributes. Fail an assert if not. Otherwise
846 : : * return the id.
847 : : */
848 : 1005386 : static inline uint64_t registerAttribute()
849 : : {
850 : 1005386 : const uint64_t id = attr::LastAttributeId<bool>::getNextId();
851 [ - + ][ - + ]: 1005386 : AlwaysAssert(id <= 63) << "Too many boolean node attributes registered "
[ - - ]
852 : : "during initialization !";
853 : 1005386 : return id;
854 : : }
855 : : }; /* class Attribute<..., bool, ...> */
856 : :
857 : : // ATTRIBUTE IDENTIFIER ASSIGNMENT =============================================
858 : :
859 : : /** Assign unique IDs to attributes at load time. */
860 : : template <class T, class value_t>
861 : : const uint64_t Attribute<T, value_t>::s_id =
862 : : Attribute<T, value_t>::registerAttribute();
863 : :
864 : : /** Assign unique IDs to attributes at load time. */
865 : : template <class T>
866 : : const uint64_t Attribute<T, bool>::s_id =
867 : : Attribute<T, bool>::registerAttribute();
868 : :
869 : : } // namespace expr
870 : : } // namespace cvc5::internal
871 : :
872 : : #endif /* CVC5__EXPR__ATTRIBUTE_INTERNALS_H */
|
