730 lines · cpp
1//===- ExportSMTLIB.cpp - SMT-LIB Emitter -----=---------------------------===//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-exception6//7//===----------------------------------------------------------------------===//8//9// This is the main SMT-LIB emitter implementation.10//11//===----------------------------------------------------------------------===//12 13#include "mlir/Target/SMTLIB/ExportSMTLIB.h"14 15#include "mlir/Dialect/Arith/Utils/Utils.h"16#include "mlir/Dialect/Func/IR/FuncOps.h"17#include "mlir/Dialect/SMT/IR/SMTOps.h"18#include "mlir/Dialect/SMT/IR/SMTVisitors.h"19#include "mlir/Support/IndentedOstream.h"20#include "mlir/Target/SMTLIB/Namespace.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/raw_ostream.h"25 26using namespace mlir;27using namespace smt;28 29using ValueMap = llvm::ScopedHashTable<mlir::Value, std::string>;30 31#define DEBUG_TYPE "export-smtlib"32 33namespace {34 35/// A visitor to print the SMT dialect types as SMT-LIB formatted sorts.36/// Printing nested types use recursive calls since nestings of a depth that37/// could lead to problems should not occur in practice.38struct TypeVisitor : public smt::SMTTypeVisitor<TypeVisitor, void,39 mlir::raw_indented_ostream &> {40 TypeVisitor(const SMTEmissionOptions &options) : options(options) {}41 42 void visitSMTType(BoolType type, mlir::raw_indented_ostream &stream) {43 stream << "Bool";44 }45 46 void visitSMTType(IntType type, mlir::raw_indented_ostream &stream) {47 stream << "Int";48 }49 50 void visitSMTType(BitVectorType type, mlir::raw_indented_ostream &stream) {51 stream << "(_ BitVec " << type.getWidth() << ")";52 }53 54 void visitSMTType(ArrayType type, mlir::raw_indented_ostream &stream) {55 stream << "(Array ";56 dispatchSMTTypeVisitor(type.getDomainType(), stream);57 stream << " ";58 dispatchSMTTypeVisitor(type.getRangeType(), stream);59 stream << ")";60 }61 62 void visitSMTType(SMTFuncType type, mlir::raw_indented_ostream &stream) {63 stream << "(";64 StringLiteral nextToken = "";65 66 for (Type domainTy : type.getDomainTypes()) {67 stream << nextToken;68 dispatchSMTTypeVisitor(domainTy, stream);69 nextToken = " ";70 }71 72 stream << ") ";73 dispatchSMTTypeVisitor(type.getRangeType(), stream);74 }75 76 void visitSMTType(SortType type, mlir::raw_indented_ostream &stream) {77 if (!type.getSortParams().empty())78 stream << "(";79 80 stream << type.getIdentifier().getValue();81 for (Type paramTy : type.getSortParams()) {82 stream << " ";83 dispatchSMTTypeVisitor(paramTy, stream);84 }85 86 if (!type.getSortParams().empty())87 stream << ")";88 }89 90private:91 // A reference to the emission options for easy use in the visitor methods.92 [[maybe_unused]] const SMTEmissionOptions &options;93};94 95/// Contains the informations passed to the ExpressionVisitor methods. Makes it96/// easier to add more information.97struct VisitorInfo {98 VisitorInfo(mlir::raw_indented_ostream &stream, ValueMap &valueMap)99 : stream(stream), valueMap(valueMap) {}100 VisitorInfo(mlir::raw_indented_ostream &stream, ValueMap &valueMap,101 unsigned indentLevel, unsigned openParens)102 : stream(stream), valueMap(valueMap), indentLevel(indentLevel),103 openParens(openParens) {}104 105 // Stream to print to.106 mlir::raw_indented_ostream &stream;107 // Mapping from SSA values to SMT-LIB expressions.108 ValueMap &valueMap;109 // Total number of spaces currently indented.110 unsigned indentLevel = 0;111 // Number of parentheses that have been opened but not closed yet.112 unsigned openParens = 0;113};114 115/// A visitor to print SMT dialect operations with exactly one result value as116/// the equivalent operator in SMT-LIB.117struct ExpressionVisitor118 : public smt::SMTOpVisitor<ExpressionVisitor, LogicalResult,119 VisitorInfo &> {120 using Base =121 smt::SMTOpVisitor<ExpressionVisitor, LogicalResult, VisitorInfo &>;122 using Base::visitSMTOp;123 124 ExpressionVisitor(const SMTEmissionOptions &options, Namespace &names)125 : options(options), typeVisitor(options), names(names) {}126 127 LogicalResult dispatchSMTOpVisitor(Operation *op, VisitorInfo &info) {128 assert(op->getNumResults() == 1 &&129 "expression op must have exactly one result value");130 131 // Print the expression inlined if it is only used once and the132 // corresponding emission option is enabled. This can lead to bad133 // performance for big inputs since the inlined expression is stored as a134 // string in the value mapping where otherwise only the symbol names of free135 // and bound variables are stored, and due to a lot of string concatenation136 // (thus it's off by default and just intended to print small examples in a137 // more human-readable format).138 Value res = op->getResult(0);139 if (res.hasOneUse() && options.inlineSingleUseValues) {140 std::string str;141 llvm::raw_string_ostream sstream(str);142 mlir::raw_indented_ostream indentedStream(sstream);143 144 VisitorInfo newInfo(indentedStream, info.valueMap, info.indentLevel,145 info.openParens);146 if (failed(Base::dispatchSMTOpVisitor(op, newInfo)))147 return failure();148 149 info.valueMap.insert(res, str);150 return success();151 }152 153 // Generate a let binding for the current expression being processed and154 // store the sybmol in the value map. Indent the expressions for easier155 // readability.156 auto name = names.newName("tmp");157 info.valueMap.insert(res, name.str());158 info.stream << "(let ((" << name << " ";159 160 VisitorInfo newInfo(info.stream, info.valueMap,161 info.indentLevel + 8 + name.size(), 0);162 if (failed(Base::dispatchSMTOpVisitor(op, newInfo)))163 return failure();164 165 info.stream << "))\n";166 167 if (options.indentLetBody) {168 // Five spaces to align with the opening parenthesis169 info.indentLevel += 5;170 }171 ++info.openParens;172 info.stream.indent(info.indentLevel);173 174 return success();175 }176 177 //===--------------------------------------------------------------------===//178 // Bit-vector theory operation visitors179 //===--------------------------------------------------------------------===//180 181 template <typename Op>182 LogicalResult printBinaryOp(Op op, StringRef name, VisitorInfo &info) {183 info.stream << "(" << name << " " << info.valueMap.lookup(op.getLhs())184 << " " << info.valueMap.lookup(op.getRhs()) << ")";185 return success();186 }187 188 template <typename Op>189 LogicalResult printVariadicOp(Op op, StringRef name, VisitorInfo &info) {190 info.stream << "(" << name;191 for (Value val : op.getOperands())192 info.stream << " " << info.valueMap.lookup(val);193 info.stream << ")";194 return success();195 }196 197 LogicalResult visitSMTOp(BVNegOp op, VisitorInfo &info) {198 info.stream << "(bvneg " << info.valueMap.lookup(op.getInput()) << ")";199 return success();200 }201 202 LogicalResult visitSMTOp(BVNotOp op, VisitorInfo &info) {203 info.stream << "(bvnot " << info.valueMap.lookup(op.getInput()) << ")";204 return success();205 }206 207#define HANDLE_OP(OPTYPE, NAME, KIND) \208 LogicalResult visitSMTOp(OPTYPE op, VisitorInfo &info) { \209 return print##KIND##Op(op, NAME, info); \210 }211 212 HANDLE_OP(BVAddOp, "bvadd", Binary);213 HANDLE_OP(BVMulOp, "bvmul", Binary);214 HANDLE_OP(BVURemOp, "bvurem", Binary);215 HANDLE_OP(BVSRemOp, "bvsrem", Binary);216 HANDLE_OP(BVSModOp, "bvsmod", Binary);217 HANDLE_OP(BVShlOp, "bvshl", Binary);218 HANDLE_OP(BVLShrOp, "bvlshr", Binary);219 HANDLE_OP(BVAShrOp, "bvashr", Binary);220 HANDLE_OP(BVUDivOp, "bvudiv", Binary);221 HANDLE_OP(BVSDivOp, "bvsdiv", Binary);222 HANDLE_OP(BVAndOp, "bvand", Binary);223 HANDLE_OP(BVOrOp, "bvor", Binary);224 HANDLE_OP(BVXOrOp, "bvxor", Binary);225 HANDLE_OP(ConcatOp, "concat", Binary);226 227 LogicalResult visitSMTOp(ExtractOp op, VisitorInfo &info) {228 info.stream << "((_ extract "229 << (op.getLowBit() + op.getType().getWidth() - 1) << " "230 << op.getLowBit() << ") " << info.valueMap.lookup(op.getInput())231 << ")";232 return success();233 }234 235 LogicalResult visitSMTOp(RepeatOp op, VisitorInfo &info) {236 info.stream << "((_ repeat " << op.getCount() << ") "237 << info.valueMap.lookup(op.getInput()) << ")";238 return success();239 }240 241 LogicalResult visitSMTOp(BVCmpOp op, VisitorInfo &info) {242 return printBinaryOp(op, "bv" + stringifyBVCmpPredicate(op.getPred()).str(),243 info);244 }245 246 //===--------------------------------------------------------------------===//247 // Int theory operation visitors248 //===--------------------------------------------------------------------===//249 250 HANDLE_OP(IntAddOp, "+", Variadic);251 HANDLE_OP(IntMulOp, "*", Variadic);252 HANDLE_OP(IntSubOp, "-", Binary);253 HANDLE_OP(IntDivOp, "div", Binary);254 HANDLE_OP(IntModOp, "mod", Binary);255 256 LogicalResult visitSMTOp(IntCmpOp op, VisitorInfo &info) {257 switch (op.getPred()) {258 case IntPredicate::ge:259 return printBinaryOp(op, ">=", info);260 case IntPredicate::le:261 return printBinaryOp(op, "<=", info);262 case IntPredicate::gt:263 return printBinaryOp(op, ">", info);264 case IntPredicate::lt:265 return printBinaryOp(op, "<", info);266 }267 return failure();268 }269 270 //===--------------------------------------------------------------------===//271 // Core theory operation visitors272 //===--------------------------------------------------------------------===//273 274 HANDLE_OP(EqOp, "=", Variadic);275 HANDLE_OP(DistinctOp, "distinct", Variadic);276 277 LogicalResult visitSMTOp(IteOp op, VisitorInfo &info) {278 info.stream << "(ite " << info.valueMap.lookup(op.getCond()) << " "279 << info.valueMap.lookup(op.getThenValue()) << " "280 << info.valueMap.lookup(op.getElseValue()) << ")";281 return success();282 }283 284 LogicalResult visitSMTOp(ApplyFuncOp op, VisitorInfo &info) {285 info.stream << "(" << info.valueMap.lookup(op.getFunc());286 for (Value arg : op.getArgs())287 info.stream << " " << info.valueMap.lookup(arg);288 info.stream << ")";289 return success();290 }291 292 template <typename OpTy>293 LogicalResult quantifierHelper(OpTy op, StringRef operatorString,294 VisitorInfo &info) {295 auto weight = op.getWeight();296 auto patterns = op.getPatterns();297 // TODO: add support298 if (op.getNoPattern())299 return op.emitError() << "no-pattern attribute not supported yet";300 301 llvm::ScopedHashTableScope<Value, std::string> scope(info.valueMap);302 info.stream << "(" << operatorString << " (";303 StringLiteral delimiter = "";304 305 SmallVector<StringRef> argNames;306 307 for (auto [i, arg] : llvm::enumerate(op.getBody().getArguments())) {308 // Generate and register a new unique name.309 StringRef prefix =310 op.getBoundVarNames()311 ? cast<StringAttr>(op.getBoundVarNames()->getValue()[i])312 .getValue()313 : "tmp";314 StringRef name = names.newName(prefix);315 argNames.push_back(name);316 317 info.valueMap.insert(arg, name.str());318 319 // Print the bound variable declaration.320 info.stream << delimiter << "(" << name << " ";321 typeVisitor.dispatchSMTTypeVisitor(arg.getType(), info.stream);322 info.stream << ")";323 delimiter = " ";324 }325 326 info.stream << ")\n";327 328 // Print the quantifier body. This assumes that quantifiers are not deeply329 // nested (at least not enough that recursive calls could become a problem).330 331 SmallVector<Value> worklist;332 Value yieldedValue = op.getBody().front().getTerminator()->getOperand(0);333 worklist.push_back(yieldedValue);334 unsigned indentExt = operatorString.size() + 2;335 VisitorInfo newInfo(info.stream, info.valueMap,336 info.indentLevel + indentExt, 0);337 if (weight != 0 || !patterns.empty())338 newInfo.stream.indent(newInfo.indentLevel);339 else340 newInfo.stream.indent(info.indentLevel);341 342 if (weight != 0 || !patterns.empty())343 info.stream << "( ! ";344 345 if (failed(printExpression(worklist, newInfo)))346 return failure();347 348 info.stream << info.valueMap.lookup(yieldedValue);349 350 for (unsigned j = 0; j < newInfo.openParens; ++j)351 info.stream << ")";352 353 if (weight != 0)354 info.stream << " :weight " << weight;355 if (!patterns.empty()) {356 bool first = true;357 info.stream << "\n:pattern (";358 for (auto &p : patterns) {359 360 if (!first)361 info.stream << " ";362 363 // retrieve argument name from the body region364 for (auto [i, arg] : llvm::enumerate(p.getArguments()))365 info.valueMap.insert(arg, argNames[i].str());366 367 SmallVector<Value> worklist;368 369 // retrieve all yielded operands in pattern region370 for (auto yieldedValue : p.front().getTerminator()->getOperands()) {371 372 worklist.push_back(yieldedValue);373 unsigned indentExt = operatorString.size() + 2;374 375 VisitorInfo newInfo2(info.stream, info.valueMap,376 info.indentLevel + indentExt, 0);377 378 info.stream.indent(0);379 380 if (failed(printExpression(worklist, newInfo2)))381 return failure();382 383 info.stream << info.valueMap.lookup(yieldedValue);384 for (unsigned j = 0; j < newInfo2.openParens; ++j)385 info.stream << ")";386 }387 388 first = false;389 }390 info.stream << ")";391 }392 393 if (weight != 0 || !patterns.empty())394 info.stream << ")";395 396 info.stream << ")";397 398 return success();399 }400 401 LogicalResult visitSMTOp(ForallOp op, VisitorInfo &info) {402 return quantifierHelper(op, "forall", info);403 }404 405 LogicalResult visitSMTOp(ExistsOp op, VisitorInfo &info) {406 return quantifierHelper(op, "exists", info);407 }408 409 LogicalResult visitSMTOp(NotOp op, VisitorInfo &info) {410 info.stream << "(not " << info.valueMap.lookup(op.getInput()) << ")";411 return success();412 }413 414 HANDLE_OP(AndOp, "and", Variadic);415 HANDLE_OP(OrOp, "or", Variadic);416 HANDLE_OP(XOrOp, "xor", Variadic);417 HANDLE_OP(ImpliesOp, "=>", Binary);418 419 //===--------------------------------------------------------------------===//420 // Array theory operation visitors421 //===--------------------------------------------------------------------===//422 423 LogicalResult visitSMTOp(ArrayStoreOp op, VisitorInfo &info) {424 info.stream << "(store " << info.valueMap.lookup(op.getArray()) << " "425 << info.valueMap.lookup(op.getIndex()) << " "426 << info.valueMap.lookup(op.getValue()) << ")";427 return success();428 }429 430 LogicalResult visitSMTOp(ArraySelectOp op, VisitorInfo &info) {431 info.stream << "(select " << info.valueMap.lookup(op.getArray()) << " "432 << info.valueMap.lookup(op.getIndex()) << ")";433 return success();434 }435 436 LogicalResult visitSMTOp(ArrayBroadcastOp op, VisitorInfo &info) {437 info.stream << "((as const ";438 typeVisitor.dispatchSMTTypeVisitor(op.getType(), info.stream);439 info.stream << ") " << info.valueMap.lookup(op.getValue()) << ")";440 return success();441 }442 443 LogicalResult visitUnhandledSMTOp(Operation *op, VisitorInfo &info) {444 return success();445 }446 447#undef HANDLE_OP448 449 /// Print an expression transitively. The root node should be added to the450 /// 'worklist' before calling.451 LogicalResult printExpression(SmallVector<Value> &worklist,452 VisitorInfo &info) {453 while (!worklist.empty()) {454 Value curr = worklist.back();455 456 // If we already have a let-binding for the value, just print it.457 if (info.valueMap.count(curr)) {458 worklist.pop_back();459 continue;460 }461 462 // Traverse until we reach a value/operation that has all operands463 // available and can thus be printed.464 bool allAvailable = true;465 Operation *defOp = curr.getDefiningOp();466 assert(defOp != nullptr &&467 "block arguments must already be in the valueMap");468 469 for (Value val : defOp->getOperands()) {470 if (!info.valueMap.count(val)) {471 worklist.push_back(val);472 allAvailable = false;473 }474 }475 476 if (!allAvailable)477 continue;478 479 if (failed(dispatchSMTOpVisitor(curr.getDefiningOp(), info)))480 return failure();481 482 worklist.pop_back();483 }484 485 return success();486 }487 488private:489 // A reference to the emission options for easy use in the visitor methods.490 [[maybe_unused]] const SMTEmissionOptions &options;491 TypeVisitor typeVisitor;492 Namespace &names;493};494 495/// A visitor to print SMT dialect operations with zero result values or496/// ones that have to initialize some global state.497struct StatementVisitor498 : public smt::SMTOpVisitor<StatementVisitor, LogicalResult,499 mlir::raw_indented_ostream &, ValueMap &> {500 using smt::SMTOpVisitor<StatementVisitor, LogicalResult,501 mlir::raw_indented_ostream &, ValueMap &>::visitSMTOp;502 503 StatementVisitor(const SMTEmissionOptions &options, Namespace &names)504 : options(options), typeVisitor(options), names(names),505 exprVisitor(options, names) {}506 507 LogicalResult visitSMTOp(BVConstantOp op, mlir::raw_indented_ostream &stream,508 ValueMap &valueMap) {509 valueMap.insert(op.getResult(), op.getValue().getValueAsString());510 return success();511 }512 513 LogicalResult visitSMTOp(BoolConstantOp op,514 mlir::raw_indented_ostream &stream,515 ValueMap &valueMap) {516 valueMap.insert(op.getResult(), op.getValue() ? "true" : "false");517 return success();518 }519 520 LogicalResult visitSMTOp(IntConstantOp op, mlir::raw_indented_ostream &stream,521 ValueMap &valueMap) {522 SmallString<16> str;523 op.getValue().toStringSigned(str);524 valueMap.insert(op.getResult(), str.str().str());525 return success();526 }527 528 LogicalResult visitSMTOp(DeclareFunOp op, mlir::raw_indented_ostream &stream,529 ValueMap &valueMap) {530 StringRef name =531 names.newName(op.getNamePrefix() ? *op.getNamePrefix() : "tmp");532 valueMap.insert(op.getResult(), name.str());533 stream << "("534 << (isa<SMTFuncType>(op.getType()) ? "declare-fun "535 : "declare-const ")536 << name << " ";537 typeVisitor.dispatchSMTTypeVisitor(op.getType(), stream);538 stream << ")\n";539 return success();540 }541 542 LogicalResult visitSMTOp(AssertOp op, mlir::raw_indented_ostream &stream,543 ValueMap &valueMap) {544 llvm::ScopedHashTableScope<Value, std::string> scope1(valueMap);545 SmallVector<Value> worklist;546 worklist.push_back(op.getInput());547 stream << "(assert ";548 VisitorInfo info(stream, valueMap, 8, 0);549 if (failed(exprVisitor.printExpression(worklist, info)))550 return failure();551 stream << valueMap.lookup(op.getInput());552 for (unsigned i = 0; i < info.openParens + 1; ++i)553 stream << ")";554 stream << "\n";555 stream.indent(0);556 return success();557 }558 559 LogicalResult visitSMTOp(ResetOp op, mlir::raw_indented_ostream &stream,560 ValueMap &valueMap) {561 stream << "(reset)\n";562 return success();563 }564 565 LogicalResult visitSMTOp(PushOp op, mlir::raw_indented_ostream &stream,566 ValueMap &valueMap) {567 stream << "(push " << op.getCount() << ")\n";568 return success();569 }570 571 LogicalResult visitSMTOp(PopOp op, mlir::raw_indented_ostream &stream,572 ValueMap &valueMap) {573 stream << "(pop " << op.getCount() << ")\n";574 return success();575 }576 577 LogicalResult visitSMTOp(CheckOp op, mlir::raw_indented_ostream &stream,578 ValueMap &valueMap) {579 if (op->getNumResults() != 0)580 return op.emitError() << "must not have any result values";581 582 if (op.getSatRegion().front().getOperations().size() != 1)583 return op->emitError() << "'sat' region must be empty";584 if (op.getUnknownRegion().front().getOperations().size() != 1)585 return op->emitError() << "'unknown' region must be empty";586 if (op.getUnsatRegion().front().getOperations().size() != 1)587 return op->emitError() << "'unsat' region must be empty";588 589 stream << "(check-sat)\n";590 return success();591 }592 593 LogicalResult visitSMTOp(SetLogicOp op, mlir::raw_indented_ostream &stream,594 ValueMap &valueMap) {595 stream << "(set-logic " << op.getLogic() << ")\n";596 return success();597 }598 599 LogicalResult visitUnhandledSMTOp(Operation *op,600 mlir::raw_indented_ostream &stream,601 ValueMap &valueMap) {602 // Ignore operations which are handled in the Expression Visitor.603 if (isa<smt::Int2BVOp, BV2IntOp>(op))604 return op->emitError("operation not supported for SMTLIB emission");605 606 return success();607 }608 609private:610 // A reference to the emission options for easy use in the visitor methods.611 [[maybe_unused]] const SMTEmissionOptions &options;612 TypeVisitor typeVisitor;613 Namespace &names;614 ExpressionVisitor exprVisitor;615};616 617} // namespace618 619//===----------------------------------------------------------------------===//620// Unified Emitter implementation621//===----------------------------------------------------------------------===//622 623/// Emit the SMT operations in the given 'solver' to the 'stream'.624static LogicalResult emit(SolverOp solver, const SMTEmissionOptions &options,625 mlir::raw_indented_ostream &stream) {626 if (!solver.getInputs().empty() || solver->getNumResults() != 0)627 return solver->emitError()628 << "solver scopes with inputs or results are not supported";629 630 Block *block = solver.getBody();631 632 // Declare uninterpreted sorts.633 DenseMap<StringAttr, unsigned> declaredSorts;634 auto result = block->walk([&](Operation *op) -> WalkResult {635 if (!isa<SMTDialect>(op->getDialect()))636 return op->emitError()637 << "solver must not contain any non-SMT operations";638 639 for (Type resTy : op->getResultTypes()) {640 auto sortTy = dyn_cast<SortType>(resTy);641 if (!sortTy)642 continue;643 644 unsigned arity = sortTy.getSortParams().size();645 if (declaredSorts.contains(sortTy.getIdentifier())) {646 if (declaredSorts[sortTy.getIdentifier()] != arity)647 return op->emitError("uninterpreted sorts with same identifier but "648 "different arity found");649 650 continue;651 }652 653 declaredSorts[sortTy.getIdentifier()] = arity;654 stream << "(declare-sort " << sortTy.getIdentifier().getValue() << " "655 << arity << ")\n";656 }657 return WalkResult::advance();658 });659 if (result.wasInterrupted())660 return failure();661 662 ValueMap valueMap;663 llvm::ScopedHashTableScope<Value, std::string> scope0(valueMap);664 Namespace names;665 StatementVisitor visitor(options, names);666 667 // Collect all statement operations (ops with no result value).668 // Declare constants and then only refer to them by identifier later on.669 result = block->walk([&](Operation *op) {670 if (failed(visitor.dispatchSMTOpVisitor(op, stream, valueMap)))671 return WalkResult::interrupt();672 return WalkResult::advance();673 });674 if (result.wasInterrupted())675 return failure();676 677 stream << "(reset)\n";678 return success();679}680 681LogicalResult smt::exportSMTLIB(Operation *module, llvm::raw_ostream &os,682 const SMTEmissionOptions &options) {683 if (module->getNumRegions() != 1)684 return module->emitError("must have exactly one region");685 if (!module->getRegion(0).hasOneBlock())686 return module->emitError("op region must have exactly one block");687 688 mlir::raw_indented_ostream ios(os);689 unsigned solverIdx = 0;690 auto result = module->walk([&](SolverOp solver) {691 ios << "; solver scope " << solverIdx << "\n";692 if (failed(emit(solver, options, ios)))693 return WalkResult::interrupt();694 ++solverIdx;695 return WalkResult::advance();696 });697 698 return failure(result.wasInterrupted());699}700 701//===----------------------------------------------------------------------===//702// mlir-translate registration703//===----------------------------------------------------------------------===//704 705void smt::registerExportSMTLIBTranslation() {706 static llvm::cl::opt<bool> inlineSingleUseValues(707 "smtlibexport-inline-single-use-values",708 llvm::cl::desc("Inline expressions that are used only once rather than "709 "generating a let-binding"),710 llvm::cl::init(false));711 712 auto getOptions = [] {713 SMTEmissionOptions opts;714 opts.inlineSingleUseValues = inlineSingleUseValues;715 return opts;716 };717 718 static mlir::TranslateFromMLIRRegistration toSMTLIB(719 "export-smtlib", "export SMT-LIB",720 [=](Operation *module, raw_ostream &output) {721 return smt::exportSMTLIB(module, output, getOptions());722 },723 [](mlir::DialectRegistry ®istry) {724 // Register the 'func' and 'HW' dialects to support printing solver725 // scopes nested in functions and modules.726 registry.insert<mlir::func::FuncDialect, arith::ArithDialect,727 smt::SMTDialect>();728 });729}730