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