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

source code of mlir/lib/Target/SMTLIB/ExportSMTLIB.cpp