From acf964b95f5421cc372719139b427be37ad79e7e Mon Sep 17 00:00:00 2001 From: Maksim Levental Date: Sat, 12 Apr 2025 16:39:16 -0400 Subject: [PATCH] [mlir][SMT] add export smtlib (#131492) This PR adds the `ExportSMTLIB` translation/egress pass for `SMT` dialect. --- 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 50ad3b285ba4..3de3e02ff3f8 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 000000000000..6415b97167cf --- /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 000000000000..09bd5cd2d407 --- /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::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(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 `_` suffix where `` 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 + `_` is returned. + /// 2. The name is given a suffix `__` where `` 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 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 000000000000..ed0bccef0e43 --- /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 . + using CacheItem = std::pair; + 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::unique_ptr &&impl) + : impl(std::move(impl)) {} + CacheItem operator*() const { return **impl; } + using llvm::iterator_facade_base::operator++; + bool operator==(const Iterator &other) const { + return *impl == other.impl.get(); + } + void operator++() { impl->operator++(); } + + private: + std::unique_ptr 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 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(other)->it; + } + Iterator it; + }; + +public: + SymbolCacheBase::Iterator begin() override { + return SymbolCacheBase::Iterator( + std::make_unique(symbolCache.begin())); + } + SymbolCacheBase::Iterator end() override { + return SymbolCacheBase::Iterator( + std::make_unique(symbolCache.end())); + } +}; + +} // namespace mlir + +#endif // MLIR_SUPPORT_SYMCACHE_H diff --git a/mlir/lib/Target/CMakeLists.txt b/mlir/lib/Target/CMakeLists.txt index c3ec1b4f1e3f..f14ec49b5a0c 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 000000000000..1fd965551ae4 --- /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 000000000000..47235c4a5a52 --- /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; + +#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(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 { + using Base = + smt::SMTOpVisitor; + 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 + LogicalResult printBinaryOp(Op op, StringRef name, VisitorInfo &info) { + info.stream << "(" << name << " " << info.valueMap.lookup(op.getLhs()) + << " " << info.valueMap.lookup(op.getRhs()) << ")"; + return success(); + } + + template + 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 + 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 scope(info.valueMap); + info.stream << "(" << operatorString << " ("; + StringLiteral delimiter = ""; + + SmallVector argNames; + + for (auto [i, arg] : llvm::enumerate(op.getBody().getArguments())) { + // Generate and register a new unique name. + StringRef prefix = + op.getBoundVarNames() + ? cast(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 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 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 &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 { + using smt::SMTOpVisitor::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(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 scope1(valueMap); + SmallVector 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(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 declaredSorts; + auto result = block->walk([&](Operation *op) -> WalkResult { + if (!isa(op->getDialect())) + return op->emitError() + << "solver must not contain any non-SMT operations"; + + for (Type resTy : op->getResultTypes()) { + auto sortTy = dyn_cast(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 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 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(); + }); +} diff --git a/mlir/test/Target/SMTLIB/array.mlir b/mlir/test/Target/SMTLIB/array.mlir new file mode 100644 index 000000000000..6d289eff1ea3 --- /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 000000000000..2f534497d0af --- /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 000000000000..ae403b0b5936 --- /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 000000000000..c58992769d9b --- /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 000000000000..691b4380da4d --- /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 000000000000..6506e17002bb --- /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 000000000000..4dc5f48f4fe5 --- /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 000000000000..aa8399aeb4ec --- /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) +}