[Mlir-commits] [mlir] [mlir][SMT] add export smtlib (PR #131492)
Maksim Levental
llvmlistbot at llvm.org
Fri Apr 11 14:41:22 PDT 2025
https://github.com/makslevental updated https://github.com/llvm/llvm-project/pull/131492
>From bcbfdfde42985e7a0fdf2d6b22de29a1fc76ef09 Mon Sep 17 00:00:00 2001
From: max <maksim.levental at gmail.com>
Date: Sun, 16 Mar 2025 00:20:47 -0400
Subject: [PATCH] [mlir][smt] add export smtlib
---
mlir/include/mlir/InitAllTranslations.h | 5 +
.../include/mlir/Target/SMTLIB/ExportSMTLIB.h | 43 ++
mlir/include/mlir/Target/SMTLIB/Namespace.h | 170 ++++
mlir/include/mlir/Target/SMTLIB/SymCache.h | 133 ++++
mlir/lib/Target/CMakeLists.txt | 1 +
mlir/lib/Target/SMTLIB/CMakeLists.txt | 13 +
mlir/lib/Target/SMTLIB/ExportSMTLIB.cpp | 730 ++++++++++++++++++
mlir/test/Target/SMTLIB/array.mlir | 21 +
mlir/test/Target/SMTLIB/attributes.mlir | 177 +++++
mlir/test/Target/SMTLIB/bitvector-errors.mlir | 7 +
mlir/test/Target/SMTLIB/bitvector.mlir | 213 +++++
mlir/test/Target/SMTLIB/core-errors.mlir | 83 ++
mlir/test/Target/SMTLIB/core.mlir | 137 ++++
mlir/test/Target/SMTLIB/integer-errors.mlir | 7 +
mlir/test/Target/SMTLIB/integer.mlir | 82 ++
15 files changed, 1822 insertions(+)
create mode 100644 mlir/include/mlir/Target/SMTLIB/ExportSMTLIB.h
create mode 100644 mlir/include/mlir/Target/SMTLIB/Namespace.h
create mode 100644 mlir/include/mlir/Target/SMTLIB/SymCache.h
create mode 100644 mlir/lib/Target/SMTLIB/CMakeLists.txt
create mode 100644 mlir/lib/Target/SMTLIB/ExportSMTLIB.cpp
create mode 100644 mlir/test/Target/SMTLIB/array.mlir
create mode 100644 mlir/test/Target/SMTLIB/attributes.mlir
create mode 100644 mlir/test/Target/SMTLIB/bitvector-errors.mlir
create mode 100644 mlir/test/Target/SMTLIB/bitvector.mlir
create mode 100644 mlir/test/Target/SMTLIB/core-errors.mlir
create mode 100644 mlir/test/Target/SMTLIB/core.mlir
create mode 100644 mlir/test/Target/SMTLIB/integer-errors.mlir
create mode 100644 mlir/test/Target/SMTLIB/integer.mlir
diff --git a/mlir/include/mlir/InitAllTranslations.h b/mlir/include/mlir/InitAllTranslations.h
index 50ad3b285ba41..3de3e02ff3f81 100644
--- a/mlir/include/mlir/InitAllTranslations.h
+++ b/mlir/include/mlir/InitAllTranslations.h
@@ -22,6 +22,10 @@ void registerToCppTranslation();
void registerToLLVMIRTranslation();
void registerToSPIRVTranslation();
+namespace smt {
+void registerExportSMTLIBTranslation();
+}
+
// This function should be called before creating any MLIRContext if one
// expects all the possible translations to be made available to the context
// automatically.
@@ -32,6 +36,7 @@ inline void registerAllTranslations() {
registerToCppTranslation();
registerToLLVMIRTranslation();
registerToSPIRVTranslation();
+ smt::registerExportSMTLIBTranslation();
return true;
}();
(void)initOnce;
diff --git a/mlir/include/mlir/Target/SMTLIB/ExportSMTLIB.h b/mlir/include/mlir/Target/SMTLIB/ExportSMTLIB.h
new file mode 100644
index 0000000000000..6415b97167cf7
--- /dev/null
+++ b/mlir/include/mlir/Target/SMTLIB/ExportSMTLIB.h
@@ -0,0 +1,43 @@
+//===- ExportSMTLIB.h - SMT-LIB Exporter ------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// Defines the interface to the SMT-LIB emitter.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef MLIR_TARGET_EXPORTSMTLIB_H
+#define MLIR_TARGET_EXPORTSMTLIB_H
+
+#include "mlir/Support/LLVM.h"
+
+namespace mlir {
+class Operation;
+namespace smt {
+
+/// Emission options for the ExportSMTLIB pass. Allows controlling the emitted
+/// format and overall behavior.
+struct SMTEmissionOptions {
+ // Don't produce 'let' expressions to bind expressions that are only used
+ // once, but inline them directly at the use-site.
+ bool inlineSingleUseValues = false;
+ // Increase indentation for each 'let' expression body.
+ bool indentLetBody = false;
+};
+
+/// Run the ExportSMTLIB pass.
+LogicalResult
+exportSMTLIB(Operation *module, llvm::raw_ostream &os,
+ const SMTEmissionOptions &options = SMTEmissionOptions());
+
+/// Register the ExportSMTLIB pass.
+void registerExportSMTLIBTranslation();
+
+} // namespace smt
+} // namespace mlir
+
+#endif // MLIR_TARGET_EXPORTSMTLIB_H
diff --git a/mlir/include/mlir/Target/SMTLIB/Namespace.h b/mlir/include/mlir/Target/SMTLIB/Namespace.h
new file mode 100644
index 0000000000000..09bd5cd2d407b
--- /dev/null
+++ b/mlir/include/mlir/Target/SMTLIB/Namespace.h
@@ -0,0 +1,170 @@
+//===- Namespace.h - Utilities for generating names -------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This file provides utilities for generating new names that do not conflict
+// with existing names.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef MLIR_SUPPORT_NAMESPACE_H
+#define MLIR_SUPPORT_NAMESPACE_H
+
+#include "mlir/IR/BuiltinOps.h"
+#include "mlir/Target/SMTLIB/SymCache.h"
+#include "llvm/ADT/SmallString.h"
+#include "llvm/ADT/StringSet.h"
+#include "llvm/ADT/Twine.h"
+
+namespace mlir {
+
+/// A namespace that is used to store existing names and generate new names in
+/// some scope within the IR. This exists to work around limitations of
+/// SymbolTables. This acts as a base class providing facilities common to all
+/// namespaces implementations.
+class Namespace {
+public:
+ Namespace() {
+ // This fills an entry for an empty string beforehand so that `newName`
+ // doesn't return an empty string.
+ nextIndex.insert({"", 0});
+ }
+ Namespace(const Namespace &other) = default;
+ Namespace(Namespace &&other)
+ : nextIndex(std::move(other.nextIndex)), locked(other.locked) {}
+
+ Namespace &operator=(const Namespace &other) = default;
+ Namespace &operator=(Namespace &&other) {
+ nextIndex = std::move(other.nextIndex);
+ locked = other.locked;
+ return *this;
+ }
+
+ void add(mlir::ModuleOp module) {
+ assert(module->getNumRegions() == 1);
+ for (auto &op : module.getBody(0)->getOperations())
+ if (auto symbol = op.getAttrOfType<mlir::StringAttr>(
+ mlir::SymbolTable::getSymbolAttrName()))
+ nextIndex.insert({symbol.getValue(), 0});
+ }
+
+ /// SymbolCache initializer; initialize from every key that is convertible to
+ /// a StringAttr in the SymbolCache.
+ void add(SymbolCache &symCache) {
+ for (auto &&[attr, _] : symCache)
+ if (auto strAttr = dyn_cast<mlir::StringAttr>(attr))
+ nextIndex.insert({strAttr.getValue(), 0});
+ }
+
+ void add(llvm::StringRef name) { nextIndex.insert({name, 0}); }
+
+ /// Removes a symbol from the namespace. Returns true if the symbol was
+ /// removed, false if the symbol was not found.
+ /// This is only allowed to be called _before_ any call to newName.
+ bool erase(llvm::StringRef symbol) {
+ assert(!locked && "Cannot erase names from a locked namespace");
+ return nextIndex.erase(symbol);
+ }
+
+ /// Empty the namespace.
+ void clear() {
+ nextIndex.clear();
+ locked = false;
+ }
+
+ /// Return a unique name, derived from the input `name`, and add the new name
+ /// to the internal namespace. There are two possible outcomes for the
+ /// returned name:
+ ///
+ /// 1. The original name is returned.
+ /// 2. The name is given a `_<n>` suffix where `<n>` is a number starting from
+ /// `0` and incrementing by one each time (`_0`, ...).
+ llvm::StringRef newName(const llvm::Twine &name) {
+ locked = true;
+ // Special case the situation where there is no name collision to avoid
+ // messing with the SmallString allocation below.
+ llvm::SmallString<64> tryName;
+ auto inserted = nextIndex.insert({name.toStringRef(tryName), 0});
+ if (inserted.second)
+ return inserted.first->getKey();
+
+ // Try different suffixes until we get a collision-free one.
+ if (tryName.empty())
+ name.toVector(tryName); // toStringRef may leave tryName unfilled
+
+ // Indexes less than nextIndex[tryName] are lready used, so skip them.
+ // Indexes larger than nextIndex[tryName] may be used in another name.
+ size_t &i = nextIndex[tryName];
+ tryName.push_back('_');
+ size_t baseLength = tryName.size();
+ do {
+ tryName.resize(baseLength);
+ llvm::Twine(i++).toVector(tryName); // append integer to tryName
+ inserted = nextIndex.insert({tryName, 0});
+ } while (!inserted.second);
+
+ return inserted.first->getKey();
+ }
+
+ /// Return a unique name, derived from the input `name` and ensure the
+ /// returned name has the input `suffix`. Also add the new name to the
+ /// internal namespace.
+ /// There are two possible outcomes for the returned name:
+ /// 1. The original name + `_<suffix>` is returned.
+ /// 2. The name is given a suffix `_<n>_<suffix>` where `<n>` is a number
+ /// starting from `0` and incrementing by one each time.
+ llvm::StringRef newName(const llvm::Twine &name, const llvm::Twine &suffix) {
+ locked = true;
+ // Special case the situation where there is no name collision to avoid
+ // messing with the SmallString allocation below.
+ llvm::SmallString<64> tryName;
+ auto inserted = nextIndex.insert(
+ {name.concat("_").concat(suffix).toStringRef(tryName), 0});
+ if (inserted.second)
+ return inserted.first->getKey();
+
+ // Try different suffixes until we get a collision-free one.
+ tryName.clear();
+ name.toVector(tryName); // toStringRef may leave tryName unfilled
+ tryName.push_back('_');
+ size_t baseLength = tryName.size();
+
+ // Get the initial number to start from. Since `:` is not a valid character
+ // in a verilog identifier, we use it separate the name and suffix.
+ // Next number for name+suffix is stored with key `name_:suffix`.
+ tryName.push_back(':');
+ suffix.toVector(tryName);
+
+ // Indexes less than nextIndex[tryName] are already used, so skip them.
+ // Indexes larger than nextIndex[tryName] may be used in another name.
+ size_t &i = nextIndex[tryName];
+ do {
+ tryName.resize(baseLength);
+ llvm::Twine(i++).toVector(tryName); // append integer to tryName
+ tryName.push_back('_');
+ suffix.toVector(tryName);
+ inserted = nextIndex.insert({tryName, 0});
+ } while (!inserted.second);
+
+ return inserted.first->getKey();
+ }
+
+protected:
+ // The "next index" that will be tried when trying to unique a string within a
+ // namespace. It follows that all values less than the "next index" value are
+ // already used.
+ llvm::StringMap<size_t> nextIndex;
+
+ // When true, no names can be erased from the namespace. This is to prevent
+ // erasing names after they have been used, thus leaving users of the
+ // namespace in an inconsistent state.
+ bool locked = false;
+};
+
+} // namespace mlir
+
+#endif // MLIR_SUPPORT_NAMESPACE_H
diff --git a/mlir/include/mlir/Target/SMTLIB/SymCache.h b/mlir/include/mlir/Target/SMTLIB/SymCache.h
new file mode 100644
index 0000000000000..ed0bccef0e433
--- /dev/null
+++ b/mlir/include/mlir/Target/SMTLIB/SymCache.h
@@ -0,0 +1,133 @@
+//===- SymCache.h - Declare Symbol Cache ------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This file declares a Symbol Cache.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef MLIR_SUPPORT_SYMCACHE_H
+#define MLIR_SUPPORT_SYMCACHE_H
+
+#include "mlir/IR/SymbolTable.h"
+#include "llvm/ADT/iterator.h"
+#include "llvm/Support/Casting.h"
+
+namespace mlir {
+
+/// Base symbol cache class to allow for cache lookup through a pointer to some
+/// abstract cache. A symbol cache stores lookup tables to make manipulating and
+/// working with the IR more efficient.
+class SymbolCacheBase {
+public:
+ virtual ~SymbolCacheBase();
+
+ /// Defines 'op' as associated with the 'symbol' in the cache.
+ virtual void addDefinition(mlir::Attribute symbol, mlir::Operation *op) = 0;
+
+ /// Adds the symbol-defining 'op' to the cache.
+ void addSymbol(mlir::SymbolOpInterface op) {
+ addDefinition(op.getNameAttr(), op);
+ }
+
+ /// Populate the symbol cache with all symbol-defining operations within the
+ /// 'top' operation.
+ void addDefinitions(mlir::Operation *top);
+
+ /// Lookup a definition for 'symbol' in the cache.
+ virtual mlir::Operation *getDefinition(mlir::Attribute symbol) const = 0;
+
+ /// Lookup a definition for 'symbol' in the cache.
+ mlir::Operation *getDefinition(mlir::FlatSymbolRefAttr symbol) const {
+ return getDefinition(symbol.getAttr());
+ }
+
+ /// Iterator support through a pointer to some abstract cache.
+ /// The implementing cache must provide an iterator that carries values on the
+ /// form of <mlir::Attribute, mlir::Operation*>.
+ using CacheItem = std::pair<mlir::Attribute, mlir::Operation *>;
+ struct CacheIteratorImpl {
+ virtual ~CacheIteratorImpl() {}
+ virtual void operator++() = 0;
+ virtual CacheItem operator*() = 0;
+ virtual bool operator==(CacheIteratorImpl *other) = 0;
+ };
+
+ struct Iterator
+ : public llvm::iterator_facade_base<Iterator, std::forward_iterator_tag,
+ CacheItem> {
+ Iterator(std::unique_ptr<CacheIteratorImpl> &&impl)
+ : impl(std::move(impl)) {}
+ CacheItem operator*() const { return **impl; }
+ using llvm::iterator_facade_base<Iterator, std::forward_iterator_tag,
+ CacheItem>::operator++;
+ bool operator==(const Iterator &other) const {
+ return *impl == other.impl.get();
+ }
+ void operator++() { impl->operator++(); }
+
+ private:
+ std::unique_ptr<CacheIteratorImpl> impl;
+ };
+ virtual Iterator begin() = 0;
+ virtual Iterator end() = 0;
+};
+
+/// Default symbol cache implementation; stores associations between names
+/// (StringAttr's) to mlir::Operation's.
+/// Adding/getting definitions from the symbol cache is not
+/// thread safe. If this is required, synchronizing cache acccess should be
+/// ensured by the caller.
+class SymbolCache : public SymbolCacheBase {
+public:
+ /// In the building phase, add symbols.
+ void addDefinition(mlir::Attribute key, mlir::Operation *op) override {
+ symbolCache.try_emplace(key, op);
+ }
+
+ // Pull in getDefinition(mlir::FlatSymbolRefAttr symbol)
+ using SymbolCacheBase::getDefinition;
+ mlir::Operation *getDefinition(mlir::Attribute attr) const override {
+ auto it = symbolCache.find(attr);
+ if (it == symbolCache.end())
+ return nullptr;
+ return it->second;
+ }
+
+protected:
+ /// This stores a lookup table from symbol attribute to the operation
+ /// that defines it.
+ llvm::DenseMap<mlir::Attribute, mlir::Operation *> symbolCache;
+
+private:
+ /// Iterator support: A simple mapping between decltype(symbolCache)::iterator
+ /// to SymbolCacheBase::Iterator.
+ using Iterator = decltype(symbolCache)::iterator;
+ struct SymbolCacheIteratorImpl : public CacheIteratorImpl {
+ SymbolCacheIteratorImpl(Iterator it) : it(it) {}
+ CacheItem operator*() override { return {it->getFirst(), it->getSecond()}; }
+ void operator++() override { it++; }
+ bool operator==(CacheIteratorImpl *other) override {
+ return it == static_cast<SymbolCacheIteratorImpl *>(other)->it;
+ }
+ Iterator it;
+ };
+
+public:
+ SymbolCacheBase::Iterator begin() override {
+ return SymbolCacheBase::Iterator(
+ std::make_unique<SymbolCacheIteratorImpl>(symbolCache.begin()));
+ }
+ SymbolCacheBase::Iterator end() override {
+ return SymbolCacheBase::Iterator(
+ std::make_unique<SymbolCacheIteratorImpl>(symbolCache.end()));
+ }
+};
+
+} // namespace mlir
+
+#endif // MLIR_SUPPORT_SYMCACHE_H
diff --git a/mlir/lib/Target/CMakeLists.txt b/mlir/lib/Target/CMakeLists.txt
index c3ec1b4f1e3fe..f14ec49b5a0c2 100644
--- a/mlir/lib/Target/CMakeLists.txt
+++ b/mlir/lib/Target/CMakeLists.txt
@@ -2,3 +2,4 @@ add_subdirectory(Cpp)
add_subdirectory(SPIRV)
add_subdirectory(LLVMIR)
add_subdirectory(LLVM)
+add_subdirectory(SMTLIB)
diff --git a/mlir/lib/Target/SMTLIB/CMakeLists.txt b/mlir/lib/Target/SMTLIB/CMakeLists.txt
new file mode 100644
index 0000000000000..1fd965551ae47
--- /dev/null
+++ b/mlir/lib/Target/SMTLIB/CMakeLists.txt
@@ -0,0 +1,13 @@
+add_mlir_translation_library(MLIRExportSMTLIB
+ ExportSMTLIB.cpp
+
+ LINK_COMPONENTS
+ Core
+
+ LINK_LIBS PUBLIC
+ MLIRSMT
+ MLIRSupport
+ MLIRFuncDialect
+ MLIRIR
+ MLIRTranslateLib
+)
diff --git a/mlir/lib/Target/SMTLIB/ExportSMTLIB.cpp b/mlir/lib/Target/SMTLIB/ExportSMTLIB.cpp
new file mode 100644
index 0000000000000..47235c4a5a52e
--- /dev/null
+++ b/mlir/lib/Target/SMTLIB/ExportSMTLIB.cpp
@@ -0,0 +1,730 @@
+//===- ExportSMTLIB.cpp - SMT-LIB Emitter -----=---------------------------===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This is the main SMT-LIB emitter implementation.
+//
+//===----------------------------------------------------------------------===//
+
+#include "mlir/Target/SMTLIB/ExportSMTLIB.h"
+
+#include "mlir/Dialect/Arith/Utils/Utils.h"
+#include "mlir/Dialect/Func/IR/FuncOps.h"
+#include "mlir/Dialect/SMT/IR/SMTOps.h"
+#include "mlir/Dialect/SMT/IR/SMTVisitors.h"
+#include "mlir/Support/IndentedOstream.h"
+#include "mlir/Target/SMTLIB/Namespace.h"
+#include "mlir/Tools/mlir-translate/Translation.h"
+#include "llvm/ADT/ScopedHashTable.h"
+#include "llvm/ADT/StringRef.h"
+#include "llvm/Support/Format.h"
+#include "llvm/Support/raw_ostream.h"
+
+using namespace mlir;
+using namespace smt;
+
+using ValueMap = llvm::ScopedHashTable<mlir::Value, std::string>;
+
+#define DEBUG_TYPE "export-smtlib"
+
+namespace {
+
+/// A visitor to print the SMT dialect types as SMT-LIB formatted sorts.
+/// Printing nested types use recursive calls since nestings of a depth that
+/// could lead to problems should not occur in practice.
+struct TypeVisitor : public smt::SMTTypeVisitor<TypeVisitor, void,
+ mlir::raw_indented_ostream &> {
+ TypeVisitor(const SMTEmissionOptions &options) : options(options) {}
+
+ void visitSMTType(BoolType type, mlir::raw_indented_ostream &stream) {
+ stream << "Bool";
+ }
+
+ void visitSMTType(IntType type, mlir::raw_indented_ostream &stream) {
+ stream << "Int";
+ }
+
+ void visitSMTType(BitVectorType type, mlir::raw_indented_ostream &stream) {
+ stream << "(_ BitVec " << type.getWidth() << ")";
+ }
+
+ void visitSMTType(ArrayType type, mlir::raw_indented_ostream &stream) {
+ stream << "(Array ";
+ dispatchSMTTypeVisitor(type.getDomainType(), stream);
+ stream << " ";
+ dispatchSMTTypeVisitor(type.getRangeType(), stream);
+ stream << ")";
+ }
+
+ void visitSMTType(SMTFuncType type, mlir::raw_indented_ostream &stream) {
+ stream << "(";
+ StringLiteral nextToken = "";
+
+ for (Type domainTy : type.getDomainTypes()) {
+ stream << nextToken;
+ dispatchSMTTypeVisitor(domainTy, stream);
+ nextToken = " ";
+ }
+
+ stream << ") ";
+ dispatchSMTTypeVisitor(type.getRangeType(), stream);
+ }
+
+ void visitSMTType(SortType type, mlir::raw_indented_ostream &stream) {
+ if (!type.getSortParams().empty())
+ stream << "(";
+
+ stream << type.getIdentifier().getValue();
+ for (Type paramTy : type.getSortParams()) {
+ stream << " ";
+ dispatchSMTTypeVisitor(paramTy, stream);
+ }
+
+ if (!type.getSortParams().empty())
+ stream << ")";
+ }
+
+private:
+ // A reference to the emission options for easy use in the visitor methods.
+ [[maybe_unused]] const SMTEmissionOptions &options;
+};
+
+/// Contains the informations passed to the ExpressionVisitor methods. Makes it
+/// easier to add more information.
+struct VisitorInfo {
+ VisitorInfo(mlir::raw_indented_ostream &stream, ValueMap &valueMap)
+ : stream(stream), valueMap(valueMap) {}
+ VisitorInfo(mlir::raw_indented_ostream &stream, ValueMap &valueMap,
+ unsigned indentLevel, unsigned openParens)
+ : stream(stream), valueMap(valueMap), indentLevel(indentLevel),
+ openParens(openParens) {}
+
+ // Stream to print to.
+ mlir::raw_indented_ostream &stream;
+ // Mapping from SSA values to SMT-LIB expressions.
+ ValueMap &valueMap;
+ // Total number of spaces currently indented.
+ unsigned indentLevel = 0;
+ // Number of parentheses that have been opened but not closed yet.
+ unsigned openParens = 0;
+};
+
+/// A visitor to print SMT dialect operations with exactly one result value as
+/// the equivalent operator in SMT-LIB.
+struct ExpressionVisitor
+ : public smt::SMTOpVisitor<ExpressionVisitor, LogicalResult,
+ VisitorInfo &> {
+ using Base =
+ smt::SMTOpVisitor<ExpressionVisitor, LogicalResult, VisitorInfo &>;
+ using Base::visitSMTOp;
+
+ ExpressionVisitor(const SMTEmissionOptions &options, Namespace &names)
+ : options(options), typeVisitor(options), names(names) {}
+
+ LogicalResult dispatchSMTOpVisitor(Operation *op, VisitorInfo &info) {
+ assert(op->getNumResults() == 1 &&
+ "expression op must have exactly one result value");
+
+ // Print the expression inlined if it is only used once and the
+ // corresponding emission option is enabled. This can lead to bad
+ // performance for big inputs since the inlined expression is stored as a
+ // string in the value mapping where otherwise only the symbol names of free
+ // and bound variables are stored, and due to a lot of string concatenation
+ // (thus it's off by default and just intended to print small examples in a
+ // more human-readable format).
+ Value res = op->getResult(0);
+ if (res.hasOneUse() && options.inlineSingleUseValues) {
+ std::string str;
+ llvm::raw_string_ostream sstream(str);
+ mlir::raw_indented_ostream indentedStream(sstream);
+
+ VisitorInfo newInfo(indentedStream, info.valueMap, info.indentLevel,
+ info.openParens);
+ if (failed(Base::dispatchSMTOpVisitor(op, newInfo)))
+ return failure();
+
+ info.valueMap.insert(res, str);
+ return success();
+ }
+
+ // Generate a let binding for the current expression being processed and
+ // store the sybmol in the value map. Indent the expressions for easier
+ // readability.
+ auto name = names.newName("tmp");
+ info.valueMap.insert(res, name.str());
+ info.stream << "(let ((" << name << " ";
+
+ VisitorInfo newInfo(info.stream, info.valueMap,
+ info.indentLevel + 8 + name.size(), 0);
+ if (failed(Base::dispatchSMTOpVisitor(op, newInfo)))
+ return failure();
+
+ info.stream << "))\n";
+
+ if (options.indentLetBody) {
+ // Five spaces to align with the opening parenthesis
+ info.indentLevel += 5;
+ }
+ ++info.openParens;
+ info.stream.indent(info.indentLevel);
+
+ return success();
+ }
+
+ //===--------------------------------------------------------------------===//
+ // Bit-vector theory operation visitors
+ //===--------------------------------------------------------------------===//
+
+ template <typename Op>
+ LogicalResult printBinaryOp(Op op, StringRef name, VisitorInfo &info) {
+ info.stream << "(" << name << " " << info.valueMap.lookup(op.getLhs())
+ << " " << info.valueMap.lookup(op.getRhs()) << ")";
+ return success();
+ }
+
+ template <typename Op>
+ LogicalResult printVariadicOp(Op op, StringRef name, VisitorInfo &info) {
+ info.stream << "(" << name;
+ for (Value val : op.getOperands())
+ info.stream << " " << info.valueMap.lookup(val);
+ info.stream << ")";
+ return success();
+ }
+
+ LogicalResult visitSMTOp(BVNegOp op, VisitorInfo &info) {
+ info.stream << "(bvneg " << info.valueMap.lookup(op.getInput()) << ")";
+ return success();
+ }
+
+ LogicalResult visitSMTOp(BVNotOp op, VisitorInfo &info) {
+ info.stream << "(bvnot " << info.valueMap.lookup(op.getInput()) << ")";
+ return success();
+ }
+
+#define HANDLE_OP(OPTYPE, NAME, KIND) \
+ LogicalResult visitSMTOp(OPTYPE op, VisitorInfo &info) { \
+ return print##KIND##Op(op, NAME, info); \
+ }
+
+ HANDLE_OP(BVAddOp, "bvadd", Binary);
+ HANDLE_OP(BVMulOp, "bvmul", Binary);
+ HANDLE_OP(BVURemOp, "bvurem", Binary);
+ HANDLE_OP(BVSRemOp, "bvsrem", Binary);
+ HANDLE_OP(BVSModOp, "bvsmod", Binary);
+ HANDLE_OP(BVShlOp, "bvshl", Binary);
+ HANDLE_OP(BVLShrOp, "bvlshr", Binary);
+ HANDLE_OP(BVAShrOp, "bvashr", Binary);
+ HANDLE_OP(BVUDivOp, "bvudiv", Binary);
+ HANDLE_OP(BVSDivOp, "bvsdiv", Binary);
+ HANDLE_OP(BVAndOp, "bvand", Binary);
+ HANDLE_OP(BVOrOp, "bvor", Binary);
+ HANDLE_OP(BVXOrOp, "bvxor", Binary);
+ HANDLE_OP(ConcatOp, "concat", Binary);
+
+ LogicalResult visitSMTOp(ExtractOp op, VisitorInfo &info) {
+ info.stream << "((_ extract "
+ << (op.getLowBit() + op.getType().getWidth() - 1) << " "
+ << op.getLowBit() << ") " << info.valueMap.lookup(op.getInput())
+ << ")";
+ return success();
+ }
+
+ LogicalResult visitSMTOp(RepeatOp op, VisitorInfo &info) {
+ info.stream << "((_ repeat " << op.getCount() << ") "
+ << info.valueMap.lookup(op.getInput()) << ")";
+ return success();
+ }
+
+ LogicalResult visitSMTOp(BVCmpOp op, VisitorInfo &info) {
+ return printBinaryOp(op, "bv" + stringifyBVCmpPredicate(op.getPred()).str(),
+ info);
+ }
+
+ //===--------------------------------------------------------------------===//
+ // Int theory operation visitors
+ //===--------------------------------------------------------------------===//
+
+ HANDLE_OP(IntAddOp, "+", Variadic);
+ HANDLE_OP(IntMulOp, "*", Variadic);
+ HANDLE_OP(IntSubOp, "-", Binary);
+ HANDLE_OP(IntDivOp, "div", Binary);
+ HANDLE_OP(IntModOp, "mod", Binary);
+
+ LogicalResult visitSMTOp(IntCmpOp op, VisitorInfo &info) {
+ switch (op.getPred()) {
+ case IntPredicate::ge:
+ return printBinaryOp(op, ">=", info);
+ case IntPredicate::le:
+ return printBinaryOp(op, "<=", info);
+ case IntPredicate::gt:
+ return printBinaryOp(op, ">", info);
+ case IntPredicate::lt:
+ return printBinaryOp(op, "<", info);
+ }
+ return failure();
+ }
+
+ //===--------------------------------------------------------------------===//
+ // Core theory operation visitors
+ //===--------------------------------------------------------------------===//
+
+ HANDLE_OP(EqOp, "=", Variadic);
+ HANDLE_OP(DistinctOp, "distinct", Variadic);
+
+ LogicalResult visitSMTOp(IteOp op, VisitorInfo &info) {
+ info.stream << "(ite " << info.valueMap.lookup(op.getCond()) << " "
+ << info.valueMap.lookup(op.getThenValue()) << " "
+ << info.valueMap.lookup(op.getElseValue()) << ")";
+ return success();
+ }
+
+ LogicalResult visitSMTOp(ApplyFuncOp op, VisitorInfo &info) {
+ info.stream << "(" << info.valueMap.lookup(op.getFunc());
+ for (Value arg : op.getArgs())
+ info.stream << " " << info.valueMap.lookup(arg);
+ info.stream << ")";
+ return success();
+ }
+
+ template <typename OpTy>
+ LogicalResult quantifierHelper(OpTy op, StringRef operatorString,
+ VisitorInfo &info) {
+ auto weight = op.getWeight();
+ auto patterns = op.getPatterns();
+ // TODO: add support
+ if (op.getNoPattern())
+ return op.emitError() << "no-pattern attribute not supported yet";
+
+ llvm::ScopedHashTableScope<Value, std::string> scope(info.valueMap);
+ info.stream << "(" << operatorString << " (";
+ StringLiteral delimiter = "";
+
+ SmallVector<StringRef> argNames;
+
+ for (auto [i, arg] : llvm::enumerate(op.getBody().getArguments())) {
+ // Generate and register a new unique name.
+ StringRef prefix =
+ op.getBoundVarNames()
+ ? cast<StringAttr>(op.getBoundVarNames()->getValue()[i])
+ .getValue()
+ : "tmp";
+ StringRef name = names.newName(prefix);
+ argNames.push_back(name);
+
+ info.valueMap.insert(arg, name.str());
+
+ // Print the bound variable declaration.
+ info.stream << delimiter << "(" << name << " ";
+ typeVisitor.dispatchSMTTypeVisitor(arg.getType(), info.stream);
+ info.stream << ")";
+ delimiter = " ";
+ }
+
+ info.stream << ")\n";
+
+ // Print the quantifier body. This assumes that quantifiers are not deeply
+ // nested (at least not enough that recursive calls could become a problem).
+
+ SmallVector<Value> worklist;
+ Value yieldedValue = op.getBody().front().getTerminator()->getOperand(0);
+ worklist.push_back(yieldedValue);
+ unsigned indentExt = operatorString.size() + 2;
+ VisitorInfo newInfo(info.stream, info.valueMap,
+ info.indentLevel + indentExt, 0);
+ if (weight != 0 || !patterns.empty())
+ newInfo.stream.indent(newInfo.indentLevel);
+ else
+ newInfo.stream.indent(info.indentLevel);
+
+ if (weight != 0 || !patterns.empty())
+ info.stream << "( ! ";
+
+ if (failed(printExpression(worklist, newInfo)))
+ return failure();
+
+ info.stream << info.valueMap.lookup(yieldedValue);
+
+ for (unsigned j = 0; j < newInfo.openParens; ++j)
+ info.stream << ")";
+
+ if (weight != 0)
+ info.stream << " :weight " << weight;
+ if (!patterns.empty()) {
+ bool first = true;
+ info.stream << "\n:pattern (";
+ for (auto &p : patterns) {
+
+ if (!first)
+ info.stream << " ";
+
+ // retrieve argument name from the body region
+ for (auto [i, arg] : llvm::enumerate(p.getArguments()))
+ info.valueMap.insert(arg, argNames[i].str());
+
+ SmallVector<Value> worklist;
+
+ // retrieve all yielded operands in pattern region
+ for (auto yieldedValue : p.front().getTerminator()->getOperands()) {
+
+ worklist.push_back(yieldedValue);
+ unsigned indentExt = operatorString.size() + 2;
+
+ VisitorInfo newInfo2(info.stream, info.valueMap,
+ info.indentLevel + indentExt, 0);
+
+ info.stream.indent(0);
+
+ if (failed(printExpression(worklist, newInfo2)))
+ return failure();
+
+ info.stream << info.valueMap.lookup(yieldedValue);
+ for (unsigned j = 0; j < newInfo2.openParens; ++j)
+ info.stream << ")";
+ }
+
+ first = false;
+ }
+ info.stream << ")";
+ }
+
+ if (weight != 0 || !patterns.empty())
+ info.stream << ")";
+
+ info.stream << ")";
+
+ return success();
+ }
+
+ LogicalResult visitSMTOp(ForallOp op, VisitorInfo &info) {
+ return quantifierHelper(op, "forall", info);
+ }
+
+ LogicalResult visitSMTOp(ExistsOp op, VisitorInfo &info) {
+ return quantifierHelper(op, "exists", info);
+ }
+
+ LogicalResult visitSMTOp(NotOp op, VisitorInfo &info) {
+ info.stream << "(not " << info.valueMap.lookup(op.getInput()) << ")";
+ return success();
+ }
+
+ HANDLE_OP(AndOp, "and", Variadic);
+ HANDLE_OP(OrOp, "or", Variadic);
+ HANDLE_OP(XOrOp, "xor", Variadic);
+ HANDLE_OP(ImpliesOp, "=>", Binary);
+
+ //===--------------------------------------------------------------------===//
+ // Array theory operation visitors
+ //===--------------------------------------------------------------------===//
+
+ LogicalResult visitSMTOp(ArrayStoreOp op, VisitorInfo &info) {
+ info.stream << "(store " << info.valueMap.lookup(op.getArray()) << " "
+ << info.valueMap.lookup(op.getIndex()) << " "
+ << info.valueMap.lookup(op.getValue()) << ")";
+ return success();
+ }
+
+ LogicalResult visitSMTOp(ArraySelectOp op, VisitorInfo &info) {
+ info.stream << "(select " << info.valueMap.lookup(op.getArray()) << " "
+ << info.valueMap.lookup(op.getIndex()) << ")";
+ return success();
+ }
+
+ LogicalResult visitSMTOp(ArrayBroadcastOp op, VisitorInfo &info) {
+ info.stream << "((as const ";
+ typeVisitor.dispatchSMTTypeVisitor(op.getType(), info.stream);
+ info.stream << ") " << info.valueMap.lookup(op.getValue()) << ")";
+ return success();
+ }
+
+ LogicalResult visitUnhandledSMTOp(Operation *op, VisitorInfo &info) {
+ return success();
+ }
+
+#undef HANDLE_OP
+
+ /// Print an expression transitively. The root node should be added to the
+ /// 'worklist' before calling.
+ LogicalResult printExpression(SmallVector<Value> &worklist,
+ VisitorInfo &info) {
+ while (!worklist.empty()) {
+ Value curr = worklist.back();
+
+ // If we already have a let-binding for the value, just print it.
+ if (info.valueMap.count(curr)) {
+ worklist.pop_back();
+ continue;
+ }
+
+ // Traverse until we reach a value/operation that has all operands
+ // available and can thus be printed.
+ bool allAvailable = true;
+ Operation *defOp = curr.getDefiningOp();
+ assert(defOp != nullptr &&
+ "block arguments must already be in the valueMap");
+
+ for (Value val : defOp->getOperands()) {
+ if (!info.valueMap.count(val)) {
+ worklist.push_back(val);
+ allAvailable = false;
+ }
+ }
+
+ if (!allAvailable)
+ continue;
+
+ if (failed(dispatchSMTOpVisitor(curr.getDefiningOp(), info)))
+ return failure();
+
+ worklist.pop_back();
+ }
+
+ return success();
+ }
+
+private:
+ // A reference to the emission options for easy use in the visitor methods.
+ [[maybe_unused]] const SMTEmissionOptions &options;
+ TypeVisitor typeVisitor;
+ Namespace &names;
+};
+
+/// A visitor to print SMT dialect operations with zero result values or
+/// ones that have to initialize some global state.
+struct StatementVisitor
+ : public smt::SMTOpVisitor<StatementVisitor, LogicalResult,
+ mlir::raw_indented_ostream &, ValueMap &> {
+ using smt::SMTOpVisitor<StatementVisitor, LogicalResult,
+ mlir::raw_indented_ostream &, ValueMap &>::visitSMTOp;
+
+ StatementVisitor(const SMTEmissionOptions &options, Namespace &names)
+ : options(options), typeVisitor(options), names(names),
+ exprVisitor(options, names) {}
+
+ LogicalResult visitSMTOp(BVConstantOp op, mlir::raw_indented_ostream &stream,
+ ValueMap &valueMap) {
+ valueMap.insert(op.getResult(), op.getValue().getValueAsString());
+ return success();
+ }
+
+ LogicalResult visitSMTOp(BoolConstantOp op,
+ mlir::raw_indented_ostream &stream,
+ ValueMap &valueMap) {
+ valueMap.insert(op.getResult(), op.getValue() ? "true" : "false");
+ return success();
+ }
+
+ LogicalResult visitSMTOp(IntConstantOp op, mlir::raw_indented_ostream &stream,
+ ValueMap &valueMap) {
+ SmallString<16> str;
+ op.getValue().toStringSigned(str);
+ valueMap.insert(op.getResult(), str.str().str());
+ return success();
+ }
+
+ LogicalResult visitSMTOp(DeclareFunOp op, mlir::raw_indented_ostream &stream,
+ ValueMap &valueMap) {
+ StringRef name =
+ names.newName(op.getNamePrefix() ? *op.getNamePrefix() : "tmp");
+ valueMap.insert(op.getResult(), name.str());
+ stream << "("
+ << (isa<SMTFuncType>(op.getType()) ? "declare-fun "
+ : "declare-const ")
+ << name << " ";
+ typeVisitor.dispatchSMTTypeVisitor(op.getType(), stream);
+ stream << ")\n";
+ return success();
+ }
+
+ LogicalResult visitSMTOp(AssertOp op, mlir::raw_indented_ostream &stream,
+ ValueMap &valueMap) {
+ llvm::ScopedHashTableScope<Value, std::string> scope1(valueMap);
+ SmallVector<Value> worklist;
+ worklist.push_back(op.getInput());
+ stream << "(assert ";
+ VisitorInfo info(stream, valueMap, 8, 0);
+ if (failed(exprVisitor.printExpression(worklist, info)))
+ return failure();
+ stream << valueMap.lookup(op.getInput());
+ for (unsigned i = 0; i < info.openParens + 1; ++i)
+ stream << ")";
+ stream << "\n";
+ stream.indent(0);
+ return success();
+ }
+
+ LogicalResult visitSMTOp(ResetOp op, mlir::raw_indented_ostream &stream,
+ ValueMap &valueMap) {
+ stream << "(reset)\n";
+ return success();
+ }
+
+ LogicalResult visitSMTOp(PushOp op, mlir::raw_indented_ostream &stream,
+ ValueMap &valueMap) {
+ stream << "(push " << op.getCount() << ")\n";
+ return success();
+ }
+
+ LogicalResult visitSMTOp(PopOp op, mlir::raw_indented_ostream &stream,
+ ValueMap &valueMap) {
+ stream << "(pop " << op.getCount() << ")\n";
+ return success();
+ }
+
+ LogicalResult visitSMTOp(CheckOp op, mlir::raw_indented_ostream &stream,
+ ValueMap &valueMap) {
+ if (op->getNumResults() != 0)
+ return op.emitError() << "must not have any result values";
+
+ if (op.getSatRegion().front().getOperations().size() != 1)
+ return op->emitError() << "'sat' region must be empty";
+ if (op.getUnknownRegion().front().getOperations().size() != 1)
+ return op->emitError() << "'unknown' region must be empty";
+ if (op.getUnsatRegion().front().getOperations().size() != 1)
+ return op->emitError() << "'unsat' region must be empty";
+
+ stream << "(check-sat)\n";
+ return success();
+ }
+
+ LogicalResult visitSMTOp(SetLogicOp op, mlir::raw_indented_ostream &stream,
+ ValueMap &valueMap) {
+ stream << "(set-logic " << op.getLogic() << ")\n";
+ return success();
+ }
+
+ LogicalResult visitUnhandledSMTOp(Operation *op,
+ mlir::raw_indented_ostream &stream,
+ ValueMap &valueMap) {
+ // Ignore operations which are handled in the Expression Visitor.
+ if (isa<smt::Int2BVOp, BV2IntOp>(op))
+ return op->emitError("operation not supported for SMTLIB emission");
+
+ return success();
+ }
+
+private:
+ // A reference to the emission options for easy use in the visitor methods.
+ [[maybe_unused]] const SMTEmissionOptions &options;
+ TypeVisitor typeVisitor;
+ Namespace &names;
+ ExpressionVisitor exprVisitor;
+};
+
+} // namespace
+
+//===----------------------------------------------------------------------===//
+// Unified Emitter implementation
+//===----------------------------------------------------------------------===//
+
+/// Emit the SMT operations in the given 'solver' to the 'stream'.
+static LogicalResult emit(SolverOp solver, const SMTEmissionOptions &options,
+ mlir::raw_indented_ostream &stream) {
+ if (!solver.getInputs().empty() || solver->getNumResults() != 0)
+ return solver->emitError()
+ << "solver scopes with inputs or results are not supported";
+
+ Block *block = solver.getBody();
+
+ // Declare uninterpreted sorts.
+ DenseMap<StringAttr, unsigned> declaredSorts;
+ auto result = block->walk([&](Operation *op) -> WalkResult {
+ if (!isa<SMTDialect>(op->getDialect()))
+ return op->emitError()
+ << "solver must not contain any non-SMT operations";
+
+ for (Type resTy : op->getResultTypes()) {
+ auto sortTy = dyn_cast<SortType>(resTy);
+ if (!sortTy)
+ continue;
+
+ unsigned arity = sortTy.getSortParams().size();
+ if (declaredSorts.contains(sortTy.getIdentifier())) {
+ if (declaredSorts[sortTy.getIdentifier()] != arity)
+ return op->emitError("uninterpreted sorts with same identifier but "
+ "different arity found");
+
+ continue;
+ }
+
+ declaredSorts[sortTy.getIdentifier()] = arity;
+ stream << "(declare-sort " << sortTy.getIdentifier().getValue() << " "
+ << arity << ")\n";
+ }
+ return WalkResult::advance();
+ });
+ if (result.wasInterrupted())
+ return failure();
+
+ ValueMap valueMap;
+ llvm::ScopedHashTableScope<Value, std::string> scope0(valueMap);
+ Namespace names;
+ StatementVisitor visitor(options, names);
+
+ // Collect all statement operations (ops with no result value).
+ // Declare constants and then only refer to them by identifier later on.
+ result = block->walk([&](Operation *op) {
+ if (failed(visitor.dispatchSMTOpVisitor(op, stream, valueMap)))
+ return WalkResult::interrupt();
+ return WalkResult::advance();
+ });
+ if (result.wasInterrupted())
+ return failure();
+
+ stream << "(reset)\n";
+ return success();
+}
+
+LogicalResult smt::exportSMTLIB(Operation *module, llvm::raw_ostream &os,
+ const SMTEmissionOptions &options) {
+ if (module->getNumRegions() != 1)
+ return module->emitError("must have exactly one region");
+ if (!module->getRegion(0).hasOneBlock())
+ return module->emitError("op region must have exactly one block");
+
+ mlir::raw_indented_ostream ios(os);
+ unsigned solverIdx = 0;
+ auto result = module->walk([&](SolverOp solver) {
+ ios << "; solver scope " << solverIdx << "\n";
+ if (failed(emit(solver, options, ios)))
+ return WalkResult::interrupt();
+ ++solverIdx;
+ return WalkResult::advance();
+ });
+
+ return failure(result.wasInterrupted());
+}
+
+//===----------------------------------------------------------------------===//
+// mlir-translate registration
+//===----------------------------------------------------------------------===//
+
+void smt::registerExportSMTLIBTranslation() {
+ static llvm::cl::opt<bool> inlineSingleUseValues(
+ "smtlibexport-inline-single-use-values",
+ llvm::cl::desc("Inline expressions that are used only once rather than "
+ "generating a let-binding"),
+ llvm::cl::init(false));
+
+ auto getOptions = [] {
+ SMTEmissionOptions opts;
+ opts.inlineSingleUseValues = inlineSingleUseValues;
+ return opts;
+ };
+
+ static mlir::TranslateFromMLIRRegistration toSMTLIB(
+ "export-smtlib", "export SMT-LIB",
+ [=](Operation *module, raw_ostream &output) {
+ return smt::exportSMTLIB(module, output, getOptions());
+ },
+ [](mlir::DialectRegistry ®istry) {
+ // Register the 'func' and 'HW' dialects to support printing solver
+ // scopes nested in functions and modules.
+ registry.insert<mlir::func::FuncDialect, arith::ArithDialect,
+ smt::SMTDialect>();
+ });
+}
diff --git a/mlir/test/Target/SMTLIB/array.mlir b/mlir/test/Target/SMTLIB/array.mlir
new file mode 100644
index 0000000000000..6d289eff1ea3d
--- /dev/null
+++ b/mlir/test/Target/SMTLIB/array.mlir
@@ -0,0 +1,21 @@
+// RUN: mlir-translate --export-smtlib %s | FileCheck %s
+// RUN: mlir-translate --export-smtlib --smtlibexport-inline-single-use-values %s | FileCheck %s --check-prefix=CHECK-INLINED
+
+smt.solver () : () -> () {
+ %c = smt.int.constant 0
+ %true = smt.constant true
+
+ // CHECK: (assert (let (([[V0:.+]] ((as const (Array Int Bool)) true)))
+ // CHECK: (let (([[V1:.+]] (store [[V0]] 0 true)))
+ // CHECK: (let (([[V2:.+]] (select [[V1]] 0)))
+ // CHECK: [[V2]]))))
+
+ // CHECK-INLINED: (assert (select (store ((as const (Array Int Bool)) true) 0 true) 0))
+ %0 = smt.array.broadcast %true : !smt.array<[!smt.int -> !smt.bool]>
+ %1 = smt.array.store %0[%c], %true : !smt.array<[!smt.int -> !smt.bool]>
+ %2 = smt.array.select %1[%c] : !smt.array<[!smt.int -> !smt.bool]>
+ smt.assert %2
+
+ // CHECK: (reset)
+ // CHECK-INLINED: (reset)
+}
diff --git a/mlir/test/Target/SMTLIB/attributes.mlir b/mlir/test/Target/SMTLIB/attributes.mlir
new file mode 100644
index 0000000000000..2f534497d0afa
--- /dev/null
+++ b/mlir/test/Target/SMTLIB/attributes.mlir
@@ -0,0 +1,177 @@
+// RUN: mlir-translate --export-smtlib %s | FileCheck %s
+// RUN: mlir-translate --export-smtlib --smtlibexport-inline-single-use-values %s | FileCheck %s --check-prefix=CHECK-INLINED
+
+smt.solver () : () -> () {
+
+ %true = smt.constant true
+
+
+ // CHECK: (assert (let (([[V10:.+]] (forall (([[A:.+]] Int) ([[B:.+]] Int))
+ // CHECK: ( ! (let (([[V11:.+]] (= [[A]] [[B]])))
+ // CHECK: [[V11]]) :weight 2))))
+ // CHECK: [[V10]]))
+
+ // CHECK-INLINED: (assert (forall (([[A:.+]] Int) ([[B:.+]] Int))
+ // CHECK-INLINED: ( ! (= [[A]] [[B]]) :weight 2)))
+ %1 = smt.forall ["a", "b"] weight 2 {
+ ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+ %2 = smt.eq %arg2, %arg3 : !smt.int
+ smt.yield %2 : !smt.bool
+ }
+ smt.assert %1
+
+
+ // CHECK: (assert (let (([[V12:.+]] (exists (([[V13:.+]] Int) ([[V14:.+]] Int))
+ // CHECK: ( ! (let (([[V15:.+]] (= [[V13]] [[V14]])))
+ // CHECK: [[V15]]) :weight 2))))
+ // CHECK: [[V12]]))
+
+ // CHECK-INLINED: (assert (exists (([[A:.+]] Int) ([[B:.+]] Int))
+ // CHECK-INLINED: ( ! (= [[A]] [[B]]) :weight 2)))
+
+ %2 = smt.exists weight 2 {
+ ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+ %3 = smt.eq %arg2, %arg3 : !smt.int
+ smt.yield %3 : !smt.bool
+ }
+ smt.assert %2
+
+
+
+ // CHECK: (assert (let (([[V16:.+]] (exists (([[V17:.+]] Int) ([[V18:.+]] Int))
+ // CHECK: ( ! (let (([[V19:.+]] (= [[V17]] [[V18]])))
+ // CHECK: (let (([[V20:.+]] (=> [[V19:.+]] true)))
+ // CHECK: [[V20:.+]])) :weight 2))))
+ // CHECK: [[V16]])){{$}}
+
+ // CHECK-INLINED: (assert (exists (([[A:.+]] Int) ([[B:.+]] Int))
+ // CHECK-INLINED: ( ! (=> (= [[A]] [[B]]) true) :weight 2)))
+
+ %3 = smt.exists weight 2 {
+ ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+ %4 = smt.eq %arg2, %arg3 : !smt.int
+ %5 = smt.implies %4, %true
+ smt.yield %5 : !smt.bool
+ }
+ smt.assert %3
+
+
+ // CHECK: (assert (let (([[V21:.+]] (exists (([[V22:.+]] Int) ([[V23:.+]] Int))
+ // CHECK: ( ! (let (([[V24:.+]] (= [[V22]] [[V23]])))
+ // CHECK: (let (([[V25:.+]] (=> [[V24]] true)))
+ // CHECK: [[V25]]))
+ // CHECK: :pattern ((let (([[V26:.+]] (= [[V22]] [[V23]])))
+ // CHECK: [[V26]]))))))
+ // CHECK: [[V21]])){{$}}
+
+ // CHECK-INLINED: (assert (exists (([[A:.+]] Int) ([[B:.+]] Int))
+ // CHECK-INLINED: ( ! (=> (= [[A]] [[B]]) true)
+ // CHECK-INLINED: :pattern ((= [[A]] [[B]])))))
+
+ %6 = smt.exists {
+ ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+ %4 = smt.eq %arg2, %arg3 : !smt.int
+ %5 = smt.implies %4, %true
+ smt.yield %5 : !smt.bool
+ } patterns {
+ ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+ %4 = smt.eq %arg2, %arg3 : !smt.int
+ smt.yield %4: !smt.bool
+ }
+ smt.assert %6
+
+ // CHECK: (assert (let (([[V27:.+]] (exists (([[V28:.+]] Int) ([[V29:.+]] Int))
+ // CHECK: ( ! (let (([[V30:.+]] (= [[V28]] [[V29]])))
+ // CHECK: (let (([[V31:.+]] (=> [[V30]] true)))
+ // CHECK: [[V31]])) :weight 2
+ // CHECK: :pattern ((let (([[V32:.+]] (= [[V28]] [[V29]])))
+ // CHECK: [[V32]]))))))
+ // CHECK: [[V27]])){{$}}
+
+ // CHECK-INLINED: (assert (exists (([[A:.+]] Int) ([[B:.+]] Int))
+ // CHECK-INLINED: ( ! (=> (= [[A]] [[B]]) true) :weight 2
+ // CHECK-INLINED: :pattern ((= [[A]] [[B]])))))
+
+ %7 = smt.exists weight 2 {
+ ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+ %4 = smt.eq %arg2, %arg3 : !smt.int
+ %5 = smt.implies %4, %true
+ smt.yield %5 : !smt.bool
+ } patterns {
+ ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+ %4 = smt.eq %arg2, %arg3 : !smt.int
+ smt.yield %4: !smt.bool
+ }
+ smt.assert %7
+
+ // CHECK: (assert (let (([[V33:.+]] (exists (([[V34:.+]] Int) ([[V35:.+]] Int))
+ // CHECK: ( ! (let (([[V36:.+]] (= [[V35]] 4)))
+ // CHECK: (let (([[V37:.+]] (= [[V34]] 3)))
+ // CHECK: (let (([[V38:.+]] (= [[V37]] [[V36]])))
+ // CHECK: [[V38]])))
+ // CHECK: :pattern ((let (([[V39:.+]] (= [[V34]] 3)))
+ // CHECK: [[V39]]) (let (([[V40:.+]] (= [[V35]] 4)))
+ // CHECK: [[V40]]))))))
+ // CHECK: [[V33]])){{$}}
+
+ // CHECK-INLINED: (assert (exists (([[A:.+]] Int) ([[B:.+]] Int))
+ // CHECK-INLINED: ( ! (= (= [[A]] 3) (= [[B]] 4))
+ // CHECK-INLINED: :pattern ((= [[A]] 3) (= [[B]] 4)))))
+
+
+ %three = smt.int.constant 3
+ %four = smt.int.constant 4
+
+ %8 = smt.exists {
+ ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+ %4 = smt.eq %arg2, %three: !smt.int
+ %5 = smt.eq %arg3, %four: !smt.int
+ %9 = smt.eq %4, %5: !smt.bool
+ smt.yield %9 : !smt.bool
+ } patterns {
+ ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+ %4 = smt.eq %arg2, %three: !smt.int
+ smt.yield %4: !smt.bool
+ }, {
+ ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+ %5 = smt.eq %arg3, %four: !smt.int
+ smt.yield %5: !smt.bool
+ }
+ smt.assert %8
+
+ smt.check sat {} unknown {} unsat {}
+
+ // CHECK: (assert (let (([[V41:.+]] (exists (([[V42:.+]] Int) ([[V43:.+]] Int))
+ // CHECK: ( ! (let (([[V44:.+]] (= [[V43]] 4)))
+ // CHECK: (let (([[V45:.+]] (= [[V42]] 3)))
+ // CHECK: (let (([[V46:.+]] (= [[V45]] [[V44]])))
+ // CHECK: [[V46]])))
+ // CHECK: :pattern ((let (([[V47:.+]] (= [[V42]] 3)))
+ // CHECK: [[V47]])(let (([[V48:.+]] (= [[V43]] 4)))
+ // CHECK: [[V48]]))))))
+ // CHECK: [[V41]])){{$}}
+
+ // CHECK-INLINED: (assert (exists (([[A:.+]] Int) ([[B:.+]] Int))
+ // CHECK-INLINED: ( ! (= (= [[A]] 3) (= [[B]] 4))
+ // CHECK-INLINED: :pattern ((= [[A]] 3)(= [[B]] 4)))))
+
+ %10 = smt.exists {
+ ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+ %4 = smt.eq %arg2, %three: !smt.int
+ %5 = smt.eq %arg3, %four: !smt.int
+ %9 = smt.eq %4, %5: !smt.bool
+ smt.yield %9 : !smt.bool
+ } patterns {
+ ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+ %4 = smt.eq %arg2, %three: !smt.int
+ %5 = smt.eq %arg3, %four: !smt.int
+ smt.yield %4, %5: !smt.bool, !smt.bool
+ }
+ smt.assert %10
+
+ smt.check sat {} unknown {} unsat {}
+
+ // CHECK: (reset)
+ // CHECK-INLINED: (reset)
+
+}
diff --git a/mlir/test/Target/SMTLIB/bitvector-errors.mlir b/mlir/test/Target/SMTLIB/bitvector-errors.mlir
new file mode 100644
index 0000000000000..ae403b0b59369
--- /dev/null
+++ b/mlir/test/Target/SMTLIB/bitvector-errors.mlir
@@ -0,0 +1,7 @@
+// RUN: mlir-translate --export-smtlib %s --split-input-file --verify-diagnostics
+
+smt.solver () : () -> () {
+ %0 = smt.bv.constant #smt.bv<5> : !smt.bv<16>
+ // expected-error @below {{operation not supported for SMTLIB emission}}
+ %1 = smt.bv2int %0 signed : !smt.bv<16>
+}
diff --git a/mlir/test/Target/SMTLIB/bitvector.mlir b/mlir/test/Target/SMTLIB/bitvector.mlir
new file mode 100644
index 0000000000000..c58992769d9b1
--- /dev/null
+++ b/mlir/test/Target/SMTLIB/bitvector.mlir
@@ -0,0 +1,213 @@
+// RUN: mlir-translate --export-smtlib %s | FileCheck %s
+// RUN: mlir-translate --export-smtlib --smtlibexport-inline-single-use-values %s | FileCheck %s --check-prefix=CHECK-INLINED
+
+smt.solver () : () -> () {
+ %c0_bv32 = smt.bv.constant #smt.bv<0> : !smt.bv<32>
+
+ // CHECK: (assert (let (([[V0:.+]] (bvneg #x00000000)))
+ // CHECK: (let (([[V1:.+]] (= [[V0]] #x00000000)))
+ // CHECK: [[V1]])))
+
+ // CHECK-INLINED: (assert (= (bvneg #x00000000) #x00000000))
+ %0 = smt.bv.neg %c0_bv32 : !smt.bv<32>
+ %a0 = smt.eq %0, %c0_bv32 : !smt.bv<32>
+ smt.assert %a0
+
+ // CHECK: (assert (let (([[V2:.+]] (bvadd #x00000000 #x00000000)))
+ // CHECK: (let (([[V3:.+]] (= [[V2]] #x00000000)))
+ // CHECK: [[V3]])))
+
+ // CHECK-INLINED: (assert (= (bvadd #x00000000 #x00000000) #x00000000))
+ %1 = smt.bv.add %c0_bv32, %c0_bv32 : !smt.bv<32>
+ %a1 = smt.eq %1, %c0_bv32 : !smt.bv<32>
+ smt.assert %a1
+
+ // CHECK: (assert (let (([[V4:.+]] (bvmul #x00000000 #x00000000)))
+ // CHECK: (let (([[V5:.+]] (= [[V4]] #x00000000)))
+ // CHECK: [[V5]])))
+
+ // CHECK-INLINED: (assert (= (bvmul #x00000000 #x00000000) #x00000000))
+ %3 = smt.bv.mul %c0_bv32, %c0_bv32 : !smt.bv<32>
+ %a3 = smt.eq %3, %c0_bv32 : !smt.bv<32>
+ smt.assert %a3
+
+ // CHECK: (assert (let (([[V6:.+]] (bvurem #x00000000 #x00000000)))
+ // CHECK: (let (([[V7:.+]] (= [[V6]] #x00000000)))
+ // CHECK: [[V7]])))
+
+ // CHECK-INLINED: (assert (= (bvurem #x00000000 #x00000000) #x00000000))
+ %4 = smt.bv.urem %c0_bv32, %c0_bv32 : !smt.bv<32>
+ %a4 = smt.eq %4, %c0_bv32 : !smt.bv<32>
+ smt.assert %a4
+
+ // CHECK: (assert (let (([[V8:.+]] (bvsrem #x00000000 #x00000000)))
+ // CHECK: (let (([[V9:.+]] (= [[V8]] #x00000000)))
+ // CHECK: [[V9]])))
+
+ // CHECK-INLINED: (assert (= (bvsrem #x00000000 #x00000000) #x00000000))
+ %5 = smt.bv.srem %c0_bv32, %c0_bv32 : !smt.bv<32>
+ %a5 = smt.eq %5, %c0_bv32 : !smt.bv<32>
+ smt.assert %a5
+
+ // CHECK: (assert (let (([[V10:.+]] (bvsmod #x00000000 #x00000000)))
+ // CHECK: (let (([[V11:.+]] (= [[V10]] #x00000000)))
+ // CHECK: [[V11]])))
+
+ // CHECK-INLINED: (assert (= (bvsmod #x00000000 #x00000000) #x00000000))
+ %7 = smt.bv.smod %c0_bv32, %c0_bv32 : !smt.bv<32>
+ %a7 = smt.eq %7, %c0_bv32 : !smt.bv<32>
+ smt.assert %a7
+
+ // CHECK: (assert (let (([[V12:.+]] (bvshl #x00000000 #x00000000)))
+ // CHECK: (let (([[V13:.+]] (= [[V12]] #x00000000)))
+ // CHECK: [[V13]])))
+
+ // CHECK-INLINED: (assert (= (bvshl #x00000000 #x00000000) #x00000000))
+ %8 = smt.bv.shl %c0_bv32, %c0_bv32 : !smt.bv<32>
+ %a8 = smt.eq %8, %c0_bv32 : !smt.bv<32>
+ smt.assert %a8
+
+ // CHECK: (assert (let (([[V14:.+]] (bvlshr #x00000000 #x00000000)))
+ // CHECK: (let (([[V15:.+]] (= [[V14]] #x00000000)))
+ // CHECK: [[V15]])))
+
+ // CHECK-INLINED: (assert (= (bvlshr #x00000000 #x00000000) #x00000000))
+ %9 = smt.bv.lshr %c0_bv32, %c0_bv32 : !smt.bv<32>
+ %a9 = smt.eq %9, %c0_bv32 : !smt.bv<32>
+ smt.assert %a9
+
+ // CHECK: (assert (let (([[V16:.+]] (bvashr #x00000000 #x00000000)))
+ // CHECK: (let (([[V17:.+]] (= [[V16]] #x00000000)))
+ // CHECK: [[V17]])))
+
+ // CHECK-INLINED: (assert (= (bvashr #x00000000 #x00000000) #x00000000))
+ %10 = smt.bv.ashr %c0_bv32, %c0_bv32 : !smt.bv<32>
+ %a10 = smt.eq %10, %c0_bv32 : !smt.bv<32>
+ smt.assert %a10
+
+ // CHECK: (assert (let (([[V18:.+]] (bvudiv #x00000000 #x00000000)))
+ // CHECK: (let (([[V19:.+]] (= [[V18]] #x00000000)))
+ // CHECK: [[V19]])))
+
+ // CHECK-INLINED: (assert (= (bvudiv #x00000000 #x00000000) #x00000000))
+ %11 = smt.bv.udiv %c0_bv32, %c0_bv32 : !smt.bv<32>
+ %a11 = smt.eq %11, %c0_bv32 : !smt.bv<32>
+ smt.assert %a11
+
+ // CHECK: (assert (let (([[V20:.+]] (bvsdiv #x00000000 #x00000000)))
+ // CHECK: (let (([[V21:.+]] (= [[V20]] #x00000000)))
+ // CHECK: [[V21]])))
+
+ // CHECK-INLINED: (assert (= (bvsdiv #x00000000 #x00000000) #x00000000))
+ %12 = smt.bv.sdiv %c0_bv32, %c0_bv32 : !smt.bv<32>
+ %a12 = smt.eq %12, %c0_bv32 : !smt.bv<32>
+ smt.assert %a12
+
+ // CHECK: (assert (let (([[V22:.+]] (bvnot #x00000000)))
+ // CHECK: (let (([[V23:.+]] (= [[V22]] #x00000000)))
+ // CHECK: [[V23]])))
+
+ // CHECK-INLINED: (assert (= (bvnot #x00000000) #x00000000))
+ %13 = smt.bv.not %c0_bv32 : !smt.bv<32>
+ %a13 = smt.eq %13, %c0_bv32 : !smt.bv<32>
+ smt.assert %a13
+
+ // CHECK: (assert (let (([[V24:.+]] (bvand #x00000000 #x00000000)))
+ // CHECK: (let (([[V25:.+]] (= [[V24]] #x00000000)))
+ // CHECK: [[V25]])))
+
+ // CHECK-INLINED: (assert (= (bvand #x00000000 #x00000000) #x00000000))
+ %14 = smt.bv.and %c0_bv32, %c0_bv32 : !smt.bv<32>
+ %a14 = smt.eq %14, %c0_bv32 : !smt.bv<32>
+ smt.assert %a14
+
+ // CHECK: (assert (let (([[V26:.+]] (bvor #x00000000 #x00000000)))
+ // CHECK: (let (([[V27:.+]] (= [[V26]] #x00000000)))
+ // CHECK: [[V27]])))
+
+ // CHECK-INLINED: (assert (= (bvor #x00000000 #x00000000) #x00000000))
+ %15 = smt.bv.or %c0_bv32, %c0_bv32 : !smt.bv<32>
+ %a15 = smt.eq %15, %c0_bv32 : !smt.bv<32>
+ smt.assert %a15
+
+ // CHECK: (assert (let (([[V28:.+]] (bvxor #x00000000 #x00000000)))
+ // CHECK: (let (([[V29:.+]] (= [[V28]] #x00000000)))
+ // CHECK: [[V29]])))
+
+ // CHECK-INLINED: (assert (= (bvxor #x00000000 #x00000000) #x00000000))
+ %16 = smt.bv.xor %c0_bv32, %c0_bv32 : !smt.bv<32>
+ %a16 = smt.eq %16, %c0_bv32 : !smt.bv<32>
+ smt.assert %a16
+
+ // CHECK: (assert (let (([[V30:.+]] (bvslt #x00000000 #x00000000)))
+ // CHECK: [[V30]]))
+
+ // CHECK-INLINED: (assert (bvslt #x00000000 #x00000000))
+ %27 = smt.bv.cmp slt %c0_bv32, %c0_bv32 : !smt.bv<32>
+ smt.assert %27
+
+ // CHECK: (assert (let (([[V31:.+]] (bvsle #x00000000 #x00000000)))
+ // CHECK: [[V31]]))
+
+ // CHECK-INLINED: (assert (bvsle #x00000000 #x00000000))
+ %28 = smt.bv.cmp sle %c0_bv32, %c0_bv32 : !smt.bv<32>
+ smt.assert %28
+
+ // CHECK: (assert (let (([[V32:.+]] (bvsgt #x00000000 #x00000000)))
+ // CHECK: [[V32]]))
+
+ // CHECK-INLINED: (assert (bvsgt #x00000000 #x00000000))
+ %29 = smt.bv.cmp sgt %c0_bv32, %c0_bv32 : !smt.bv<32>
+ smt.assert %29
+
+ // CHECK: (assert (let (([[V33:.+]] (bvsge #x00000000 #x00000000)))
+ // CHECK: [[V33]]))
+
+ // CHECK-INLINED: (assert (bvsge #x00000000 #x00000000))
+ %30 = smt.bv.cmp sge %c0_bv32, %c0_bv32 : !smt.bv<32>
+ smt.assert %30
+
+ // CHECK: (assert (let (([[V34:.+]] (bvult #x00000000 #x00000000)))
+ // CHECK: [[V34]]))
+
+ // CHECK-INLINED: (assert (bvult #x00000000 #x00000000))
+ %31 = smt.bv.cmp ult %c0_bv32, %c0_bv32 : !smt.bv<32>
+ smt.assert %31
+
+ // CHECK: (assert (let (([[V35:.+]] (bvule #x00000000 #x00000000)))
+ // CHECK: [[V35]]))
+
+ // CHECK-INLINED: (assert (bvule #x00000000 #x00000000))
+ %32 = smt.bv.cmp ule %c0_bv32, %c0_bv32 : !smt.bv<32>
+ smt.assert %32
+
+ // CHECK: (assert (let (([[V36:.+]] (bvugt #x00000000 #x00000000)))
+ // CHECK: [[V36]]))
+
+ // CHECK-INLINED: (assert (bvugt #x00000000 #x00000000))
+ %33 = smt.bv.cmp ugt %c0_bv32, %c0_bv32 : !smt.bv<32>
+ smt.assert %33
+
+ // CHECK: (assert (let (([[V37:.+]] (bvuge #x00000000 #x00000000)))
+ // CHECK: [[V37]]))
+
+ // CHECK-INLINED: (assert (bvuge #x00000000 #x00000000))
+ %34 = smt.bv.cmp uge %c0_bv32, %c0_bv32 : !smt.bv<32>
+ smt.assert %34
+
+ // CHECK: (assert (let (([[V38:.+]] (concat #x00000000 #x00000000)))
+ // CHECK: (let (([[V39:.+]] ((_ extract 23 8) [[V38]])))
+ // CHECK: (let (([[V40:.+]] ((_ repeat 2) [[V39]])))
+ // CHECK: (let (([[V41:.+]] (= [[V40]] #x00000000)))
+ // CHECK: [[V41]])))))
+
+ // CHECK-INLINED: (assert (= ((_ repeat 2) ((_ extract 23 8) (concat #x00000000 #x00000000))) #x00000000))
+ %35 = smt.bv.concat %c0_bv32, %c0_bv32 : !smt.bv<32>, !smt.bv<32>
+ %36 = smt.bv.extract %35 from 8 : (!smt.bv<64>) -> !smt.bv<16>
+ %37 = smt.bv.repeat 2 times %36 : !smt.bv<16>
+ %a37 = smt.eq %37, %c0_bv32 : !smt.bv<32>
+ smt.assert %a37
+
+ // CHECK: (reset)
+ // CHECK-INLINED: (reset)
+}
diff --git a/mlir/test/Target/SMTLIB/core-errors.mlir b/mlir/test/Target/SMTLIB/core-errors.mlir
new file mode 100644
index 0000000000000..691b4380da4d9
--- /dev/null
+++ b/mlir/test/Target/SMTLIB/core-errors.mlir
@@ -0,0 +1,83 @@
+// RUN: mlir-translate --export-smtlib %s --split-input-file --verify-diagnostics
+
+smt.solver () : () -> () {
+ %0 = smt.constant true
+ // expected-error @below {{must not have any result values}}
+ %1 = smt.check sat {
+ smt.yield %0 : !smt.bool
+ } unknown {
+ smt.yield %0 : !smt.bool
+ } unsat {
+ smt.yield %0 : !smt.bool
+ } -> !smt.bool
+}
+
+// -----
+
+smt.solver () : () -> () {
+ // expected-error @below {{'sat' region must be empty}}
+ smt.check sat {
+ %0 = smt.constant true
+ smt.yield
+ } unknown {
+ } unsat {
+ }
+}
+
+// -----
+
+smt.solver () : () -> () {
+ // expected-error @below {{'unknown' region must be empty}}
+ smt.check sat {
+ } unknown {
+ %0 = smt.constant true
+ smt.yield
+ } unsat {
+ }
+}
+
+// -----
+
+smt.solver () : () -> () {
+ // expected-error @below {{'unsat' region must be empty}}
+ smt.check sat {
+ } unknown {
+ } unsat {
+ %0 = smt.constant true
+ smt.yield
+ }
+}
+
+// -----
+
+// expected-error @below {{solver scopes with inputs or results are not supported}}
+%0 = smt.solver () : () -> (i1) {
+ %1 = arith.constant true
+ smt.yield %1 : i1
+}
+
+// -----
+
+smt.solver () : () -> () {
+ // expected-error @below {{solver must not contain any non-SMT operations}}
+ %1 = arith.constant true
+}
+
+// -----
+
+func.func @solver_input(%arg0: i1) {
+ // expected-error @below {{solver scopes with inputs or results are not supported}}
+ smt.solver (%arg0) : (i1) -> () {
+ ^bb0(%arg1: i1):
+ smt.yield
+ }
+ return
+}
+
+// -----
+
+smt.solver () : () -> () {
+ %0 = smt.declare_fun : !smt.sort<"uninterpreted0">
+ // expected-error @below {{uninterpreted sorts with same identifier but different arity found}}
+ %1 = smt.declare_fun : !smt.sort<"uninterpreted0"[!smt.bool]>
+}
diff --git a/mlir/test/Target/SMTLIB/core.mlir b/mlir/test/Target/SMTLIB/core.mlir
new file mode 100644
index 0000000000000..6506e17002bbe
--- /dev/null
+++ b/mlir/test/Target/SMTLIB/core.mlir
@@ -0,0 +1,137 @@
+// RUN: mlir-translate --export-smtlib %s | FileCheck %s
+// RUN: mlir-translate --export-smtlib --smtlibexport-inline-single-use-values %s | FileCheck %s --check-prefix=CHECK-INLINED
+
+smt.solver () : () -> () {
+ %c0_bv32 = smt.bv.constant #smt.bv<0> : !smt.bv<32>
+ %true = smt.constant true
+ %false = smt.constant false
+
+ // CHECK: (declare-const b (_ BitVec 32))
+ // CHECK: (assert (let (([[V0:.+]] (= #x00000000 b)))
+ // CHECK: [[V0]]))
+
+ // CHECK-INLINED: (declare-const b (_ BitVec 32))
+ // CHECK-INLINED: (assert (= #x00000000 b))
+ %21 = smt.declare_fun "b" : !smt.bv<32>
+ %23 = smt.eq %c0_bv32, %21 : !smt.bv<32>
+ smt.assert %23
+
+ // CHECK: (assert (let (([[V1:.+]] (distinct #x00000000 #x00000000)))
+ // CHECK: [[V1]]))
+
+ // CHECK-INLINED: (assert (distinct #x00000000 #x00000000))
+ %24 = smt.distinct %c0_bv32, %c0_bv32 : !smt.bv<32>
+ smt.assert %24
+
+ // CHECK: (declare-const a Bool)
+ // CHECK: (assert (let (([[V2:.+]] (ite a #x00000000 b)))
+ // CHECK: (let (([[V3:.+]] (= #x00000000 [[V2]])))
+ // CHECK: [[V3]])))
+
+ // CHECK-INLINED: (declare-const a Bool)
+ // CHECK-INLINED: (assert (= #x00000000 (ite a #x00000000 b)))
+ %20 = smt.declare_fun "a" : !smt.bool
+ %38 = smt.ite %20, %c0_bv32, %21 : !smt.bv<32>
+ %4 = smt.eq %c0_bv32, %38 : !smt.bv<32>
+ smt.assert %4
+
+ // CHECK: (assert (let (([[V4:.+]] (not true)))
+ // CHECK: (let (([[V5:.+]] (and [[V4]] true false)))
+ // CHECK: (let (([[V6:.+]] (or [[V5]] [[V4]] true)))
+ // CHECK: (let (([[V7:.+]] (xor [[V4]] [[V6]])))
+ // CHECK: (let (([[V8:.+]] (=> [[V7]] false)))
+ // CHECK: [[V8]]))))))
+
+ // CHECK-INLINED: (assert (let (([[V15:.+]] (not true)))
+ // CHECK-INLINED: (=> (xor [[V15]] (or (and [[V15]] true false) [[V15]] true)) false)))
+ %39 = smt.not %true
+ %40 = smt.and %39, %true, %false
+ %41 = smt.or %40, %39, %true
+ %42 = smt.xor %39, %41
+ %43 = smt.implies %42, %false
+ smt.assert %43
+
+ // CHECK: (declare-fun func1 (Bool Bool) Bool)
+ // CHECK: (assert (let (([[V9:.+]] (func1 true false)))
+ // CHECK: [[V9]]))
+
+ // CHECK-INLINED: (declare-fun func1 (Bool Bool) Bool)
+ // CHECK-INLINED: (assert (func1 true false))
+ %44 = smt.declare_fun "func1" : !smt.func<(!smt.bool, !smt.bool) !smt.bool>
+ %45 = smt.apply_func %44(%true, %false) : !smt.func<(!smt.bool, !smt.bool) !smt.bool>
+ smt.assert %45
+
+ // CHECK: (assert (let (([[V10:.+]] (forall (([[A:.+]] Int) ([[B:.+]] Int))
+ // CHECK: (let (([[V11:.+]] (= [[A]] [[B]])))
+ // CHECK: [[V11]]))))
+ // CHECK: [[V10]]))
+
+ // CHECK-INLINED: (assert (forall (([[A:.+]] Int) ([[B:.+]] Int))
+ // CHECK-INLINED: (= [[A]] [[B]])))
+ %1 = smt.forall ["a", "b"] {
+ ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+ %2 = smt.eq %arg2, %arg3 : !smt.int
+ smt.yield %2 : !smt.bool
+ }
+ smt.assert %1
+
+ // CHECK: (assert (let (([[V12:.+]] (exists (([[V13:.+]] Int) ([[V14:.+]] Int))
+ // CHECK: (let (([[V15:.+]] (= [[V13]] [[V14]])))
+ // CHECK: [[V15]]))))
+ // CHECK: [[V12]]))
+
+ // CHECK-INLINED: (assert (exists (([[A:.+]] Int) ([[B:.+]] Int))
+ // CHECK-INLINED: (= [[A]] [[B]])))
+ %2 = smt.exists {
+ ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+ %3 = smt.eq %arg2, %arg3 : !smt.int
+ smt.yield %3 : !smt.bool
+ }
+ smt.assert %2
+
+ // Test: make sure that open parens from outside quantifier bodies are not
+ // propagated into the body.
+ // CHECK: (assert (let (([[V15:.+]] (exists (([[V16:.+]] Int) ([[V17:.+]] Int)){{$}}
+ // CHECK: (let (([[V18:.+]] (= [[V16]] [[V17]]))){{$}}
+ // CHECK: [[V18]])))){{$}}
+ // CHECK: (let (([[V19:.+]] (exists (([[V20:.+]] Int) ([[V21:.+]] Int)){{$}}
+ // CHECK: (let (([[V22:.+]] (= [[V20]] [[V21]]))){{$}}
+ // CHECK: [[V22]])))){{$}}
+ // CHECK: (let (([[V23:.+]] (and [[V19]] [[V15]]))){{$}}
+ // CHECK: [[V23]])))){{$}}
+ %3 = smt.exists {
+ ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+ %5 = smt.eq %arg2, %arg3 : !smt.int
+ smt.yield %5 : !smt.bool
+ }
+ %5 = smt.exists {
+ ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+ %6 = smt.eq %arg2, %arg3 : !smt.int
+ smt.yield %6 : !smt.bool
+ }
+ %6 = smt.and %3, %5
+ smt.assert %6
+
+ // CHECK: (check-sat)
+ // CHECK-INLINED: (check-sat)
+ smt.check sat {} unknown {} unsat {}
+
+ // CHECK: (reset)
+ // CHECK-INLINED: (reset)
+ smt.reset
+
+ // CHECK: (push 1)
+ // CHECK-INLINED: (push 1)
+ smt.push 1
+
+ // CHECK: (pop 1)
+ // CHECK-INLINED: (pop 1)
+ smt.pop 1
+
+ // CHECK: (set-logic AUFLIA)
+ // CHECK-INLINED: (set-logic AUFLIA)
+ smt.set_logic "AUFLIA"
+
+ // CHECK: (reset)
+ // CHECK-INLINED: (reset)
+}
diff --git a/mlir/test/Target/SMTLIB/integer-errors.mlir b/mlir/test/Target/SMTLIB/integer-errors.mlir
new file mode 100644
index 0000000000000..4dc5f48f4fe5b
--- /dev/null
+++ b/mlir/test/Target/SMTLIB/integer-errors.mlir
@@ -0,0 +1,7 @@
+// RUN: mlir-translate --export-smtlib %s --split-input-file --verify-diagnostics
+
+smt.solver () : () -> () {
+ %0 = smt.int.constant 5
+ // expected-error @below {{operation not supported for SMTLIB emission}}
+ %1 = smt.int2bv %0 : !smt.bv<4>
+}
diff --git a/mlir/test/Target/SMTLIB/integer.mlir b/mlir/test/Target/SMTLIB/integer.mlir
new file mode 100644
index 0000000000000..aa8399aeb4ece
--- /dev/null
+++ b/mlir/test/Target/SMTLIB/integer.mlir
@@ -0,0 +1,82 @@
+// RUN: mlir-translate --export-smtlib %s | FileCheck %s
+
+smt.solver () : () -> () {
+ %0 = smt.int.constant 5
+ %1 = smt.int.constant 10
+
+ // CHECK: (assert (let (([[V0:.+]] (+ 5 5 5)))
+ // CHECK: (let (([[V1:.+]] (= [[V0]] 10)))
+ // CHECK: [[V1]])))
+
+ // CHECK-INLINED: (assert (= (+ 5 5 5) 10))
+ %2 = smt.int.add %0, %0, %0
+ %a2 = smt.eq %2, %1 : !smt.int
+ smt.assert %a2
+
+ // CHECK: (assert (let (([[V2:.+]] (* 5 5 5)))
+ // CHECK: (let (([[V3:.+]] (= [[V2]] 10)))
+ // CHECK: [[V3]])))
+
+ // CHECK-INLINED: (assert (= (* 5 5 5) 10))
+ %3 = smt.int.mul %0, %0, %0
+ %a3 = smt.eq %3, %1 : !smt.int
+ smt.assert %a3
+
+ // CHECK: (assert (let (([[V4:.+]] (- 5 5)))
+ // CHECK: (let (([[V5:.+]] (= [[V4]] 10)))
+ // CHECK: [[V5]])))
+
+ // CHECK-INLINED: (assert (= (- 5 5) 10))
+ %4 = smt.int.sub %0, %0
+ %a4 = smt.eq %4, %1 : !smt.int
+ smt.assert %a4
+
+ // CHECK: (assert (let (([[V6:.+]] (div 5 5)))
+ // CHECK: (let (([[V7:.+]] (= [[V6]] 10)))
+ // CHECK: [[V7]])))
+
+ // CHECK-INLINED: (assert (= (div 5 5) 10))
+ %5 = smt.int.div %0, %0
+ %a5 = smt.eq %5, %1 : !smt.int
+ smt.assert %a5
+
+ // CHECK: (assert (let (([[V8:.+]] (mod 5 5)))
+ // CHECK: (let (([[V9:.+]] (= [[V8]] 10)))
+ // CHECK: [[V9]])))
+
+ // CHECK-INLINED: (assert (= (mod 5 5) 10))
+ %6 = smt.int.mod %0, %0
+ %a6 = smt.eq %6, %1 : !smt.int
+ smt.assert %a6
+
+ // CHECK: (assert (let (([[V10:.+]] (<= 5 5)))
+ // CHECK: [[V10]]))
+
+ // CHECK-INLINED: (assert (<= 5 5))
+ %9 = smt.int.cmp le %0, %0
+ smt.assert %9
+
+ // CHECK: (assert (let (([[V11:.+]] (< 5 5)))
+ // CHECK: [[V11]]))
+
+ // CHECK-INLINED: (assert (< 5 5))
+ %10 = smt.int.cmp lt %0, %0
+ smt.assert %10
+
+ // CHECK: (assert (let (([[V12:.+]] (>= 5 5)))
+ // CHECK: [[V12]]))
+
+ // CHECK-INLINED: (assert (>= 5 5))
+ %11 = smt.int.cmp ge %0, %0
+ smt.assert %11
+
+ // CHECK: (assert (let (([[V13:.+]] (> 5 5)))
+ // CHECK: [[V13]]))
+
+ // CHECK-INLINED: (assert (> 5 5))
+ %12 = smt.int.cmp gt %0, %0
+ smt.assert %12
+
+ // CHECK: (reset)
+ // CHECK-INLINED: (reset)
+}
More information about the Mlir-commits
mailing list