Loading [MathJax]/extensions/tex2jax.js
CIRCT 21.0.0git
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
DNF.cpp
Go to the documentation of this file.
1//===----------------------------------------------------------------------===//
2//
3// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4// See https://llvm.org/LICENSE.txt for license information.
5// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6//
7//===----------------------------------------------------------------------===//
8
9#include "DNF.h"
10#include "mlir/IR/OperationSupport.h"
11
12using namespace mlir;
13using namespace circt;
14using namespace llhd;
15using llvm::SmallMapVector;
16
17//===----------------------------------------------------------------------===//
18// Utilities
19//===----------------------------------------------------------------------===//
20
21/// Insert an item into something like a vector, maintaining the vector in
22/// sorted order and removing any duplicates.
23template <typename Container, typename Item>
24static bool insertUniqued(Container &container, Item item) {
25 auto it = llvm::lower_bound(container, item);
26 if (it != container.end() && *it == item)
27 return false;
28 container.insert(it, std::move(item));
29 return true;
30}
31
32/// Check whether a container is sorted and contains only unique items.
33template <typename Container>
34static bool isUniqued(Container &container) {
35 if (container.size() < 2)
36 return true;
37 auto it = container.begin();
38 auto prev = it++;
39 auto end = container.end();
40 for (; it != end; ++it, ++prev)
41 if (!(*prev < *it))
42 return false;
43 return true;
44}
45
46//===----------------------------------------------------------------------===//
47// AndTerm
48//===----------------------------------------------------------------------===//
49
50int AndTerm::compare(const AndTerm other) const {
51 if (value.getAsOpaquePointer() < other.value.getAsOpaquePointer())
52 return -1;
53 if (value.getAsOpaquePointer() > other.value.getAsOpaquePointer())
54 return 1;
55 if (uses.to_ulong() < other.uses.to_ulong())
56 return -1;
57 if (uses.to_ulong() > other.uses.to_ulong())
58 return 1;
59 return 0;
60}
61
62bool AndTerm::isSubsetOf(const AndTerm &other) const {
63 if (value != other.value)
64 return false;
65 return (uses & other.uses) == other.uses;
66}
67
69 Use &flippedUse) const {
70 if (value != other.value)
71 return 2; // not a subset
72
73 // Determine which bits are present in this and the other term. For this to be
74 // a subset of the other term, all other terms must be present in this term.
75 auto thisMask = (uses | (uses << 2) | (uses >> 2));
76 auto otherMask = (other.uses | (other.uses << 2) | (other.uses >> 2));
77 auto mask = thisMask & otherMask;
78 if (mask != otherMask)
79 return 2; // not a subset
80
81 // Determine the terms that are different. If the uses differ only by a
82 // single inverted term, the resulting bit set will have those two bits set:
83 // this = 0011 (Past|Id)
84 // other = 0110 (Past|NotId)
85 // diff = 0101 (Id|NotId)
86 // which = 0001 (Id)
87 auto diff = (uses & mask) ^ (other.uses & mask);
88 if (diff.none())
89 return 0; // identical terms, no flips
90 auto which = diff & (diff >> 2);
91 if (llvm::popcount(diff.to_ulong()) != 2 ||
92 llvm::popcount(which.to_ulong()) != 1)
93 return 2; // more than one flipped term
94 flippedUse = Use(llvm::countr_zero(which.to_ulong()));
95 return 1; // exactly one flipped term
96}
97
98void AndTerm::print(llvm::raw_ostream &os,
99 llvm::function_ref<void(Value)> printValue) const {
100 // Default value printer giving each value and anonymous `vN` name.
101 SmallMapVector<Value, unsigned, 8> valueIds;
102 auto defaultPrintValue = [&](Value value) {
103 os << "v" << valueIds.insert({value, valueIds.size()}).first->second;
104 };
105 if (!printValue)
106 printValue = defaultPrintValue;
107
108 // Duplicate the term, handle posedge/negedge separately, and then print the
109 // remaining terms.
110 auto that = *this;
111 bool needsSeparator = false;
112 if (that.hasAllUses(PosEdgeUses)) {
113 that.removeUses(PosEdgeUses);
114 os << "/";
115 printValue(value);
116 needsSeparator = true;
117 }
118 if (that.hasAllUses(NegEdgeUses)) {
119 that.removeUses(NegEdgeUses);
120 if (needsSeparator)
121 os << "&";
122 os << "\\";
123 printValue(value);
124 needsSeparator = true;
125 }
126 for (unsigned i = 0; i < 4; ++i) {
127 auto use = Use(i);
128 if (that.hasUse(use)) {
129 if (needsSeparator)
130 os << "&";
131 if (use & Not)
132 os << "!";
133 if (use == Past || use == NotPast)
134 os << "@";
135 printValue(value);
136 needsSeparator = true;
137 }
138 }
139}
140
141//===----------------------------------------------------------------------===//
142// OrTerm
143//===----------------------------------------------------------------------===//
144
145bool OrTerm::contains(const AndTerm &andTerm) const {
146 auto it = llvm::lower_bound(andTerms, andTerm);
147 return it != andTerms.end() && *it == andTerm;
148}
149
150int OrTerm::compare(const OrTerm &other) const {
151 auto &a = *this;
152 auto &b = other;
153 if (a.andTerms.size() < b.andTerms.size())
154 return -1;
155 if (a.andTerms.size() > b.andTerms.size())
156 return 1;
157 for (auto [aTerm, bTerm] : llvm::zip(a.andTerms, b.andTerms))
158 if (auto order = aTerm.compare(bTerm); order != 0)
159 return order;
160 return 0;
161}
162
164 unsigned &flippedIdx,
165 AndTerm::Use &flippedUse) const {
166
167 // For `this` to be a subset of `other`, all terms of `other` must be
168 // present in `this`, with `this` potentially containing other terms. So
169 // `this` must at least have as many terms as `other`.
170 if (andTerms.size() < other.andTerms.size())
171 return false;
172
173 // Iterate through the terms in `this` and `other`, and make sure every term
174 // in `other` is present in `this`, and skip terms in `this` that are not
175 // present in `other`.
176 unsigned thisIdx = 0;
177 unsigned otherIdx = 0;
178 bool flipFound = false;
179 while (thisIdx < andTerms.size() && otherIdx < other.andTerms.size()) {
180 auto thisTerm = andTerms[thisIdx];
181 auto otherTerm = other.andTerms[otherIdx];
182 unsigned flips = thisTerm.isSubsetOfModuloSingleFlip(otherTerm, flippedUse);
183 if (flips == 0) {
184 ++thisIdx;
185 ++otherIdx;
186 } else if (flips == 1) {
187 // Catch the case where this is the second flip we find.
188 if (flipFound)
189 return false;
190 flipFound = true;
191 flippedIdx = thisIdx;
192 ++thisIdx;
193 ++otherIdx;
194 } else if (thisTerm < otherTerm) {
195 ++thisIdx;
196 } else {
197 return false;
198 }
199 }
200 return otherIdx == other.andTerms.size() && flipFound;
201}
202
203bool OrTerm::isSubsetOf(const OrTerm &other) const {
204 // For `this` to be a subset of `other`, all terms of `other` must be
205 // present in `this`, with `this` potentially containing other terms. So
206 // `this` must at least have as many terms as `other`.
207 if (andTerms.size() < other.andTerms.size())
208 return false;
209
210 // Iterate through the terms in `this` and `other`, and make sure every term
211 // in `other` is present in `this`, and skip terms in `this` that are not
212 // present in `other`.
213 unsigned thisIdx = 0;
214 unsigned otherIdx = 0;
215 while (thisIdx < andTerms.size() && otherIdx < other.andTerms.size()) {
216 auto thisTerm = andTerms[thisIdx];
217 auto otherTerm = other.andTerms[otherIdx];
218 if (thisTerm.isSubsetOf(otherTerm)) {
219 ++thisIdx;
220 ++otherIdx;
221 } else if (thisTerm < otherTerm) {
222 ++thisIdx;
223 } else {
224 return false;
225 }
226 }
227 return otherIdx == other.andTerms.size();
228}
229
230llvm::hash_code OrTerm::flipInvariantHash() const {
231 auto range = llvm::map_range(andTerms, [](AndTerm andTerm) {
232 // Enable all complementary uses in the term to make the hash invariant
233 // under term flipping.
234 andTerm.uses |= andTerm.uses >> 2;
235 andTerm.uses |= andTerm.uses << 2;
236 return llvm::hash_combine(andTerm.value, andTerm.uses.to_ulong());
237 });
238 return llvm::hash_combine_range(range.begin(), range.end());
239}
240
241static bool compareValueOnly(const AndTerm &a, const AndTerm &b) {
242 return a.value.getAsOpaquePointer() < b.value.getAsOpaquePointer();
243}
244
246 // Try to merge into an existing term with the same value.
247 auto it = llvm::lower_bound(andTerms, term, compareValueOnly);
248 if (it != andTerms.end() && it->value == term.value) {
249 it->addUses(term.uses);
250 return !it->isFalse();
251 }
252
253 // Otherwise insert.
254 andTerms.insert(it, std::move(term));
255 return true;
256}
257
258bool OrTerm::addTerms(ArrayRef<AndTerm> terms) {
259 for (auto term : terms)
260 if (!addTerm(term))
261 return false;
262 return true;
263}
264
266 for (unsigned idx = 0; idx + 1 < andTerms.size(); ++idx)
267 if (andTerms[idx] >= andTerms[idx + 1])
268 return false;
269 for (auto &andTerm : andTerms)
270 if (andTerm.isFalse() || andTerm.isTrue())
271 return false;
272 return true;
273}
274
275std::optional<bool> OrTerm::evaluate(
276 llvm::function_ref<std::optional<bool>(Value, bool)> evaluateTerm) {
277 bool allTrue = true;
278 for (auto &andTerm : andTerms) {
279 for (unsigned use = 0; use < 4; ++use) {
280 if (!andTerm.hasUse(AndTerm::Use(use)))
281 continue;
282 auto result =
283 evaluateTerm(andTerm.value, (use & ~AndTerm::Not) == AndTerm::Past);
284 if (!result) {
285 allTrue = false;
286 continue;
287 }
288 if (use & AndTerm::Not)
289 *result = !*result;
290 if (!*result)
291 return {false};
292 }
293 }
294 if (allTrue)
295 return {true};
296 return {};
297}
298
299void OrTerm::print(llvm::raw_ostream &os,
300 llvm::function_ref<void(Value)> printValue) const {
301 // Handle trivial true.
302 if (isTrue()) {
303 os << "true";
304 return;
305 }
306
307 // Default value printer giving each value and anonymous `vN` name.
308 SmallMapVector<Value, unsigned, 8> valueIds;
309 auto defaultPrintValue = [&](Value value) {
310 os << "v" << valueIds.insert({value, valueIds.size()}).first->second;
311 };
312 if (!printValue)
313 printValue = defaultPrintValue;
314
315 // Print terms.
316 llvm::interleave(
317 andTerms, os, [&](auto andTerm) { andTerm.print(os, printValue); }, "&");
318}
319
320//===----------------------------------------------------------------------===//
321// DNF
322//===----------------------------------------------------------------------===//
323
324bool DNF::contains(const OrTerm &orTerm) const {
325 auto it = llvm::lower_bound(orTerms, orTerm);
326 return it != orTerms.end() && *it == orTerm;
327}
328
329bool DNF::contains(const AndTerm &andTerm) const {
330 for (auto &orTerm : orTerms)
331 if (orTerm.contains(andTerm))
332 return true;
333 return false;
334}
335
336int DNF::compare(const DNF &other) const {
337 auto &a = *this;
338 auto &b = other;
339 if (a.orTerms.size() < b.orTerms.size())
340 return -1;
341 if (a.orTerms.size() > b.orTerms.size())
342 return 1;
343 for (auto [aTerm, bTerm] : llvm::zip(a.orTerms, b.orTerms))
344 if (auto order = aTerm.compare(bTerm); order != 0)
345 return order;
346 return 0;
347}
348
350 for (auto &orTerm : orTerms)
351 if (!orTerm.isSortedAndUnique())
352 return false;
353 for (unsigned idx = 0; idx + 1 < orTerms.size(); ++idx)
354 if (orTerms[idx] >= orTerms[idx + 1])
355 return false;
356 return true;
357}
358
360 // Count the number of distinct input terms.
361 SmallMapVector<std::pair<Value, AndTerm::Use>, uint8_t, 8> terms;
362 for (auto &orTerm : orTerms) {
363 for (auto &andTerm : orTerm.andTerms) {
364 if (andTerm.hasAnyUses(1 << AndTerm::Id | 1 << AndTerm::NotId))
365 terms.insert({{andTerm.value, AndTerm::Id}, uint8_t(terms.size())});
366 if (andTerm.hasAnyUses(1 << AndTerm::Past | 1 << AndTerm::NotPast))
367 terms.insert({{andTerm.value, AndTerm::Past}, uint8_t(terms.size())});
368 if (terms.size() > 16)
369 return;
370 }
371 }
372 unsigned tableSize = 1 << terms.size();
373
374 // Compute the truth table.
375 auto table = APInt::getZero(tableSize);
376 auto getCheckerMask = [&](unsigned idx) {
377 return APInt::getSplat(tableSize,
378 APInt::getHighBitsSet(2 << idx, 1 << idx));
379 };
380 auto getTermMask = [&](Value value, AndTerm::Use use) {
381 return getCheckerMask(terms.lookup({value, use}));
382 };
383 for (auto &orTerm : orTerms) {
384 auto orTable = APInt::getAllOnes(tableSize);
385 for (auto &andTerm : orTerm.andTerms) {
386 if (andTerm.hasUse(AndTerm::Id))
387 orTable &= getTermMask(andTerm.value, AndTerm::Id);
388 if (andTerm.hasUse(AndTerm::NotId))
389 orTable &= ~getTermMask(andTerm.value, AndTerm::Id);
390 if (andTerm.hasUse(AndTerm::Past))
391 orTable &= getTermMask(andTerm.value, AndTerm::Past);
392 if (andTerm.hasUse(AndTerm::NotPast))
393 orTable &= ~getTermMask(andTerm.value, AndTerm::Past);
394 }
395 table |= orTable;
396 }
397
398 // Handle the trivial cases.
399 if (table.isZero()) {
400 orTerms.clear();
401 return;
402 }
403 if (table.isAllOnes()) {
404 orTerms.clear();
405 orTerms.push_back(OrTerm());
406 return;
407 }
408
409 // Convert the truth table back to the corresponding AND and OR terms.
410 OrTerms newTerms;
411 auto remainingBits = table;
412 for (unsigned i = 0; i < 10 && !remainingBits.isZero(); ++i) {
413 unsigned nextIdx = remainingBits.countTrailingZeros();
414 unsigned bestKeeps = -1;
415 auto bestMask = APInt::getZero(tableSize);
416 for (unsigned keeps = 0; keeps < tableSize; ++keeps) {
417 auto mask = APInt::getAllOnes(tableSize);
418 for (unsigned termIdx = 0; termIdx < terms.size(); ++termIdx)
419 if (keeps & (1 << termIdx))
420 mask &= (nextIdx & (1 << termIdx)) ? getCheckerMask(termIdx)
421 : ~getCheckerMask(termIdx);
422 if ((table & mask) == mask &&
423 llvm::popcount(keeps) < llvm::popcount(bestKeeps)) {
424 bestKeeps = keeps;
425 bestMask = mask;
426 }
427 }
428 OrTerm::AndTerms andTerms;
429 for (auto [term, termIdx] : terms) {
430 if (~bestKeeps & (1 << termIdx))
431 continue;
432 unsigned use = term.second;
433 if (~nextIdx & (1 << termIdx))
434 use |= AndTerm::Not;
435 if (!andTerms.empty() && andTerms.back().value == term.first)
436 andTerms.back().addUse(AndTerm::Use(use));
437 else
438 andTerms.push_back(AndTerm(term.first, 1 << use));
439 }
440 llvm::sort(andTerms);
441 newTerms.push_back(OrTerm(std::move(andTerms)));
442 remainingBits &= ~bestMask;
443 }
444
445 llvm::sort(newTerms);
446 orTerms = std::move(newTerms);
447}
448
449std::optional<bool> DNF::evaluate(
450 llvm::function_ref<std::optional<bool>(Value, bool)> evaluateTerm) {
451 bool allFalse = true;
452 for (auto &orTerm : orTerms) {
453 auto result = orTerm.evaluate(evaluateTerm);
454 if (!result) {
455 allFalse = false;
456 continue;
457 }
458 if (*result)
459 return {true};
460 }
461 if (allFalse)
462 return {false};
463 return {};
464}
465
466void DNF::print(llvm::raw_ostream &os,
467 llvm::function_ref<void(Value)> printValue) const {
468 // Handle trivial cases.
469 if (isNull()) {
470 os << "null";
471 return;
472 }
473 if (isFalse()) {
474 os << "false";
475 return;
476 }
477 if (isTrue()) {
478 os << "true";
479 return;
480 }
481
482 // Default value printer giving each value and anonymous `vN` name.
483 SmallMapVector<Value, unsigned, 8> valueIds;
484 auto defaultPrintValue = [&](Value value) {
485 os << "v" << valueIds.insert({value, valueIds.size()}).first->second;
486 };
487 if (!printValue)
488 printValue = defaultPrintValue;
489
490 // Print the terms.
491 llvm::interleave(
492 orTerms, os, [&](auto &orTerm) { orTerm.print(os, printValue); }, " | ");
493}
494
495void DNF::printWithValues(llvm::raw_ostream &os) const {
496 os << "DNF(";
497
498 // Print the DNF itself.
499 SmallMapVector<Value, unsigned, 8> valueIds;
500 print(os, [&](Value value) {
501 auto id = valueIds.insert({value, valueIds.size()}).first->second;
502 os << "v" << id;
503 });
504
505 // Print the values used.
506 if (!valueIds.empty()) {
507 os << " with ";
508 llvm::interleaveComma(valueIds, os, [&](auto valueAndId) {
509 os << "v" << valueAndId.second << " = ";
510 valueAndId.first.printAsOperand(os, OpPrintingFlags());
511 });
512 }
513
514 os << ")";
515}
516
517//===----------------------------------------------------------------------===//
518// OR Operation
519//===----------------------------------------------------------------------===//
520
521DNF DNF::operator|(const DNF &other) const {
522 if (isNull() || other.isNull())
523 return DNF();
524
525 // Handle `true | a -> true`.
526 if (isTrue())
527 return DNF(true);
528
529 // Handle `a | true -> true`.
530 if (other.isTrue())
531 return DNF(true);
532
533 // Handle `false | a -> a`.
534 if (isFalse())
535 return other;
536
537 // Handle `a | false -> a`.
538 if (other.isFalse())
539 return *this;
540
541 // Combine the or terms of the two DNFs, deduplicating them along the way. We
542 // assume that the terms in both DNFs are ordered. That allows us to use a
543 // two-index method to linearly scan through the terms and pick the lower ones
544 // first, ensuring that the merged terms are again ordered.
545 auto result = DNF(false);
546 unsigned thisIdx = 0;
547 unsigned otherIdx = 0;
548 while (thisIdx < orTerms.size() && otherIdx < other.orTerms.size()) {
549 OrTerm nextTerm;
550 auto order = orTerms[thisIdx].compare(other.orTerms[otherIdx]);
551 if (order < 0) {
552 nextTerm = std::move(orTerms[thisIdx++]);
553 } else if (order > 0) {
554 nextTerm = other.orTerms[otherIdx++];
555 } else {
556 ++otherIdx;
557 continue; // don't add duplicates
558 }
559 result.orTerms.push_back(std::move(nextTerm));
560 }
561 for (; thisIdx < orTerms.size(); ++thisIdx)
562 result.orTerms.push_back(std::move(orTerms[thisIdx]));
563 for (; otherIdx < other.orTerms.size(); ++otherIdx)
564 result.orTerms.push_back(other.orTerms[otherIdx]);
565
566 result.optimize();
567 return result;
568}
569
570//===----------------------------------------------------------------------===//
571// AND Operation
572//===----------------------------------------------------------------------===//
573
574DNF DNF::operator&(const DNF &other) const {
575 if (isNull() || other.isNull())
576 return DNF();
577
578 // Handle `false & a -> false`.
579 if (isFalse())
580 return DNF(false);
581
582 // Handle `a & false -> false`.
583 if (other.isFalse())
584 return DNF(false);
585
586 // Handle `true & a -> a`.
587 if (isTrue())
588 return other;
589
590 // Handle `a & true -> a`.
591 if (other.isTrue())
592 return *this;
593
594 // Handle the general case.
595 auto result = DNF(false);
596 for (auto &thisTerm : orTerms) {
597 for (auto &otherTerm : other.orTerms) {
598 auto newTerm = thisTerm;
599 if (newTerm.addTerms(otherTerm.andTerms))
600 insertUniqued(result.orTerms, newTerm);
601 }
602 }
603 assert(result.isSortedAndUnique());
604 result.optimize();
605 return result;
606}
607
608//===----------------------------------------------------------------------===//
609// XOR Operation
610//===----------------------------------------------------------------------===//
611
612DNF DNF::operator^(const DNF &other) const {
613 if (isNull() || other.isNull())
614 return DNF();
615
616 // Handle `a ^ false -> a`.
617 if (isFalse())
618 return other;
619
620 // Handle `false ^ a -> a`.
621 if (other.isFalse())
622 return *this;
623
624 // Handle `a ^ true -> ~a`.
625 if (isTrue())
626 return ~other;
627
628 // Handle `true ^ a -> ~a`.
629 if (other.isTrue())
630 return ~(*this);
631
632 // Otherwise compute a ^ b as (!a&b) | (a&!b).
633 return ~(*this) & other | *this & ~other;
634}
635
636//===----------------------------------------------------------------------===//
637// NOT Operation
638//===----------------------------------------------------------------------===//
639
641 // Handle the trivial cases.
642 if (isNull())
643 return DNF();
644 if (isTrue())
645 return DNF(false);
646 if (isFalse())
647 return DNF(true);
648
649 // Otherwise go through each of the AND terms, negate them individually, and
650 // then AND them into the result. For example:
651 // !(a&b | c&d | e&f)
652 // !(a&b) & !(c&d) & !(e&f)
653 // (!a | !b) & (!c & !d) & (!e & !f)
654 auto result = DNF(true);
655 auto inverted = DNF(false);
656 for (auto &orTerm : orTerms) {
657 // Map `!(a&b&c)` to `(!a | !b | !c)`.
658 for (auto &andTerm : orTerm.andTerms)
659 for (unsigned i = 0; i < 4; ++i)
660 if (andTerm.hasUse(AndTerm::Use(i)))
661 inverted.orTerms.push_back(
662 OrTerm(AndTerm(andTerm.value, 1 << (i ^ AndTerm::Not))));
663 llvm::sort(inverted.orTerms);
664 result &= inverted;
665 inverted.orTerms.clear();
666 }
667 assert(result.isSortedAndUnique());
668 return result;
669}
assert(baseType &&"element must be base type")
static bool isUniqued(Container &container)
Check whether a container is sorted and contains only unique items.
Definition DNF.cpp:34
static bool insertUniqued(Container &container, Item item)
Insert an item into something like a vector, maintaining the vector in sorted order and removing any ...
Definition DNF.cpp:24
static bool compareValueOnly(const AndTerm &a, const AndTerm &b)
Definition DNF.cpp:241
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.
An individual term of an AND expression in a DNF.
Definition DNF.h:20
Use
An integer indicating one use of the value in this term.
Definition DNF.h:24
@ NotPast
The inverted past value !@x.
Definition DNF.h:34
@ Past
The past value @x.
Definition DNF.h:28
@ Id
The plain value x.
Definition DNF.h:26
@ NotId
The inverted value !x.
Definition DNF.h:32
@ Not
The bit that indicates inversion.
Definition DNF.h:30
static constexpr Uses PosEdgeUses
The set of uses that indicates a posedge.
Definition DNF.h:40
Uses uses
The different uses of this value.
Definition DNF.h:51
bool isSubsetOf(const AndTerm &other) const
Check if this term is a subset of another term.
Definition DNF.cpp:62
unsigned isSubsetOfModuloSingleFlip(const AndTerm &other, Use &flippedUse) const
Check if this term is a subset of another term modulo a single flipped term.
Definition DNF.cpp:68
Value value
The value.
Definition DNF.h:49
static constexpr Uses NegEdgeUses
The set of uses that indicates a negedge.
Definition DNF.h:42
int compare(const AndTerm other) const
Compare against another term.
Definition DNF.cpp:50
void print(llvm::raw_ostream &os, llvm::function_ref< void(Value)> printValue={}) const
Print this term to os, using the given callback to print the value.
Definition DNF.cpp:98
OrTerms orTerms
Definition DNF.h:201
DNF operator~() const
Compute the boolean NOT of this DNF.
Definition DNF.cpp:640
DNF()
Construct a null DNF.
Definition DNF.h:204
DNF operator&(const DNF &other) const
Compute the boolean AND of this and another DNF.
Definition DNF.cpp:574
std::optional< bool > evaluate(llvm::function_ref< std::optional< bool >(Value, bool)> evaluateTerm)
Try to evaluate this DNF to a constant true or false value.
Definition DNF.cpp:449
DNF operator|(const DNF &other) const
Compute the boolean OR of this and another DNF.
Definition DNF.cpp:521
void print(llvm::raw_ostream &os, llvm::function_ref< void(Value)> printValue={}) const
Print this DNF to os, using the given callback to print the value.
Definition DNF.cpp:466
int compare(const DNF &other) const
Compare against another DNF.
Definition DNF.cpp:336
bool contains(const OrTerm &orTerm) const
Check if this DNF contains a specific OR term.
Definition DNF.cpp:324
void printWithValues(llvm::raw_ostream &os) const
Print this DNF to os, followed by a list of the concrete values used.
Definition DNF.cpp:495
void optimize()
Removes redundant terms as follows:
Definition DNF.cpp:359
DNF operator^(const DNF &other) const
Compute the boolean XOR of this and another DNF.
Definition DNF.cpp:612
bool isTrue() const
Check whether this DNF is trivially true.
Definition DNF.h:231
bool isNull() const
Check whether this DNF is null.
Definition DNF.h:222
bool isFalse() const
Check whether this DNF is trivially false.
Definition DNF.h:229
bool isSortedAndUnique() const
Check that all terms in the DNF are sorted.
Definition DNF.cpp:349
An individual term of an OR expression in a DNF.
Definition DNF.h:127
llvm::hash_code flipInvariantHash() const
Return a hash code for this term that is invariant to inversion of individual terms.
Definition DNF.cpp:230
void print(llvm::raw_ostream &os, llvm::function_ref< void(Value)> printValue={}) const
Print this term to os, using the given callback to print the value.
Definition DNF.cpp:299
bool isSubsetOfModuloSingleFlip(const OrTerm &other, unsigned &flippedIdx, AndTerm::Use &flippedUse) const
Check if this term is a subset of another term modulo a single flipped term.
Definition DNF.cpp:163
bool contains(const AndTerm &andTerm) const
Check if this OR term contains a specific AND term.
Definition DNF.cpp:145
bool isTrue() const
Check if this term is trivially true.
Definition DNF.h:141
AndTerms andTerms
Definition DNF.h:129
SmallVector< AndTerm, 1 > AndTerms
Definition DNF.h:128
std::optional< bool > evaluate(llvm::function_ref< std::optional< bool >(Value, bool)> evaluateTerm)
Try to evaluate this term to a constant true or false value.
Definition DNF.cpp:275
bool isSubsetOf(const OrTerm &other) const
Check if this term is a subset of another term.
Definition DNF.cpp:203
bool addTerm(AndTerm term)
Add an AndTerm.
Definition DNF.cpp:245
int compare(const OrTerm &other) const
Compare against another term.
Definition DNF.cpp:150
bool isSortedAndUnique() const
Check that all terms in this OrTerm are sorted.
Definition DNF.cpp:265
bool addTerms(ArrayRef< AndTerm > terms)
Add multiple AndTerms.
Definition DNF.cpp:258