18 #include "mlir/Dialect/Func/IR/FuncOps.h"
19 #include "mlir/IR/BuiltinOps.h"
20 #include "mlir/Support/IndentedOstream.h"
21 #include "mlir/Tools/mlir-translate/Translation.h"
22 #include "llvm/ADT/ScopedHashTable.h"
23 #include "llvm/ADT/StringRef.h"
24 #include "llvm/Support/Format.h"
25 #include "llvm/Support/raw_ostream.h"
27 using namespace circt;
29 using namespace ExportSMTLIB;
31 using ValueMap = llvm::ScopedHashTable<mlir::Value, std::string>;
33 #define DEBUG_TYPE "export-smtlib"
41 mlir::raw_indented_ostream &> {
44 void visitSMTType(BoolType type, mlir::raw_indented_ostream &stream) {
48 void visitSMTType(IntType type, mlir::raw_indented_ostream &stream) {
52 void visitSMTType(BitVectorType type, mlir::raw_indented_ostream &stream) {
53 stream <<
"(_ BitVec " << type.getWidth() <<
")";
56 void visitSMTType(ArrayType type, mlir::raw_indented_ostream &stream) {
58 dispatchSMTTypeVisitor(type.getDomainType(), stream);
60 dispatchSMTTypeVisitor(type.getRangeType(), stream);
64 void visitSMTType(SMTFuncType type, mlir::raw_indented_ostream &stream) {
66 StringLiteral nextToken =
"";
68 for (Type domainTy : type.getDomainTypes()) {
70 dispatchSMTTypeVisitor(domainTy, stream);
75 dispatchSMTTypeVisitor(type.getRangeType(), stream);
78 void visitSMTType(SortType type, mlir::raw_indented_ostream &stream) {
79 if (!type.getSortParams().empty())
82 stream << type.getIdentifier().getValue();
83 for (Type paramTy : type.getSortParams()) {
85 dispatchSMTTypeVisitor(paramTy, stream);
88 if (!type.getSortParams().empty())
100 VisitorInfo(mlir::raw_indented_ostream &stream,
ValueMap &valueMap)
101 : stream(stream), valueMap(valueMap) {}
102 VisitorInfo(mlir::raw_indented_ostream &stream,
ValueMap &valueMap,
103 unsigned indentLevel,
unsigned openParens)
104 : stream(stream), valueMap(valueMap), indentLevel(indentLevel),
105 openParens(openParens) {}
108 mlir::raw_indented_ostream &stream;
112 unsigned indentLevel = 0;
114 unsigned openParens = 0;
119 struct ExpressionVisitor
124 using Base::visitSMTOp;
127 : options(options), typeVisitor(options), names(names) {}
129 LogicalResult dispatchSMTOpVisitor(Operation *op, VisitorInfo &info) {
130 assert(op->getNumResults() == 1 &&
131 "expression op must have exactly one result value");
140 Value res = op->getResult(0);
143 llvm::raw_string_ostream sstream(str);
144 mlir::raw_indented_ostream indentedStream(sstream);
146 VisitorInfo newInfo(indentedStream, info.valueMap, info.indentLevel,
148 if (failed(Base::dispatchSMTOpVisitor(op, newInfo)))
151 info.valueMap.insert(res, str);
158 auto name = names.
newName(
"tmp");
159 info.valueMap.insert(res, name.str());
160 info.stream <<
"(let ((" << name <<
" ";
162 VisitorInfo newInfo(info.stream, info.valueMap,
163 info.indentLevel + 8 + name.size(), 0);
164 if (failed(Base::dispatchSMTOpVisitor(op, newInfo)))
167 info.stream <<
"))\n";
171 info.indentLevel += 5;
174 info.stream.indent(info.indentLevel);
183 template <
typename Op>
184 LogicalResult printBinaryOp(Op op, StringRef name, VisitorInfo &info) {
185 info.stream <<
"(" << name <<
" " << info.valueMap.lookup(op.getLhs())
186 <<
" " << info.valueMap.lookup(op.getRhs()) <<
")";
190 template <
typename Op>
191 LogicalResult printVariadicOp(Op op, StringRef name, VisitorInfo &info) {
192 info.stream <<
"(" << name;
193 for (Value val : op.getOperands())
194 info.stream <<
" " << info.valueMap.lookup(val);
199 LogicalResult visitSMTOp(BVNegOp op, VisitorInfo &info) {
200 info.stream <<
"(bvneg " << info.valueMap.lookup(op.getInput()) <<
")";
204 LogicalResult visitSMTOp(BVNotOp op, VisitorInfo &info) {
205 info.stream <<
"(bvnot " << info.valueMap.lookup(op.getInput()) <<
")";
209 #define HANDLE_OP(OPTYPE, NAME, KIND) \
210 LogicalResult visitSMTOp(OPTYPE op, VisitorInfo &info) { \
211 return print##KIND##Op(op, NAME, info); \
229 LogicalResult visitSMTOp(ExtractOp op, VisitorInfo &info) {
230 info.stream <<
"((_ extract "
231 << (op.getLowBit() + op.getType().getWidth() - 1) <<
" "
232 << op.getLowBit() <<
") " << info.valueMap.lookup(op.getInput())
237 LogicalResult visitSMTOp(RepeatOp op, VisitorInfo &info) {
238 info.stream <<
"((_ repeat " << op.getCount() <<
") "
239 << info.valueMap.lookup(op.getInput()) <<
")";
243 LogicalResult visitSMTOp(BVCmpOp op, VisitorInfo &info) {
244 return printBinaryOp(op,
"bv" + stringifyBVCmpPredicate(op.getPred()).str(),
258 LogicalResult visitSMTOp(IntCmpOp op, VisitorInfo &info) {
259 switch (op.getPred()) {
260 case IntPredicate::ge:
261 return printBinaryOp(op,
">=", info);
262 case IntPredicate::le:
263 return printBinaryOp(op,
"<=", info);
264 case IntPredicate::gt:
265 return printBinaryOp(op,
">", info);
266 case IntPredicate::lt:
267 return printBinaryOp(op,
"<", info);
277 HANDLE_OP(DistinctOp,
"distinct", Variadic);
279 LogicalResult visitSMTOp(IteOp op, VisitorInfo &info) {
280 info.stream <<
"(ite " << info.valueMap.lookup(op.getCond()) <<
" "
281 << info.valueMap.lookup(op.getThenValue()) <<
" "
282 << info.valueMap.lookup(op.getElseValue()) <<
")";
286 LogicalResult visitSMTOp(ApplyFuncOp op, VisitorInfo &info) {
287 info.stream <<
"(" << info.valueMap.lookup(op.getFunc());
288 for (Value arg : op.getArgs())
289 info.stream <<
" " << info.valueMap.lookup(arg);
294 template <
typename OpTy>
295 LogicalResult quantifierHelper(OpTy op, StringRef operatorString,
297 auto weight = op.getWeight();
300 if (op.getNoPattern())
301 return op.emitError() <<
"no-pattern attribute not supported yet";
303 llvm::ScopedHashTableScope<Value, std::string> scope(info.valueMap);
304 info.stream <<
"(" << operatorString <<
" (";
305 StringLiteral delimiter =
"";
307 SmallVector<StringRef> argNames;
309 for (
auto [i, arg] : llvm::enumerate(op.getBody().getArguments())) {
312 op.getBoundVarNames()
313 ? cast<StringAttr>(op.getBoundVarNames()->getValue()[i])
316 StringRef name = names.
newName(prefix);
317 argNames.push_back(name);
319 info.valueMap.insert(arg, name.str());
322 info.stream << delimiter <<
"(" << name <<
" ";
323 typeVisitor.dispatchSMTTypeVisitor(arg.getType(), info.stream);
328 info.stream <<
")\n";
333 SmallVector<Value> worklist;
334 Value yieldedValue = op.getBody().front().getTerminator()->getOperand(0);
335 worklist.push_back(yieldedValue);
336 unsigned indentExt = operatorString.size() + 2;
337 VisitorInfo newInfo(info.stream, info.valueMap,
338 info.indentLevel + indentExt, 0);
339 if (weight != 0 || !
patterns.empty())
340 newInfo.stream.indent(newInfo.indentLevel);
342 newInfo.stream.indent(info.indentLevel);
344 if (weight != 0 || !
patterns.empty())
345 info.stream <<
"( ! ";
347 if (failed(printExpression(worklist, newInfo)))
350 info.stream << info.valueMap.lookup(yieldedValue);
352 for (
unsigned j = 0; j < newInfo.openParens; ++j)
356 info.stream <<
" :weight " << weight;
359 info.stream <<
"\n:pattern (";
366 for (
auto [i, arg] : llvm::enumerate(p.getArguments()))
367 info.valueMap.insert(arg, argNames[i].str());
369 SmallVector<Value> worklist;
372 for (
auto yieldedValue : p.front().getTerminator()->getOperands()) {
374 worklist.push_back(yieldedValue);
375 unsigned indentExt = operatorString.size() + 2;
377 VisitorInfo newInfo2(info.stream, info.valueMap,
378 info.indentLevel + indentExt, 0);
380 info.stream.indent(0);
382 if (failed(printExpression(worklist, newInfo2)))
385 info.stream << info.valueMap.lookup(yieldedValue);
386 for (
unsigned j = 0; j < newInfo2.openParens; ++j)
395 if (weight != 0 || !
patterns.empty())
403 LogicalResult visitSMTOp(ForallOp op, VisitorInfo &info) {
404 return quantifierHelper(op,
"forall", info);
407 LogicalResult visitSMTOp(ExistsOp op, VisitorInfo &info) {
408 return quantifierHelper(op,
"exists", info);
411 LogicalResult visitSMTOp(NotOp op, VisitorInfo &info) {
412 info.stream <<
"(not " << info.valueMap.lookup(op.getInput()) <<
")";
425 LogicalResult visitSMTOp(ArrayStoreOp op, VisitorInfo &info) {
426 info.stream <<
"(store " << info.valueMap.lookup(op.getArray()) <<
" "
427 << info.valueMap.lookup(op.getIndex()) <<
" "
428 << info.valueMap.lookup(op.getValue()) <<
")";
432 LogicalResult visitSMTOp(ArraySelectOp op, VisitorInfo &info) {
433 info.stream <<
"(select " << info.valueMap.lookup(op.getArray()) <<
" "
434 << info.valueMap.lookup(op.getIndex()) <<
")";
438 LogicalResult visitSMTOp(ArrayBroadcastOp op, VisitorInfo &info) {
439 info.stream <<
"((as const ";
440 typeVisitor.dispatchSMTTypeVisitor(op.getType(), info.stream);
441 info.stream <<
") " << info.valueMap.lookup(op.getValue()) <<
")";
445 LogicalResult visitUnhandledSMTOp(Operation *op, VisitorInfo &info) {
453 LogicalResult printExpression(SmallVector<Value> &worklist,
455 while (!worklist.empty()) {
456 Value curr = worklist.back();
459 if (info.valueMap.count(curr)) {
466 bool allAvailable =
true;
467 Operation *defOp = curr.getDefiningOp();
468 assert(defOp !=
nullptr &&
469 "block arguments must already be in the valueMap");
471 for (Value val : defOp->getOperands()) {
472 if (!info.valueMap.count(val)) {
473 worklist.push_back(val);
474 allAvailable =
false;
481 if (failed(dispatchSMTOpVisitor(curr.getDefiningOp(), info)))
493 TypeVisitor typeVisitor;
499 struct StatementVisitor
501 mlir::raw_indented_ostream &, ValueMap &> {
503 mlir::raw_indented_ostream &,
ValueMap &>::visitSMTOp;
506 : options(options), typeVisitor(options), names(names),
507 exprVisitor(options, names) {}
509 LogicalResult visitSMTOp(BVConstantOp op, mlir::raw_indented_ostream &stream,
511 valueMap.insert(op.getResult(), op.getValue().getValueAsString());
515 LogicalResult visitSMTOp(BoolConstantOp op,
516 mlir::raw_indented_ostream &stream,
518 valueMap.insert(op.getResult(), op.getValue() ?
"true" :
"false");
522 LogicalResult visitSMTOp(IntConstantOp op, mlir::raw_indented_ostream &stream,
525 op.getValue().toStringSigned(str);
526 valueMap.insert(op.getResult(), str.str().str());
530 LogicalResult visitSMTOp(DeclareFunOp op, mlir::raw_indented_ostream &stream,
533 names.
newName(op.getNamePrefix() ? *op.getNamePrefix() :
"tmp");
534 valueMap.insert(op.getResult(), name.str());
536 << (isa<SMTFuncType>(op.getType()) ?
"declare-fun "
539 typeVisitor.dispatchSMTTypeVisitor(op.getType(), stream);
544 LogicalResult visitSMTOp(AssertOp op, mlir::raw_indented_ostream &stream,
546 llvm::ScopedHashTableScope<Value, std::string> scope1(valueMap);
547 SmallVector<Value> worklist;
548 worklist.push_back(op.getInput());
549 stream <<
"(assert ";
550 VisitorInfo info(stream, valueMap, 8, 0);
551 if (failed(exprVisitor.printExpression(worklist, info)))
553 stream << valueMap.lookup(op.getInput());
554 for (
unsigned i = 0; i < info.openParens + 1; ++i)
561 LogicalResult visitSMTOp(ResetOp op, mlir::raw_indented_ostream &stream,
563 stream <<
"(reset)\n";
567 LogicalResult visitSMTOp(PushOp op, mlir::raw_indented_ostream &stream,
569 stream <<
"(push " << op.getCount() <<
")\n";
573 LogicalResult visitSMTOp(PopOp op, mlir::raw_indented_ostream &stream,
575 stream <<
"(pop " << op.getCount() <<
")\n";
579 LogicalResult visitSMTOp(CheckOp op, mlir::raw_indented_ostream &stream,
581 if (op->getNumResults() != 0)
582 return op.emitError() <<
"must not have any result values";
584 if (op.getSatRegion().front().getOperations().size() != 1)
585 return op->emitError() <<
"'sat' region must be empty";
586 if (op.getUnknownRegion().front().getOperations().size() != 1)
587 return op->emitError() <<
"'unknown' region must be empty";
588 if (op.getUnsatRegion().front().getOperations().size() != 1)
589 return op->emitError() <<
"'unsat' region must be empty";
591 stream <<
"(check-sat)\n";
595 LogicalResult visitUnhandledSMTOp(Operation *op,
596 mlir::raw_indented_ostream &stream,
605 TypeVisitor typeVisitor;
607 ExpressionVisitor exprVisitor;
618 mlir::raw_indented_ostream &stream) {
619 if (!solver.getInputs().empty() || solver->getNumResults() != 0)
620 return solver->emitError()
621 <<
"solver scopes with inputs or results are not supported";
623 Block *block = solver.getBody();
626 DenseMap<StringAttr, unsigned> declaredSorts;
627 auto result = block->walk([&](Operation *op) -> WalkResult {
628 if (!isa<SMTDialect>(op->getDialect()))
629 return op->emitError()
630 <<
"solver must not contain any non-SMT operations";
632 for (Type resTy : op->getResultTypes()) {
633 auto sortTy = dyn_cast<SortType>(resTy);
637 unsigned arity = sortTy.getSortParams().size();
638 if (declaredSorts.contains(sortTy.getIdentifier())) {
639 if (declaredSorts[sortTy.getIdentifier()] != arity)
640 return op->emitError(
"uninterpreted sorts with same identifier but "
641 "different arity found");
646 declaredSorts[sortTy.getIdentifier()] = arity;
647 stream <<
"(declare-sort " << sortTy.getIdentifier().getValue() <<
" "
650 return WalkResult::advance();
652 if (result.wasInterrupted())
656 llvm::ScopedHashTableScope<Value, std::string> scope0(valueMap);
658 StatementVisitor visitor(options, names);
662 result = block->walk([&](Operation *op) {
663 if (failed(visitor.dispatchSMTOpVisitor(op, stream, valueMap)))
664 return WalkResult::interrupt();
665 return WalkResult::advance();
667 if (result.wasInterrupted())
670 stream <<
"(reset)\n";
675 llvm::raw_ostream &os,
677 if (module->getNumRegions() != 1)
678 return module->emitError(
"must have exactly one region");
679 if (!module->getRegion(0).hasOneBlock())
680 return module->emitError(
"op region must have exactly one block");
682 mlir::raw_indented_ostream ios(os);
683 unsigned solverIdx = 0;
684 auto result = module->walk([&](SolverOp solver) {
685 ios <<
"; solver scope " << solverIdx <<
"\n";
686 if (failed(
emit(solver, options, ios)))
687 return WalkResult::interrupt();
689 return WalkResult::advance();
692 return failure(result.wasInterrupted());
701 "smtlibexport-inline-single-use-values",
702 llvm::cl::desc(
"Inline expressions that are used only once rather than "
703 "generating a let-binding"),
704 llvm::cl::init(
false));
706 auto getOptions = [] {
712 static mlir::TranslateFromMLIRRegistration toSMTLIB(
713 "export-smtlib",
"export SMT-LIB",
714 [=](Operation *module, raw_ostream &output) {
717 [](mlir::DialectRegistry ®istry) {
721 .insert<mlir::func::FuncDialect, hw::HWDialect, smt::SMTDialect>();
assert(baseType &&"element must be base type")
llvm::ScopedHashTable< mlir::Value, std::string > ValueMap
static LogicalResult emit(SolverOp solver, const SMTEmissionOptions &options, mlir::raw_indented_ostream &stream)
Emit the SMT operations in the given 'solver' to the 'stream'.
#define HANDLE_OP(OPTYPE, NAME, KIND)
A namespace that is used to store existing names and generate new names in some scope within the IR.
StringRef newName(const Twine &name)
Return a unique name, derived from the input name, and add the new name to the internal namespace.
This helps visit SMT nodes.
This helps visit SMT types.
LogicalResult exportSMTLIB(Operation *module, llvm::raw_ostream &os, const SMTEmissionOptions &options=SMTEmissionOptions())
Run the ExportSMTLIB pass.
void registerExportSMTLIBTranslation()
Register the ExportSMTLIB pass.
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.
Emission options for the ExportSMTLIB pass.
bool inlineSingleUseValues