CIRCT 23.0.0git
Loading...
Searching...
No Matches
SynthOps.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
16#include "mlir/Analysis/TopologicalSortUtils.h"
17#include "mlir/IR/BuiltinAttributes.h"
18#include "mlir/IR/Matchers.h"
19#include "mlir/IR/OpDefinition.h"
20#include "mlir/IR/PatternMatch.h"
21#include "mlir/IR/Value.h"
22#include "llvm/ADT/APInt.h"
23#include "llvm/ADT/SmallVector.h"
24#include "llvm/Support/Casting.h"
25#include "llvm/Support/LogicalResult.h"
26
27using namespace mlir;
28using namespace circt;
29using namespace circt::synth;
30using namespace circt::synth::aig;
31using namespace circt::comb;
32using namespace matchers;
33
34#define GET_OP_CLASSES
35#include "circt/Dialect/Synth/Synth.cpp.inc"
36
37namespace {
38
39inline llvm::KnownBits applyInversion(llvm::KnownBits value, bool inverted) {
40 if (inverted)
41 std::swap(value.Zero, value.One);
42 return value;
43}
44
45template <typename SubType>
46struct ComplementMatcher {
47 SubType lhs;
48 ComplementMatcher(SubType lhs) : lhs(std::move(lhs)) {}
49 bool match(Operation *op) {
50 auto boolOp = dyn_cast<BooleanLogicOpInterface>(op);
51 return boolOp && boolOp.getInputs().size() == 1 && boolOp.isInverted(0) &&
52 lhs.match(op->getOperand(0));
53 }
54};
55
56template <typename SubType>
57static inline ComplementMatcher<SubType> m_Complement(const SubType &subExpr) {
58 return ComplementMatcher<SubType>(subExpr);
59}
60
61} // namespace
62
63LogicalResult ChoiceOp::verify() {
64 if (getNumOperands() < 1)
65 return emitOpError("requires at least one operand");
66 return success();
67}
68
69OpFoldResult ChoiceOp::fold(FoldAdaptor adaptor) {
70 if (adaptor.getInputs().size() == 1)
71 return getOperand(0);
72 return {};
73}
74
75// Canonicalize a network of synth.choice operations by computing their
76// transitive closure and flattening them into a single choice operation.
77// This merges nested choices and deduplicates shared operands.
78// Pattern matched:
79// %0 = synth.choice %x, %y, %z
80// %1 = synth.choice %0, %u
81// %2 = synth.choice %z, %v
82// =>
83// %merged = synth.choice %x, %y, %z, %u, %v
84LogicalResult ChoiceOp::canonicalize(ChoiceOp op, PatternRewriter &rewriter) {
85 llvm::SetVector<Value> worklist;
87
88 auto addToWorklist = [&](ChoiceOp choice) -> bool {
89 if (choice->getBlock() == op->getBlock() && visitedChoices.insert(choice)) {
90 worklist.insert(choice.getInputs().begin(), choice.getInputs().end());
91 return true;
92 }
93 return false;
94 };
95
96 addToWorklist(op);
97
98 bool mergedOtherChoices = false;
99
100 // Look up and down at definitions and users.
101 for (unsigned i = 0; i < worklist.size(); ++i) {
102 Value val = worklist[i];
103 if (auto defOp = val.getDefiningOp<synth::ChoiceOp>()) {
104
105 if (addToWorklist(defOp))
106 mergedOtherChoices = true;
107 }
108
109 for (Operation *user : val.getUsers()) {
110 if (auto userChoice = llvm::dyn_cast<synth::ChoiceOp>(user)) {
111 if (addToWorklist(userChoice)) {
112 mergedOtherChoices = true;
113 }
114 }
115 }
116 }
117
118 llvm::SmallVector<mlir::Value> finalOperands;
119 for (Value v : worklist) {
120 if (!visitedChoices.contains(v.getDefiningOp())) {
121 finalOperands.push_back(v);
122 }
123 }
124
125 if (!mergedOtherChoices && finalOperands.size() == op.getInputs().size())
126 return llvm::failure();
127
128 auto newChoice = synth::ChoiceOp::create(rewriter, op->getLoc(), op.getType(),
129 finalOperands);
130 for (Operation *visited : visitedChoices.takeVector())
131 rewriter.replaceOp(visited, newChoice);
132
133 for (auto value : newChoice.getInputs())
134 rewriter.replaceAllUsesExcept(value, newChoice.getResult(), newChoice);
135
136 return success();
137}
138
139//===----------------------------------------------------------------------===//
140// AndInverterOp
141//===----------------------------------------------------------------------===//
142
143bool AndInverterOp::areInputsPermutationInvariant() { return true; }
144
145OpFoldResult AndInverterOp::fold(FoldAdaptor adaptor) {
146 if (getNumOperands() == 1 && !isInverted(0))
147 return getOperand(0);
148
149 auto inputs = adaptor.getInputs();
150 if (inputs.size() == 2)
151 if (auto intAttr = dyn_cast_or_null<IntegerAttr>(inputs[1])) {
152 auto value = intAttr.getValue();
153 if (isInverted(1))
154 value = ~value;
155 if (value.isZero())
156 return IntegerAttr::get(
157 IntegerType::get(getContext(), value.getBitWidth()), value);
158 if (value.isAllOnes()) {
159 if (isInverted(0))
160 return {};
161
162 return getOperand(0);
163 }
164 }
165 return {};
166}
167
168LogicalResult AndInverterOp::canonicalize(AndInverterOp op,
169 PatternRewriter &rewriter) {
171 SmallVector<Value> uniqueValues;
172 SmallVector<bool> uniqueInverts;
173
174 APInt constValue =
175 APInt::getAllOnes(op.getResult().getType().getIntOrFloatBitWidth());
176
177 bool invertedConstFound = false;
178 bool flippedFound = false;
179
180 for (auto [value, inverted] : llvm::zip(op.getInputs(), op.getInverted())) {
181 bool newInverted = inverted;
182 if (auto constOp = value.getDefiningOp<hw::ConstantOp>()) {
183 if (inverted) {
184 constValue &= ~constOp.getValue();
185 invertedConstFound = true;
186 } else {
187 constValue &= constOp.getValue();
188 }
189 continue;
190 }
191
192 if (auto andInverterOp = value.getDefiningOp<synth::aig::AndInverterOp>()) {
193 if (andInverterOp.getInputs().size() == 1 &&
194 andInverterOp.isInverted(0)) {
195 value = andInverterOp.getOperand(0);
196 newInverted = andInverterOp.isInverted(0) ^ inverted;
197 flippedFound = true;
198 }
199 }
200
201 auto it = seen.find(value);
202 if (it == seen.end()) {
203 seen.insert({value, newInverted});
204 uniqueValues.push_back(value);
205 uniqueInverts.push_back(newInverted);
206 } else if (it->second != newInverted) {
207 // replace with const 0
208 rewriter.replaceOpWithNewOp<hw::ConstantOp>(
209 op, APInt::getZero(value.getType().getIntOrFloatBitWidth()));
210 return success();
211 }
212 }
213
214 // If the constant is zero, we can just replace with zero.
215 if (constValue.isZero()) {
216 rewriter.replaceOpWithNewOp<hw::ConstantOp>(op, constValue);
217 return success();
218 }
219
220 // No change.
221 if ((uniqueValues.size() == op.getInputs().size() && !flippedFound) ||
222 (!constValue.isAllOnes() && !invertedConstFound &&
223 uniqueValues.size() + 1 == op.getInputs().size()))
224 return failure();
225
226 if (!constValue.isAllOnes()) {
227 auto constOp = hw::ConstantOp::create(rewriter, op.getLoc(), constValue);
228 uniqueInverts.push_back(false);
229 uniqueValues.push_back(constOp);
230 }
231
232 // It means the input is reduced to all ones.
233 if (uniqueValues.empty()) {
234 rewriter.replaceOpWithNewOp<hw::ConstantOp>(op, constValue);
235 return success();
236 }
237
238 // build new op with reduced input values
239 replaceOpWithNewOpAndCopyNamehint<synth::aig::AndInverterOp>(
240 rewriter, op, uniqueValues, uniqueInverts);
241 return success();
242}
243
244APInt AndInverterOp::evaluateBooleanLogicWithoutInversion(
245 llvm::ArrayRef<APInt> inputs) {
246 assert(!inputs.empty() && "expected non-empty input list");
247 APInt result = APInt::getAllOnes(inputs.front().getBitWidth());
248 for (const APInt &input : inputs)
249 result &= input;
250 return result;
251}
252
253bool AndInverterOp::supportsNumInputs(unsigned numInputs) {
254 return numInputs >= 1;
255}
256
257llvm::KnownBits AndInverterOp::computeKnownBits(
258 llvm::function_ref<const llvm::KnownBits &(unsigned)> getInputKnownBits) {
259 assert(getNumOperands() > 0 && "Expected non-empty input list");
260
261 auto width = getInputKnownBits(0).getBitWidth();
262 llvm::KnownBits result(width);
263 result.One = APInt::getAllOnes(width);
264 result.Zero = APInt::getZero(width);
265
266 for (auto [i, inverted] : llvm::enumerate(getInverted()))
267 result &= applyInversion(getInputKnownBits(i), inverted);
268
269 return result;
270}
271
272int64_t AndInverterOp::getLogicDepthCost() {
273 return llvm::Log2_64_Ceil(getNumOperands());
274}
275
276std::optional<uint64_t> AndInverterOp::getLogicAreaCost() {
277 int64_t bitWidth = hw::getBitWidth(getType());
278 if (bitWidth < 0)
279 return std::nullopt;
280 return static_cast<uint64_t>(getNumOperands() - 1) * bitWidth;
281}
282
283void AndInverterOp::emitCNFWithoutInversion(
284 int outVar, llvm::ArrayRef<int> inputVars,
285 llvm::function_ref<void(llvm::ArrayRef<int>)> addClause,
286 llvm::function_ref<int()> newVar) {
287 (void)newVar;
288 circt::addAndClauses(outVar, inputVars, addClause);
289}
290
291//===----------------------------------------------------------------------===//
292// XorInverterOp
293//===----------------------------------------------------------------------===//
294
295bool XorInverterOp::areInputsPermutationInvariant() { return true; }
296
297OpFoldResult XorInverterOp::fold(FoldAdaptor adaptor) {
298 // xor_inv(a) -> a
299 if (getNumOperands() == 1 && !isInverted(0))
300 return getOperand(0);
301
302 auto inputs = adaptor.getInputs();
303 if (inputs.size() == 2)
304 if (auto intAttr = dyn_cast_or_null<IntegerAttr>(inputs[1])) {
305 auto value = intAttr.getValue();
306 if (isInverted(1))
307 value = ~value;
308 // xor_inv(a, 0000000) -> a
309 if (value.isZero())
310 return getOperand(0);
311 }
312 return {};
313}
314
315LogicalResult XorInverterOp::canonicalize(XorInverterOp op,
316 PatternRewriter &rewriter) {
317
318 // Map to store active (non-canceled) operands and their inversion state
319 SmallMapVector<Value, bool, 4> activeOperands;
320
321 // XOR identity is zero; accumulate all constant operands here.
322 APInt constValue =
323 APInt::getZero(op.getResult().getType().getIntOrFloatBitWidth());
324
325 bool constFound = false;
326 bool changed = false;
327
328 for (auto [value, inverted] : llvm::zip(op.getInputs(), op.getInverted())) {
329 Value currentValue = value;
330 bool newInverted = inverted;
331
332 // xor_inv(a, c0, c1) -> xor_inv(a, c0 ^ c1)
333 // xor_inv(a, not c0) -> xor_inv(a, ~c0)
334 if (auto constOp = currentValue.getDefiningOp<hw::ConstantOp>()) {
335 APInt val = constOp.getValue();
336 if (newInverted)
337 val = ~val;
338 constValue ^= val;
339 constFound = true;
340 continue;
341 }
342
343 // xor_inv(a, not (xor_inv/aig_inv not b)) -> xor_inv(a, b)
344 Value matchedVal;
345 if (newInverted &&
346 matchPattern(currentValue, m_Complement(m_Any(&matchedVal)))) {
347 currentValue = matchedVal;
348 newInverted = false; // double inversion cancels out
349 changed = true;
350 }
351
352 // xor_inv (a, a, b) -> b
353 // xor_inv (a, not a, b) -> ~b
354 if (activeOperands.count(currentValue)) {
355 // If we see the value again, they cancel out.
356 // If one was inverted and the other wasn't (x ^ ~x), it results in a '1'.
357 if (activeOperands[currentValue] != newInverted)
358 constValue.flipAllBits();
359 activeOperands.erase(currentValue);
360 changed = true;
361 } else {
362 activeOperands[currentValue] = newInverted;
363 }
364 }
365
366 // No constants were folded and no operands cancelled out. There is nothing to
367 // do.
368 if (!changed && !constFound && activeOperands.size() == op.getInputs().size())
369 return failure();
370
371 // xor_inv(a, 1111111) -> xor_inv(not a)
372 // xor_inv(a, c0, c1) -> xor_inv(a, c0^c1)
373 if (!constValue.isZero()) {
374 if (constValue.isAllOnes() && !activeOperands.empty()) {
375 // Propagate ones as an inversion on the last operand.
376 activeOperands.back().second = !activeOperands.back().second;
377 } else {
378 if (op.getInputs().size() == 2 && !op.getInverted()[1] &&
379 activeOperands.size() == 1)
380 return failure();
381 auto constOp = hw::ConstantOp::create(rewriter, op.getLoc(), constValue);
382 activeOperands.insert({constOp, false});
383 }
384 }
385
386 if (activeOperands.empty()) {
387 rewriter.replaceOpWithNewOp<hw::ConstantOp>(
388 op, APInt::getZero(op.getResult().getType().getIntOrFloatBitWidth()));
389 return success();
390 }
391
392 replaceOpAndCopyNamehint(rewriter, op,
393 XorInverterOp::create(rewriter, op.getLoc(),
394 activeOperands.getArrayRef()));
395 return success();
396}
397
398APInt XorInverterOp::evaluateBooleanLogicWithoutInversion(
399 llvm::ArrayRef<APInt> inputs) {
400 assert(!inputs.empty() && "expected non-empty input list");
401 APInt result = APInt::getZero(inputs.front().getBitWidth());
402 for (const APInt &input : inputs)
403 result ^= input;
404 return result;
405}
406
407bool XorInverterOp::supportsNumInputs(unsigned numInputs) {
408 return numInputs >= 1;
409}
410
411llvm::KnownBits XorInverterOp::computeKnownBits(
412 llvm::function_ref<const llvm::KnownBits &(unsigned)> getInputKnownBits) {
413 assert(getNumOperands() > 0 && "Expected non-empty input list");
414
415 llvm::KnownBits result(getInputKnownBits(0).getBitWidth());
416 for (auto [i, inverted] : llvm::enumerate(getInverted()))
417 result ^= applyInversion(getInputKnownBits(i), inverted);
418 return result;
419}
420
421int64_t XorInverterOp::getLogicDepthCost() {
422 return llvm::Log2_64_Ceil(getNumOperands());
423}
424
425std::optional<uint64_t> XorInverterOp::getLogicAreaCost() {
426 int64_t bitWidth = hw::getBitWidth(getType());
427 if (bitWidth < 0)
428 return std::nullopt;
429 return static_cast<uint64_t>(getNumOperands() - 1) * bitWidth;
430}
431
432void XorInverterOp::emitCNFWithoutInversion(
433 int outVar, llvm::ArrayRef<int> inputVars,
434 llvm::function_ref<void(llvm::ArrayRef<int>)> addClause,
435 llvm::function_ref<int()> newVar) {
436 circt::addParityClauses(outVar, inputVars, addClause, newVar);
437}
438
439//===----------------------------------------------------------------------===//
440// DotOp
441//===----------------------------------------------------------------------===//
442
443void DotOp::emitCNFWithoutInversion(
444 int outVar, llvm::ArrayRef<int> inputVars,
445 llvm::function_ref<void(llvm::ArrayRef<int>)> addClause,
446 llvm::function_ref<int()> newVar) {
447 assert(inputVars.size() == 3 && "expected one SAT variable per operand");
448 int andVar = newVar();
449 int orVar = newVar();
450 // andVar = x and y
451 circt::addAndClauses(andVar, {inputVars[0], inputVars[1]}, addClause);
452 // orVar = z or andVar
453 circt::addOrClauses(orVar, {inputVars[2], andVar}, addClause);
454 // outVar = x xor orVar
455 circt::addXorClauses(outVar, inputVars[0], orVar, addClause);
456}
457
458//===----------------------------------------------------------------------===//
459// MajorityOp
460//===----------------------------------------------------------------------===//
461
462void MajorityOp::emitCNFWithoutInversion(
463 int outVar, llvm::ArrayRef<int> inputVars,
464 llvm::function_ref<void(llvm::ArrayRef<int>)> addClause,
465 llvm::function_ref<int()> newVar) {
466 assert(inputVars.size() == 3 && "expected exactly three inputs");
467 int ab = newVar();
468 int ac = newVar();
469 int bc = newVar();
470 // ab = a & b
471 circt::addAndClauses(ab, {inputVars[0], inputVars[1]}, addClause);
472 // ac = a & c
473 circt::addAndClauses(ac, {inputVars[0], inputVars[2]}, addClause);
474 // bc = b & c
475 circt::addAndClauses(bc, {inputVars[1], inputVars[2]}, addClause);
476 // out = ab | ac | bc
477 circt::addOrClauses(outVar, {ab, ac, bc}, addClause);
478}
479
481 Location loc, ValueRange operands, ArrayRef<bool> inverts,
482 PatternRewriter &rewriter,
483 llvm::function_ref<Value(Value, bool)> createUnary,
484 llvm::function_ref<Value(Value, Value, bool, bool)> createBinary) {
485 switch (operands.size()) {
486 case 0:
487 assert(0 && "cannot be called with empty operand range");
488 break;
489 case 1:
490 return inverts[0] ? createUnary(operands[0], true) : operands[0];
491 case 2:
492 return createBinary(operands[0], operands[1], inverts[0], inverts[1]);
493 default:
494 auto firstHalf = operands.size() / 2;
495 auto lhs = lowerVariadicInvertibleOp(loc, operands.take_front(firstHalf),
496 inverts.take_front(firstHalf),
497 rewriter, createUnary, createBinary);
498 auto rhs = lowerVariadicInvertibleOp(loc, operands.drop_front(firstHalf),
499 inverts.drop_front(firstHalf),
500 rewriter, createUnary, createBinary);
501 return createBinary(lhs, rhs, false, false);
502 }
503 return Value();
504}
505
506template <typename OpTy>
508 PatternRewriter &rewriter) {
509 if (op.getInputs().size() <= 2)
510 return failure();
511 auto result = lowerVariadicInvertibleOp(
512 op.getLoc(), op.getOperands(), op.getInverted(), rewriter,
513 [&](Value input, bool invert) {
514 return OpTy::create(rewriter, op.getLoc(), input, invert);
515 },
516 [&](Value lhs, Value rhs, bool invertLhs, bool invertRhs) {
517 return OpTy::create(rewriter, op.getLoc(), lhs, rhs, invertLhs,
518 invertRhs);
519 });
520 replaceOpAndCopyNamehint(rewriter, op, result);
521 return success();
522}
523
525 RewritePatternSet &patterns) {
526 patterns.add(lowerVariadicAndInverterOpConversion<aig::AndInverterOp>);
527}
528
530 RewritePatternSet &patterns) {
531 patterns.add(lowerVariadicAndInverterOpConversion<XorInverterOp>);
532}
533
534bool circt::synth::isLogicNetworkOp(Operation *op) {
535 return isa<synth::BooleanLogicOpInterface, synth::ChoiceOp, comb::ExtractOp,
536 comb::ReplicateOp, comb::ConcatOp>(op);
537}
538
540 mlir::Operation *op,
541 llvm::function_ref<bool(mlir::Value, mlir::Operation *)> isOperandReady) {
542 // Sort the operations topologically
543 auto walkResult = op->walk([&](Region *region) {
544 auto regionKindOp =
545 dyn_cast<mlir::RegionKindInterface>(region->getParentOp());
546 if (!regionKindOp ||
547 regionKindOp.hasSSADominance(region->getRegionNumber()))
548 return WalkResult::advance();
549
550 // Graph region.
551 for (auto &block : *region) {
552 if (!mlir::sortTopologically(&block, isOperandReady))
553 return WalkResult::interrupt();
554 }
555 return WalkResult::advance();
556 });
557
558 return success(!walkResult.wasInterrupted());
559}
560
561//===----------------------------------------------------------------------===//
562// OneHotOp
563//===----------------------------------------------------------------------===//
564
565void OneHotOp::emitCNFWithoutInversion(
566 int outVar, llvm::ArrayRef<int> inputVars,
567 llvm::function_ref<void(llvm::ArrayRef<int>)> addClause,
568 llvm::function_ref<int()> newVar) {
569 assert(inputVars.size() == 3 && "expected exactly three inputs");
570
571 // parity = a ^ b ^ c.
572 int parity = newVar();
573 circt::addParityClauses(parity, inputVars, addClause, newVar);
574
575 // allSet = a & b & c.
576 int allSet = newVar();
577 circt::addAndClauses(allSet, inputVars, addClause);
578
579 // out = (a ^ b ^ c) & ~(a & b & c).
580 circt::addAndClauses(outVar, {parity, -allSet}, addClause);
581}
582
583//===----------------------------------------------------------------------===//
584// MuxInverterOp
585//===----------------------------------------------------------------------===//
586
587void MuxInverterOp::emitCNFWithoutInversion(
588 int outVar, llvm::ArrayRef<int> inputVars,
589 llvm::function_ref<void(llvm::ArrayRef<int>)> addClause,
590 llvm::function_ref<int()> newVar) {
591 assert(inputVars.size() == 3 && "expected exactly three inputs");
592
593 int cond = inputVars[0];
594 int trueValue = inputVars[1];
595 int falseValue = inputVars[2];
596
597 int lhs = newVar();
598 int rhs = newVar();
599
600 // lhs = cond & trueValue
601 circt::addAndClauses(lhs, {cond, trueValue}, addClause);
602 // rhs = ~cond & falseValue
603 circt::addAndClauses(rhs, {-cond, falseValue}, addClause);
604 // out = lhs | rhs
605 circt::addOrClauses(outVar, {lhs, rhs}, addClause);
606}
607
608//===----------------------------------------------------------------------===//
609// GambleOp
610//===----------------------------------------------------------------------===//
611
612void GambleOp::emitCNFWithoutInversion(
613 int outVar, llvm::ArrayRef<int> inputVars,
614 llvm::function_ref<void(llvm::ArrayRef<int>)> addClause,
615 llvm::function_ref<int()> newVar) {
616 assert(inputVars.size() == 3 && "expected exactly three inputs");
617
618 // allSet = a & b & c
619 int allSet = newVar();
620 circt::addAndClauses(allSet, inputVars, addClause);
621
622 // orSet = a | b | c
623 int orSet = newVar();
624 circt::addOrClauses(orSet, inputVars, addClause);
625
626 // out = allSet | ~orSet
627 circt::addOrClauses(outVar, {allSet, -orSet}, addClause);
628}
assert(baseType &&"element must be base type")
static ComplementMatcher< SubType > m_Complement(const SubType &subExpr)
Definition CombFolds.cpp:85
LogicalResult lowerVariadicAndInverterOpConversion(OpTy op, PatternRewriter &rewriter)
Definition SynthOps.cpp:507
static Value lowerVariadicInvertibleOp(Location loc, ValueRange operands, ArrayRef< bool > inverts, PatternRewriter &rewriter, llvm::function_ref< Value(Value, bool)> createUnary, llvm::function_ref< Value(Value, Value, bool, bool)> createBinary)
Definition SynthOps.cpp:480
create(data_type, value)
Definition hw.py:433
int64_t getBitWidth(mlir::Type type)
Return the hardware bit width of a type.
Definition HWTypes.cpp:110
void populateVariadicXorInverterLoweringPatterns(mlir::RewritePatternSet &patterns)
LogicalResult topologicallySortGraphRegionBlocks(mlir::Operation *op, llvm::function_ref< bool(mlir::Value, mlir::Operation *)> isOperandReady)
This function performs a topological sort on the operations within each block of graph regions in the...
Definition SynthOps.cpp:539
bool isLogicNetworkOp(mlir::Operation *op)
void populateVariadicAndInverterLoweringPatterns(mlir::RewritePatternSet &patterns)
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.
void addAndClauses(int outVar, llvm::ArrayRef< int > inputLits, llvm::function_ref< void(llvm::ArrayRef< int >)> addClause)
Emit clauses encoding outVar <=> and(inputLits).
void addXorClauses(int outVar, int lhsLit, int rhsLit, llvm::function_ref< void(llvm::ArrayRef< int >)> addClause)
Emit clauses encoding outVar <=> (lhsLit xor rhsLit).
void replaceOpAndCopyNamehint(PatternRewriter &rewriter, Operation *op, Value newValue)
A wrapper of PatternRewriter::replaceOp to propagate "sv.namehint" attribute.
Definition Naming.cpp:73
void addOrClauses(int outVar, llvm::ArrayRef< int > inputLits, llvm::function_ref< void(llvm::ArrayRef< int >)> addClause)
Emit clauses encoding outVar <=> or(inputLits).
void addParityClauses(int outVar, llvm::ArrayRef< int > inputLits, llvm::function_ref< void(llvm::ArrayRef< int >)> addClause, llvm::function_ref< int()> newVar)
Emit clauses encoding outVar <=> parity(inputLits).