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