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 | |
27 | using namespace mlir; |
28 | using namespace smt; |
29 | |
30 | using ValueMap = llvm::ScopedHashTable<mlir::Value, std::string>; |
31 | |
32 | #define DEBUG_TYPE "export-smtlib" |
33 | |
34 | namespace { |
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. |
39 | struct 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 | |
91 | private: |
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. |
98 | struct 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. |
118 | struct 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 | |
489 | private: |
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. |
498 | struct 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 | |
610 | private: |
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'. |
625 | static 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 | |
682 | LogicalResult 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 | |
706 | void 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 ®istry) { |
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 | |