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/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 that
37/// 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: type.getDomainType(), args&: stream);
57 stream << " ";
58 dispatchSMTTypeVisitor(type: type.getRangeType(), args&: 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(type: domainTy, args&: stream);
69 nextToken = " ";
70 }
71
72 stream << ") ";
73 dispatchSMTTypeVisitor(type: type.getRangeType(), args&: 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(type: paramTy, args&: 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 it
96/// 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 as
116/// the equivalent operator in SMT-LIB.
117struct ExpressionVisitor
118 : 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 the
132 // corresponding emission option is enabled. This can lead to bad
133 // performance for big inputs since the inlined expression is stored as a
134 // string in the value mapping where otherwise only the symbol names of free
135 // and bound variables are stored, and due to a lot of string concatenation
136 // (thus it's off by default and just intended to print small examples in a
137 // more human-readable format).
138 Value res = op->getResult(idx: 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(Result: Base::dispatchSMTOpVisitor(op, args&: newInfo)))
147 return failure();
148
149 info.valueMap.insert(Key: res, Val: str);
150 return success();
151 }
152
153 // Generate a let binding for the current expression being processed and
154 // store the sybmol in the value map. Indent the expressions for easier
155 // readability.
156 auto name = names.newName(name: "tmp");
157 info.valueMap.insert(Key: res, Val: 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(Result: Base::dispatchSMTOpVisitor(op, args&: newInfo)))
163 return failure();
164
165 info.stream << "))\n";
166
167 if (options.indentLetBody) {
168 // Five spaces to align with the opening parenthesis
169 info.indentLevel += 5;
170 }
171 ++info.openParens;
172 info.stream.indent(with: info.indentLevel);
173
174 return success();
175 }
176
177 //===--------------------------------------------------------------------===//
178 // Bit-vector theory operation visitors
179 //===--------------------------------------------------------------------===//
180
181 template <typename Op>
182 LogicalResult printBinaryOp(Op op, StringRef name, VisitorInfo &info) {
183 info.stream << "(" << name << " " << info.valueMap.lookup(Key: op.getLhs())
184 << " " << info.valueMap.lookup(Key: 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(Key: val);
193 info.stream << ")";
194 return success();
195 }
196
197 LogicalResult visitSMTOp(BVNegOp op, VisitorInfo &info) {
198 info.stream << "(bvneg " << info.valueMap.lookup(Key: op.getInput()) << ")";
199 return success();
200 }
201
202 LogicalResult visitSMTOp(BVNotOp op, VisitorInfo &info) {
203 info.stream << "(bvnot " << info.valueMap.lookup(Key: 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(Key: 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(Key: op.getInput()) << ")";
238 return success();
239 }
240
241 LogicalResult visitSMTOp(BVCmpOp op, VisitorInfo &info) {
242 return printBinaryOp(op, name: "bv" + stringifyBVCmpPredicate(op.getPred()).str(),
243 info);
244 }
245
246 //===--------------------------------------------------------------------===//
247 // Int theory operation visitors
248 //===--------------------------------------------------------------------===//
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, name: ">=", info);
260 case IntPredicate::le:
261 return printBinaryOp(op, name: "<=", info);
262 case IntPredicate::gt:
263 return printBinaryOp(op, name: ">", info);
264 case IntPredicate::lt:
265 return printBinaryOp(op, name: "<", info);
266 }
267 return failure();
268 }
269
270 //===--------------------------------------------------------------------===//
271 // Core theory operation visitors
272 //===--------------------------------------------------------------------===//
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(Key: op.getCond()) << " "
279 << info.valueMap.lookup(Key: op.getThenValue()) << " "
280 << info.valueMap.lookup(Key: op.getElseValue()) << ")";
281 return success();
282 }
283
284 LogicalResult visitSMTOp(ApplyFuncOp op, VisitorInfo &info) {
285 info.stream << "(" << info.valueMap.lookup(Key: op.getFunc());
286 for (Value arg : op.getArgs())
287 info.stream << " " << info.valueMap.lookup(Key: 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 support
298 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(name: prefix);
315 argNames.push_back(Elt: name);
316
317 info.valueMap.insert(Key: arg, Val: name.str());
318
319 // Print the bound variable declaration.
320 info.stream << delimiter << "(" << name << " ";
321 typeVisitor.dispatchSMTTypeVisitor(type: arg.getType(), args&: 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 deeply
329 // 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(Elt: 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(with: newInfo.indentLevel);
339 else
340 newInfo.stream.indent(with: info.indentLevel);
341
342 if (weight != 0 || !patterns.empty())
343 info.stream << "( ! ";
344
345 if (failed(Result: printExpression(worklist, info&: newInfo)))
346 return failure();
347
348 info.stream << info.valueMap.lookup(Key: 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 region
364 for (auto [i, arg] : llvm::enumerate(p.getArguments()))
365 info.valueMap.insert(Key: arg, Val: argNames[i].str());
366
367 SmallVector<Value> worklist;
368
369 // retrieve all yielded operands in pattern region
370 for (auto yieldedValue : p.front().getTerminator()->getOperands()) {
371
372 worklist.push_back(Elt: 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(with: 0);
379
380 if (failed(Result: printExpression(worklist, info&: newInfo2)))
381 return failure();
382
383 info.stream << info.valueMap.lookup(Key: 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, operatorString: "forall", info);
403 }
404
405 LogicalResult visitSMTOp(ExistsOp op, VisitorInfo &info) {
406 return quantifierHelper(op, operatorString: "exists", info);
407 }
408
409 LogicalResult visitSMTOp(NotOp op, VisitorInfo &info) {
410 info.stream << "(not " << info.valueMap.lookup(Key: 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 visitors
421 //===--------------------------------------------------------------------===//
422
423 LogicalResult visitSMTOp(ArrayStoreOp op, VisitorInfo &info) {
424 info.stream << "(store " << info.valueMap.lookup(Key: op.getArray()) << " "
425 << info.valueMap.lookup(Key: op.getIndex()) << " "
426 << info.valueMap.lookup(Key: op.getValue()) << ")";
427 return success();
428 }
429
430 LogicalResult visitSMTOp(ArraySelectOp op, VisitorInfo &info) {
431 info.stream << "(select " << info.valueMap.lookup(Key: op.getArray()) << " "
432 << info.valueMap.lookup(Key: op.getIndex()) << ")";
433 return success();
434 }
435
436 LogicalResult visitSMTOp(ArrayBroadcastOp op, VisitorInfo &info) {
437 info.stream << "((as const ";
438 typeVisitor.dispatchSMTTypeVisitor(type: op.getType(), args&: info.stream);
439 info.stream << ") " << info.valueMap.lookup(Key: op.getValue()) << ")";
440 return success();
441 }
442
443 LogicalResult visitUnhandledSMTOp(Operation *op, VisitorInfo &info) {
444 return success();
445 }
446
447#undef HANDLE_OP
448
449 /// Print an expression transitively. The root node should be added to the
450 /// '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(Key: curr)) {
458 worklist.pop_back();
459 continue;
460 }
461
462 // Traverse until we reach a value/operation that has all operands
463 // 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(Key: val)) {
471 worklist.push_back(Elt: val);
472 allAvailable = false;
473 }
474 }
475
476 if (!allAvailable)
477 continue;
478
479 if (failed(Result: dispatchSMTOpVisitor(op: 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 or
496/// ones that have to initialize some global state.
497struct StatementVisitor
498 : 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(Key: op.getResult(), Val: 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(Key: op.getResult(), Val: 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&: str);
524 valueMap.insert(Key: op.getResult(), Val: 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(name: op.getNamePrefix() ? *op.getNamePrefix() : "tmp");
532 valueMap.insert(Key: op.getResult(), Val: name.str());
533 stream << "("
534 << (isa<SMTFuncType>(Val: op.getType()) ? "declare-fun "
535 : "declare-const ")
536 << name << " ";
537 typeVisitor.dispatchSMTTypeVisitor(type: op.getType(), args&: 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(Elt: op.getInput());
547 stream << "(assert ";
548 VisitorInfo info(stream, valueMap, 8, 0);
549 if (failed(Result: exprVisitor.printExpression(worklist, info)))
550 return failure();
551 stream << valueMap.lookup(Key: op.getInput());
552 for (unsigned i = 0; i < info.openParens + 1; ++i)
553 stream << ")";
554 stream << "\n";
555 stream.indent(with: 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>(Val: op))
604 return op->emitError(message: "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} // namespace
618
619//===----------------------------------------------------------------------===//
620// Unified Emitter implementation
621//===----------------------------------------------------------------------===//
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(callback: [&](Operation *op) -> WalkResult {
635 if (!isa<SMTDialect>(Val: 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>(Val&: resTy);
641 if (!sortTy)
642 continue;
643
644 unsigned arity = sortTy.getSortParams().size();
645 if (declaredSorts.contains(Val: sortTy.getIdentifier())) {
646 if (declaredSorts[sortTy.getIdentifier()] != arity)
647 return op->emitError(message: "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(callback: [&](Operation *op) {
670 if (failed(Result: visitor.dispatchSMTOpVisitor(op, args&: stream, args&: 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(message: "must have exactly one region");
685 if (!module->getRegion(index: 0).hasOneBlock())
686 return module->emitError(message: "op region must have exactly one block");
687
688 mlir::raw_indented_ostream ios(os);
689 unsigned solverIdx = 0;
690 auto result = module->walk(callback: [&](SolverOp solver) {
691 ios << "; solver scope " << solverIdx << "\n";
692 if (failed(Result: emit(solver, options, stream&: ios)))
693 return WalkResult::interrupt();
694 ++solverIdx;
695 return WalkResult::advance();
696 });
697
698 return failure(IsFailure: result.wasInterrupted());
699}
700
701//===----------------------------------------------------------------------===//
702// mlir-translate registration
703//===----------------------------------------------------------------------===//
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(Val: 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, os&: output, options: getOptions());
722 },
723 [](mlir::DialectRegistry &registry) {
724 // Register the 'func' and 'HW' dialects to support printing solver
725 // scopes nested in functions and modules.
726 registry.insert<mlir::func::FuncDialect, arith::ArithDialect,
727 smt::SMTDialect>();
728 });
729}
730

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