[Mlir-commits] [mlir] [mlir][smt] add export smtlib (PR #131492)
Maksim Levental
llvmlistbot at llvm.org
Sat Mar 15 21:21:19 PDT 2025
https://github.com/makslevental created https://github.com/llvm/llvm-project/pull/131492
None
>From 25f19c2208f3d5134346fad2effbd949c3807b89 Mon Sep 17 00:00:00 2001
From: max <maksim.levental at gmail.com>
Date: Sat, 15 Mar 2025 19:14:37 -0400
Subject: [PATCH 1/2] [mlir][smt] upstream SMT dialect
---
mlir/include/mlir/Dialect/CMakeLists.txt | 1 +
mlir/include/mlir/Dialect/SMT/CMakeLists.txt | 1 +
.../mlir/Dialect/SMT/IR/CMakeLists.txt | 16 +
mlir/include/mlir/Dialect/SMT/IR/SMT.td | 22 +
.../mlir/Dialect/SMT/IR/SMTArrayOps.td | 99 ++++
.../mlir/Dialect/SMT/IR/SMTAttributes.h | 29 +
.../mlir/Dialect/SMT/IR/SMTAttributes.td | 74 +++
.../mlir/Dialect/SMT/IR/SMTBitVectorOps.td | 255 +++++++++
mlir/include/mlir/Dialect/SMT/IR/SMTDialect.h | 20 +
.../include/mlir/Dialect/SMT/IR/SMTDialect.td | 30 ++
mlir/include/mlir/Dialect/SMT/IR/SMTIntOps.td | 137 +++++
mlir/include/mlir/Dialect/SMT/IR/SMTOps.h | 25 +
mlir/include/mlir/Dialect/SMT/IR/SMTOps.td | 477 +++++++++++++++++
mlir/include/mlir/Dialect/SMT/IR/SMTTypes.h | 30 ++
mlir/include/mlir/Dialect/SMT/IR/SMTTypes.td | 145 +++++
.../include/mlir/Dialect/SMT/IR/SMTVisitors.h | 201 +++++++
mlir/include/mlir/InitAllDialects.h | 2 +
mlir/lib/Dialect/CMakeLists.txt | 1 +
mlir/lib/Dialect/SMT/CMakeLists.txt | 1 +
mlir/lib/Dialect/SMT/IR/CMakeLists.txt | 27 +
mlir/lib/Dialect/SMT/IR/SMTAttributes.cpp | 201 +++++++
mlir/lib/Dialect/SMT/IR/SMTDialect.cpp | 47 ++
mlir/lib/Dialect/SMT/IR/SMTOps.cpp | 472 +++++++++++++++++
mlir/lib/Dialect/SMT/IR/SMTTypes.cpp | 92 ++++
mlir/test/Dialect/SMT/array-errors.mlir | 13 +
mlir/test/Dialect/SMT/array.mlir | 14 +
mlir/test/Dialect/SMT/basic.mlir | 200 +++++++
mlir/test/Dialect/SMT/bitvector-errors.mlir | 112 ++++
mlir/test/Dialect/SMT/bitvectors.mlir | 81 +++
mlir/test/Dialect/SMT/core-errors.mlir | 497 ++++++++++++++++++
mlir/test/Dialect/SMT/cse-test.mlir | 12 +
mlir/test/Dialect/SMT/integers.mlir | 36 ++
32 files changed, 3370 insertions(+)
create mode 100644 mlir/include/mlir/Dialect/SMT/CMakeLists.txt
create mode 100644 mlir/include/mlir/Dialect/SMT/IR/CMakeLists.txt
create mode 100644 mlir/include/mlir/Dialect/SMT/IR/SMT.td
create mode 100644 mlir/include/mlir/Dialect/SMT/IR/SMTArrayOps.td
create mode 100644 mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.h
create mode 100644 mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.td
create mode 100644 mlir/include/mlir/Dialect/SMT/IR/SMTBitVectorOps.td
create mode 100644 mlir/include/mlir/Dialect/SMT/IR/SMTDialect.h
create mode 100644 mlir/include/mlir/Dialect/SMT/IR/SMTDialect.td
create mode 100644 mlir/include/mlir/Dialect/SMT/IR/SMTIntOps.td
create mode 100644 mlir/include/mlir/Dialect/SMT/IR/SMTOps.h
create mode 100644 mlir/include/mlir/Dialect/SMT/IR/SMTOps.td
create mode 100644 mlir/include/mlir/Dialect/SMT/IR/SMTTypes.h
create mode 100644 mlir/include/mlir/Dialect/SMT/IR/SMTTypes.td
create mode 100644 mlir/include/mlir/Dialect/SMT/IR/SMTVisitors.h
create mode 100644 mlir/lib/Dialect/SMT/CMakeLists.txt
create mode 100644 mlir/lib/Dialect/SMT/IR/CMakeLists.txt
create mode 100644 mlir/lib/Dialect/SMT/IR/SMTAttributes.cpp
create mode 100644 mlir/lib/Dialect/SMT/IR/SMTDialect.cpp
create mode 100644 mlir/lib/Dialect/SMT/IR/SMTOps.cpp
create mode 100644 mlir/lib/Dialect/SMT/IR/SMTTypes.cpp
create mode 100644 mlir/test/Dialect/SMT/array-errors.mlir
create mode 100644 mlir/test/Dialect/SMT/array.mlir
create mode 100644 mlir/test/Dialect/SMT/basic.mlir
create mode 100644 mlir/test/Dialect/SMT/bitvector-errors.mlir
create mode 100644 mlir/test/Dialect/SMT/bitvectors.mlir
create mode 100644 mlir/test/Dialect/SMT/core-errors.mlir
create mode 100644 mlir/test/Dialect/SMT/cse-test.mlir
create mode 100644 mlir/test/Dialect/SMT/integers.mlir
diff --git a/mlir/include/mlir/Dialect/CMakeLists.txt b/mlir/include/mlir/Dialect/CMakeLists.txt
index f710235197334..9d1a840d6644b 100644
--- a/mlir/include/mlir/Dialect/CMakeLists.txt
+++ b/mlir/include/mlir/Dialect/CMakeLists.txt
@@ -33,6 +33,7 @@ add_subdirectory(Ptr)
add_subdirectory(Quant)
add_subdirectory(SCF)
add_subdirectory(Shape)
+add_subdirectory(SMT)
add_subdirectory(SparseTensor)
add_subdirectory(SPIRV)
add_subdirectory(Tensor)
diff --git a/mlir/include/mlir/Dialect/SMT/CMakeLists.txt b/mlir/include/mlir/Dialect/SMT/CMakeLists.txt
new file mode 100644
index 0000000000000..f33061b2d87cf
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/CMakeLists.txt
@@ -0,0 +1 @@
+add_subdirectory(IR)
diff --git a/mlir/include/mlir/Dialect/SMT/IR/CMakeLists.txt b/mlir/include/mlir/Dialect/SMT/IR/CMakeLists.txt
new file mode 100644
index 0000000000000..bd743ed510a9e
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/IR/CMakeLists.txt
@@ -0,0 +1,16 @@
+add_mlir_dialect(SMT smt)
+add_mlir_doc(SMT SMT Dialects/SMTOps -gen-op-doc)
+# TODO(maX)
+#add_mlir_doc(SMT SMT Dialects/SMTTypes -gen-typedef-doc -dialect smt)
+
+set(LLVM_TARGET_DEFINITIONS SMT.td)
+
+mlir_tablegen(SMTAttributes.h.inc -gen-attrdef-decls)
+mlir_tablegen(SMTAttributes.cpp.inc -gen-attrdef-defs)
+add_public_tablegen_target(MLIRSMTAttrIncGen)
+add_dependencies(mlir-headers MLIRSMTAttrIncGen)
+
+mlir_tablegen(SMTEnums.h.inc -gen-enum-decls)
+mlir_tablegen(SMTEnums.cpp.inc -gen-enum-defs)
+add_public_tablegen_target(MLIRSMTEnumsIncGen)
+add_dependencies(mlir-headers MLIRSMTEnumsIncGen)
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMT.td b/mlir/include/mlir/Dialect/SMT/IR/SMT.td
new file mode 100644
index 0000000000000..dd7bd033c9fa5
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMT.td
@@ -0,0 +1,22 @@
+//===- SMT.td - SMT dialect definition ---------------------*- tablegen -*-===//
+//
+// 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
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef MLIR_DIALECT_SMT_SMT_TD
+#define MLIR_DIALECT_SMT_SMT_TD
+
+include "mlir/IR/OpBase.td"
+
+include "mlir/Dialect/SMT/IR/SMTAttributes.td"
+include "mlir/Dialect/SMT/IR/SMTDialect.td"
+include "mlir/Dialect/SMT/IR/SMTTypes.td"
+include "mlir/Dialect/SMT/IR/SMTOps.td"
+include "mlir/Dialect/SMT/IR/SMTArrayOps.td"
+include "mlir/Dialect/SMT/IR/SMTBitVectorOps.td"
+include "mlir/Dialect/SMT/IR/SMTIntOps.td"
+
+#endif // MLIR_DIALECT_SMT_SMT_TD
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTArrayOps.td b/mlir/include/mlir/Dialect/SMT/IR/SMTArrayOps.td
new file mode 100644
index 0000000000000..05b5398b6a7f9
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTArrayOps.td
@@ -0,0 +1,99 @@
+//===- SMTArrayOps.td - SMT array operations ---------------*- tablegen -*-===//
+//
+// 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
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef MLIR_DIALECT_SMT_SMTARRAYOPS_TD
+#define MLIR_DIALECT_SMT_SMTARRAYOPS_TD
+
+include "mlir/Dialect/SMT/IR/SMTDialect.td"
+include "mlir/Dialect/SMT/IR/SMTAttributes.td"
+include "mlir/Dialect/SMT/IR/SMTTypes.td"
+include "mlir/Interfaces/SideEffectInterfaces.td"
+
+class SMTArrayOp<string mnemonic, list<Trait> traits = []> :
+ SMTOp<"array." # mnemonic, traits>;
+
+def ArrayStoreOp : SMTArrayOp<"store", [
+ Pure,
+ TypesMatchWith<"summary", "array", "index",
+ "cast<ArrayType>($_self).getDomainType()">,
+ TypesMatchWith<"summary", "array", "value",
+ "cast<ArrayType>($_self).getRangeType()">,
+ AllTypesMatch<["array", "result"]>,
+]> {
+ let summary = "stores a value at a given index and returns the new array";
+ let description = [{
+ This operation returns a new array which is the same as the 'array' operand
+ except that the value at the given 'index' is changed to the given 'value'.
+ The semantics are equivalent to the 'store' operator described in the
+ [SMT ArrayEx theory](https://smtlib.cs.uiowa.edu/Theories/ArraysEx.smt2) of
+ the SMT-LIB standard 2.6.
+ }];
+
+ let arguments = (ins ArrayType:$array, AnySMTType:$index, AnySMTType:$value);
+ let results = (outs ArrayType:$result);
+
+ let assemblyFormat = [{
+ $array `[` $index `]` `,` $value attr-dict `:` qualified(type($array))
+ }];
+}
+
+def ArraySelectOp : SMTArrayOp<"select", [
+ Pure,
+ TypesMatchWith<"summary", "array", "index",
+ "cast<ArrayType>($_self).getDomainType()">,
+ TypesMatchWith<"summary", "array", "result",
+ "cast<ArrayType>($_self).getRangeType()">,
+]> {
+ let summary = "get the value stored in the array at the given index";
+ let description = [{
+ This operation is retuns the value stored in the given array at the given
+ index. The semantics are equivalent to the `select` operator defined in the
+ [SMT ArrayEx theory](https://smtlib.cs.uiowa.edu/Theories/ArraysEx.smt2) of
+ the SMT-LIB standard 2.6.
+ }];
+
+ let arguments = (ins ArrayType:$array, AnySMTType:$index);
+ let results = (outs AnySMTType:$result);
+
+ let assemblyFormat = [{
+ $array `[` $index `]` attr-dict `:` qualified(type($array))
+ }];
+}
+
+def ArrayBroadcastOp : SMTArrayOp<"broadcast", [
+ Pure,
+ TypesMatchWith<"summary", "result", "value",
+ "cast<ArrayType>($_self).getRangeType()">,
+]> {
+ let summary = "construct an array with the given value stored at every index";
+ let description = [{
+ This operation represents a broadcast of the 'value' operand to all indices
+ of the array. It is equivalent to
+ ```
+ %0 = smt.declare "array" : !smt.array<[!smt.int -> !smt.bool]>
+ %1 = smt.forall ["idx"] {
+ ^bb0(%idx: !smt.int):
+ %2 = smt.array.select %0[%idx] : !smt.array<[!smt.int -> !smt.bool]>
+ %3 = smt.eq %value, %2 : !smt.bool
+ smt.yield %3 : !smt.bool
+ }
+ smt.assert %1
+ // return %0
+ ```
+
+ In SMT-LIB, this is frequently written as
+ `((as const (Array Int Bool)) value)`.
+ }];
+
+ let arguments = (ins AnySMTType:$value);
+ let results = (outs ArrayType:$result);
+
+ let assemblyFormat = "$value attr-dict `:` qualified(type($result))";
+}
+
+#endif // MLIR_DIALECT_SMT_SMTARRAYOPS_TD
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.h b/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.h
new file mode 100644
index 0000000000000..590364d572699
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.h
@@ -0,0 +1,29 @@
+//===- SMTAttributes.h - Declare SMT dialect attributes ----------*- 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
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef MLIR_DIALECT_SMT_SMTATTRIBUTES_H
+#define MLIR_DIALECT_SMT_SMTATTRIBUTES_H
+
+#include "mlir/IR/Attributes.h"
+#include "mlir/IR/BuiltinAttributeInterfaces.h"
+#include "mlir/IR/BuiltinAttributes.h"
+
+namespace mlir {
+namespace smt {
+namespace detail {
+
+struct BitVectorAttrStorage;
+
+} // namespace detail
+} // namespace smt
+} // namespace mlir
+
+#define GET_ATTRDEF_CLASSES
+#include "mlir/Dialect/SMT/IR/SMTAttributes.h.inc"
+
+#endif // MLIR_DIALECT_SMT_SMTATTRIBUTES_H
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.td b/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.td
new file mode 100644
index 0000000000000..4231363fdf05b
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.td
@@ -0,0 +1,74 @@
+//===- SMTAttributes.td - Attributes for SMT dialect -------*- tablegen -*-===//
+//
+// 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 defines SMT dialect specific attributes.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef MLIR_DIALECT_SMT_SMTATTRIBUTES_TD
+#define MLIR_DIALECT_SMT_SMTATTRIBUTES_TD
+
+include "mlir/Dialect/SMT/IR/SMTDialect.td"
+include "mlir/IR/EnumAttr.td"
+include "mlir/IR/BuiltinAttributeInterfaces.td"
+
+def BitVectorAttr : AttrDef<SMTDialect, "BitVector", [
+ DeclareAttrInterfaceMethods<TypedAttrInterface>
+]> {
+ let mnemonic = "bv";
+ let description = [{
+ This attribute represents a constant value of the `(_ BitVec width)` sort as
+ described in the [SMT bit-vector
+ theory](https://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml).
+
+ The constant is as #bX (binary) or #xX (hexadecimal) in SMT-LIB
+ where X is the value in the corresponding format without any further
+ prefixing. Here, the bit-vector constant is given as a regular integer
+ literal and the associated bit-vector type indicating the bit-width.
+
+ Examples:
+ ```mlir
+ #smt.bv<5> : !smt.bv<4>
+ #smt.bv<92> : !smt.bv<8>
+ ```
+
+ The explicit type-suffix is mandatory to uniquely represent the attribute,
+ i.e., this attribute should always be used in the extended form (using the
+ `quantified` keyword in the operation assembly format string).
+
+ The bit-width must be greater than zero (i.e., at least one digit has to be
+ present).
+ }];
+
+ let parameters = (ins "llvm::APInt":$value);
+
+ let hasCustomAssemblyFormat = true;
+ let genVerifyDecl = true;
+
+ // We need to manually define the storage class because the generated one is
+ // buggy (because the APInt asserts matching bitwidth in the `==` operator and
+ // the generated storage uses that directly.
+ // Alternatively: add a type parameter to redundantly store the bitwidth of
+ // of the attribute type, it it's in the order before the 'value' it will be
+ // checked before the APInt equality (this is the reason it works for the
+ // builtin integer attribute), but would be more fragile (and we'd store
+ // duplicate data).
+ let genStorageClass = false;
+
+ let builders = [
+ AttrBuilder<(ins "llvm::StringRef":$value)>,
+ AttrBuilder<(ins "uint64_t":$value, "unsigned":$width)>,
+ ];
+
+ let extraClassDeclaration = [{
+ /// Return the bit-vector constant as a SMT-LIB formatted string.
+ std::string getValueAsString(bool prefix = true) const;
+ }];
+}
+
+#endif // MLIR_DIALECT_SMT_SMTATTRIBUTES_TD
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTBitVectorOps.td b/mlir/include/mlir/Dialect/SMT/IR/SMTBitVectorOps.td
new file mode 100644
index 0000000000000..b6ca34e142d82
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTBitVectorOps.td
@@ -0,0 +1,255 @@
+//===- SMTBitVectorOps.td - SMT bit-vector dialect ops -----*- tablegen -*-===//
+//
+// 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
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef MLIR_DIALECT_SMT_SMTBITVECTOROPS_TD
+#define MLIR_DIALECT_SMT_SMTBITVECTOROPS_TD
+
+include "mlir/Dialect/SMT/IR/SMTDialect.td"
+include "mlir/Dialect/SMT/IR/SMTAttributes.td"
+include "mlir/Dialect/SMT/IR/SMTTypes.td"
+include "mlir/IR/EnumAttr.td"
+include "mlir/IR/OpAsmInterface.td"
+include "mlir/Interfaces/InferTypeOpInterface.td"
+include "mlir/Interfaces/SideEffectInterfaces.td"
+
+class SMTBVOp<string mnemonic, list<Trait> traits = []> :
+ Op<SMTDialect, "bv." # mnemonic, traits>;
+
+def BVConstantOp : SMTBVOp<"constant", [
+ Pure,
+ ConstantLike,
+ FirstAttrDerivedResultType,
+ DeclareOpInterfaceMethods<InferTypeOpInterface, ["inferReturnTypes"]>,
+ DeclareOpInterfaceMethods<OpAsmOpInterface, ["getAsmResultNames"]>
+]> {
+ let summary = "produce a constant bit-vector";
+ let description = [{
+ This operation produces an SSA value equal to the bit-vector constant
+ specified by the 'value' attribute.
+ Refer to the `BitVectorAttr` documentation for more information about
+ the semantics of bit-vector constants, their format, and associated sort.
+ The result type always matches the attribute's type.
+
+ Examples:
+ ```mlir
+ %c92_bv8 = smt.bv.constant #smt.bv<92> : !smt.bv<8>
+ %c5_bv4 = smt.bv.constant #smt.bv<5> : !smt.bv<4>
+ ```
+ }];
+
+ let arguments = (ins BitVectorAttr:$value);
+ let results = (outs BitVectorType:$result);
+
+ let assemblyFormat = "qualified($value) attr-dict";
+
+ let builders = [
+ OpBuilder<(ins "const llvm::APInt &":$value), [{
+ build($_builder, $_state,
+ BitVectorAttr::get($_builder.getContext(), value));
+ }]>,
+ OpBuilder<(ins "uint64_t":$value, "unsigned":$width), [{
+ build($_builder, $_state,
+ BitVectorAttr::get($_builder.getContext(), value, width));
+ }]>,
+ ];
+
+ let hasFolder = true;
+}
+
+class BVArithmeticOrBitwiseOp<string mnemonic, string desc> :
+ SMTBVOp<mnemonic, [Pure, SameOperandsAndResultType]> {
+ let summary = "equivalent to bv" # mnemonic # " in SMT-LIB";
+ let description = "This operation performs " # desc # [{. The semantics are
+ equivalent to the `bv}] # mnemonic # [{` operator defined in the SMT-LIB 2.6
+ standard. More precisely in the [theory of FixedSizeBitVectors](https://smtlib.cs.uiowa.edu/Theories/FixedSizeBitVectors.smt2)
+ and the [QF_BV logic](https://smtlib.cs.uiowa.edu/Logics/QF_BV.smt2)
+ describing closed quantifier-free formulas over the theory of fixed-size
+ bit-vectors.
+ }];
+
+ let results = (outs BitVectorType:$result);
+}
+
+class BinaryBVOp<string mnemonic, string desc> :
+ BVArithmeticOrBitwiseOp<mnemonic, desc> {
+ let arguments = (ins BitVectorType:$lhs, BitVectorType:$rhs);
+ let assemblyFormat = "$lhs `,` $rhs attr-dict `:` qualified(type($result))";
+}
+
+class UnaryBVOp<string mnemonic, string desc> :
+ BVArithmeticOrBitwiseOp<mnemonic, desc> {
+ let arguments = (ins BitVectorType:$input);
+ let assemblyFormat = "$input attr-dict `:` qualified(type($result))";
+}
+
+def BVNotOp : UnaryBVOp<"not", "bitwise negation">;
+def BVNegOp : UnaryBVOp<"neg", "two's complement unary minus">;
+
+def BVAndOp : BinaryBVOp<"and", "bitwise AND">;
+def BVOrOp : BinaryBVOp<"or", "bitwise OR">;
+def BVXOrOp : BinaryBVOp<"xor", "bitwise exclusive OR">;
+
+def BVAddOp : BinaryBVOp<"add", "addition">;
+def BVMulOp : BinaryBVOp<"mul", "multiplication">;
+def BVUDivOp : BinaryBVOp<"udiv", "unsigned division (rounded towards zero)">;
+def BVSDivOp : BinaryBVOp<"sdiv", "two's complement signed division">;
+def BVURemOp : BinaryBVOp<"urem", "unsigned remainder">;
+def BVSRemOp : BinaryBVOp<"srem",
+ "two's complement signed remainder (sign follows dividend)">;
+def BVSModOp : BinaryBVOp<"smod",
+ "two's complement signed remainder (sign follows divisor)">;
+def BVShlOp : BinaryBVOp<"shl", "shift left">;
+def BVLShrOp : BinaryBVOp<"lshr", "logical shift right">;
+def BVAShrOp : BinaryBVOp<"ashr", "arithmetic shift right">;
+
+def PredicateSLT : I64EnumAttrCase<"slt", 0>;
+def PredicateSLE : I64EnumAttrCase<"sle", 1>;
+def PredicateSGT : I64EnumAttrCase<"sgt", 2>;
+def PredicateSGE : I64EnumAttrCase<"sge", 3>;
+def PredicateULT : I64EnumAttrCase<"ult", 4>;
+def PredicateULE : I64EnumAttrCase<"ule", 5>;
+def PredicateUGT : I64EnumAttrCase<"ugt", 6>;
+def PredicateUGE : I64EnumAttrCase<"uge", 7>;
+let cppNamespace = "mlir::smt" in
+def BVCmpPredicate : I64EnumAttr<
+ "BVCmpPredicate",
+ "smt bit-vector comparison predicate",
+ [PredicateSLT, PredicateSLE, PredicateSGT, PredicateSGE,
+ PredicateULT, PredicateULE, PredicateUGT, PredicateUGE]>;
+
+def BVCmpOp : SMTBVOp<"cmp", [Pure, SameTypeOperands]> {
+ let summary = "compare bit-vectors interpreted as signed or unsigned";
+ let description = [{
+ This operation compares bit-vector values, interpreting them as signed or
+ unsigned values depending on the predicate. The semantics are equivalent to
+ the `bvslt`, `bvsle`, `bvsgt`, `bvsge`, `bvult`, `bvule`, `bvugt`, or
+ `bvuge` operator defined in the SMT-LIB 2.6 standard depending on the
+ specified predicate. More precisely in the
+ [theory of FixedSizeBitVectors](https://smtlib.cs.uiowa.edu/Theories/FixedSizeBitVectors.smt2)
+ and the [QF_BV logic](https://smtlib.cs.uiowa.edu/Logics/QF_BV.smt2)
+ describing closed quantifier-free formulas over the theory of fixed-size
+ bit-vectors.
+ }];
+
+ let arguments = (ins BVCmpPredicate:$pred,
+ BitVectorType:$lhs,
+ BitVectorType:$rhs);
+ let results = (outs BoolType:$result);
+
+ let assemblyFormat = [{
+ $pred $lhs `,` $rhs attr-dict `:` qualified(type($lhs))
+ }];
+}
+
+def ConcatOp : SMTBVOp<"concat", [
+ Pure,
+ DeclareOpInterfaceMethods<InferTypeOpInterface, ["inferReturnTypes"]>
+]> {
+ let summary = "bit-vector concatenation";
+ let description = [{
+ This operation concatenates bit-vector values with semantics equivalent to
+ the `concat` operator defined in the SMT-LIB 2.6 standard. More precisely in
+ the [theory of FixedSizeBitVectors](https://smtlib.cs.uiowa.edu/Theories/FixedSizeBitVectors.smt2)
+ and the [QF_BV logic](https://smtlib.cs.uiowa.edu/Logics/QF_BV.smt2)
+ describing closed quantifier-free formulas over the theory of fixed-size
+ bit-vectors.
+
+ Note that the following equivalences hold:
+ * `smt.bv.concat %a, %b : !smt.bv<4>, !smt.bv<4>` is equivalent to
+ `(concat a b)` in SMT-LIB
+ * `(= (concat #xf #x0) #xf0)`
+ }];
+
+ let arguments = (ins BitVectorType:$lhs, BitVectorType:$rhs);
+ let results = (outs BitVectorType:$result);
+
+ let assemblyFormat = "$lhs `,` $rhs attr-dict `:` qualified(type(operands))";
+}
+
+def ExtractOp : SMTBVOp<"extract", [Pure]> {
+ let summary = "bit-vector extraction";
+ let description = [{
+ This operation extracts the range of bits starting at the 'lowBit' index
+ (inclusive) up to the 'lowBit' + result-width index (exclusive). The
+ semantics are equivalent to the `extract` operator defined in the SMT-LIB
+ 2.6 standard. More precisely in the
+ [theory of FixedSizeBitVectors](https://smtlib.cs.uiowa.edu/Theories/FixedSizeBitVectors.smt2)
+ and the [QF_BV logic](https://smtlib.cs.uiowa.edu/Logics/QF_BV.smt2)
+ describing closed quantifier-free formulas over the theory of fixed-size
+ bit-vectors.
+
+ Note that `smt.bv.extract %bv from 2 : (!smt.bv<32>) -> !smt.bv<16>` is
+ equivalent to `((_ extract 17 2) bv)`, i.e., the SMT-LIB operator takes the
+ low and high indices where both are inclusive. The following equivalence
+ holds: `(= ((_ extract 3 0) #x0f) #xf)`
+ }];
+
+ let arguments = (ins I32Attr:$lowBit, BitVectorType:$input);
+ let results = (outs BitVectorType:$result);
+
+ let assemblyFormat = [{
+ $input `from` $lowBit attr-dict `:` functional-type($input, $result)
+ }];
+
+ let hasVerifier = true;
+}
+
+def RepeatOp : SMTBVOp<"repeat", [Pure]> {
+ let summary = "repeated bit-vector concatenation of one value";
+ let description = [{
+ This operation is a shorthand for repeated concatenation of the same
+ bit-vector value, i.e.,
+ ```mlir
+ smt.bv.repeat 5 times %a : !smt.bv<4>
+ // is the same as
+ %0 = smt.bv.repeat 4 times %a : !smt.bv<4>
+ smt.bv.concat %a, %0 : !smt.bv<4>, !smt.bv<16>
+ // or also
+ %0 = smt.bv.repeat 4 times %a : !smt.bv<4>
+ smt.bv.concat %0, %a : !smt.bv<16>, !smt.bv<4>
+ ```
+
+ The semantics are equivalent to the `repeat` operator defined in the SMT-LIB
+ 2.6 standard. More precisely in the
+ [theory of FixedSizeBitVectors](https://smtlib.cs.uiowa.edu/Theories/FixedSizeBitVectors.smt2)
+ and the [QF_BV logic](https://smtlib.cs.uiowa.edu/Logics/QF_BV.smt2)
+ describing closed quantifier-free formulas over the theory of fixed-size
+ bit-vectors.
+ }];
+
+ let arguments = (ins BitVectorType:$input);
+ let results = (outs BitVectorType:$result);
+
+ let hasCustomAssemblyFormat = true;
+ let hasVerifier = true;
+
+ let builders = [
+ OpBuilder<(ins "unsigned":$count, "mlir::Value":$input)>,
+ ];
+
+ let extraClassDeclaration = [{
+ /// Get the number of times the input operand is repeated.
+ unsigned getCount();
+ }];
+}
+
+def BV2IntOp : SMTOp<"bv2int", [Pure]> {
+ let summary = "Convert an SMT bit-vector to an SMT integer.";
+ let description = [{
+ Create an integer from the bit-vector argument `input`. If `is_signed` is
+ present, the bit-vector is treated as two's complement signed. Otherwise,
+ it is treated as an unsigned integer in the range [0..2^N-1], where N is
+ the number of bits in `input`.
+ }];
+ let arguments = (ins BitVectorType:$input, UnitAttr:$is_signed);
+ let results = (outs IntType:$result);
+ let assemblyFormat = [{$input (`signed` $is_signed^)? attr-dict `:`
+ qualified(type($input))}];
+}
+
+#endif // MLIR_DIALECT_SMT_SMTBITVECTOROPS_TD
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTDialect.h b/mlir/include/mlir/Dialect/SMT/IR/SMTDialect.h
new file mode 100644
index 0000000000000..e808583a9e593
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTDialect.h
@@ -0,0 +1,20 @@
+//===- SMTDialect.h - SMT dialect definition --------------------*- 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
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef MLIR_DIALECT_SMT_SMTDIALECT_H
+#define MLIR_DIALECT_SMT_SMTDIALECT_H
+
+#include "mlir/IR/BuiltinOps.h"
+#include "mlir/IR/Dialect.h"
+#include "mlir/Support/LLVM.h"
+
+// Pull in the dialect definition.
+#include "mlir/Dialect/SMT/IR/SMTDialect.h.inc"
+#include "mlir/Dialect/SMT/IR/SMTEnums.h.inc"
+
+#endif // MLIR_DIALECT_SMT_SMTDIALECT_H
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTDialect.td b/mlir/include/mlir/Dialect/SMT/IR/SMTDialect.td
new file mode 100644
index 0000000000000..4b74187e85b87
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTDialect.td
@@ -0,0 +1,30 @@
+//===- SMTDialect.td - SMT dialect definition --------------*- tablegen -*-===//
+//
+// 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
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef MLIR_DIALECT_SMT_SMTDIALECT_TD
+#define MLIR_DIALECT_SMT_SMTDIALECT_TD
+
+include "mlir/IR/DialectBase.td"
+
+def SMTDialect : Dialect {
+ let name = "smt";
+ let summary = "a dialect that models satisfiability modulo theories";
+ let cppNamespace = "mlir::smt";
+
+ let useDefaultAttributePrinterParser = 1;
+ let useDefaultTypePrinterParser = 1;
+
+ let hasConstantMaterializer = 1;
+
+ let extraClassDeclaration = [{
+ void registerAttributes();
+ void registerTypes();
+ }];
+}
+
+#endif // MLIR_DIALECT_SMT_SMTDIALECT_TD
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTIntOps.td b/mlir/include/mlir/Dialect/SMT/IR/SMTIntOps.td
new file mode 100644
index 0000000000000..6606c9608ef55
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTIntOps.td
@@ -0,0 +1,137 @@
+//===- SMTIntOps.td - SMT dialect int theory operations ----*- tablegen -*-===//
+//
+// 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
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef MLIR_DIALECT_SMT_SMTINTOPS_TD
+#define MLIR_DIALECT_SMT_SMTINTOPS_TD
+
+include "mlir/Dialect/SMT/IR/SMTDialect.td"
+include "mlir/Dialect/SMT/IR/SMTAttributes.td"
+include "mlir/Dialect/SMT/IR/SMTTypes.td"
+include "mlir/IR/EnumAttr.td"
+include "mlir/IR/OpAsmInterface.td"
+include "mlir/Interfaces/SideEffectInterfaces.td"
+
+class SMTIntOp<string mnemonic, list<Trait> traits = []> :
+ SMTOp<"int." # mnemonic, traits>;
+
+def IntConstantOp : SMTIntOp<"constant", [
+ Pure,
+ ConstantLike,
+ DeclareOpInterfaceMethods<OpAsmOpInterface, ["getAsmResultNames"]>,
+]> {
+ let summary = "produce a constant (infinite-precision) integer";
+ let description = [{
+ This operation represents (infinite-precision) integer literals of the `Int`
+ sort. The set of values for the sort `Int` consists of all numerals and
+ all terms of the form `-n`where n is a numeral other than 0. For more
+ information refer to the
+ [SMT Ints theory](https://smtlib.cs.uiowa.edu/Theories/Ints.smt2) of the
+ SMT-LIB 2.6 standard.
+ }];
+
+ let arguments = (ins APIntAttr:$value);
+ let results = (outs IntType:$result);
+
+ let hasCustomAssemblyFormat = true;
+ let hasFolder = true;
+}
+
+class VariadicIntOp<string mnemonic> : SMTIntOp<mnemonic, [Pure, Commutative]> {
+ let description = [{
+ This operation represents (infinite-precision) }] # summary # [{.
+ The semantics are equivalent to the corresponding operator described in
+ the [SMT Ints theory](https://smtlib.cs.uiowa.edu/Theories/Ints.smt2) of the
+ SMT-LIB 2.6 standard.
+ }];
+
+ let arguments = (ins Variadic<IntType>:$inputs);
+ let results = (outs IntType:$result);
+ let assemblyFormat = "$inputs attr-dict";
+
+ let builders = [
+ OpBuilder<(ins "mlir::ValueRange":$inputs), [{
+ build($_builder, $_state, $_builder.getType<smt::IntType>(), inputs);
+ }]>,
+ ];
+}
+
+class BinaryIntOp<string mnemonic> : SMTIntOp<mnemonic, [Pure]> {
+ let description = [{
+ This operation represents (infinite-precision) }] # summary # [{.
+ The semantics are equivalent to the corresponding operator described in
+ the [SMT Ints theory](https://smtlib.cs.uiowa.edu/Theories/Ints.smt2) of the
+ SMT-LIB 2.6 standard.
+ }];
+
+ let arguments = (ins IntType:$lhs, IntType:$rhs);
+ let results = (outs IntType:$result);
+ let assemblyFormat = "$lhs `,` $rhs attr-dict";
+}
+
+def IntAbsOp : SMTIntOp<"abs", [Pure]> {
+ let summary = "the absolute value of an Int";
+ let description = [{
+ This operation represents the absolute value function for the `Int` sort.
+ The semantics are equivalent to the `abs` operator as described in the
+ [SMT Ints theory](https://smtlib.cs.uiowa.edu/Theories/Ints.smt2) of the
+ SMT-LIB 2.6 standard.
+ }];
+
+ let arguments = (ins IntType:$input);
+ let results = (outs IntType:$result);
+ let assemblyFormat = "$input attr-dict";
+}
+
+def IntAddOp : VariadicIntOp<"add"> { let summary = "integer addition"; }
+def IntMulOp : VariadicIntOp<"mul"> { let summary = "integer multiplication"; }
+def IntSubOp : BinaryIntOp<"sub"> { let summary = "integer subtraction"; }
+def IntDivOp : BinaryIntOp<"div"> { let summary = "integer division"; }
+def IntModOp : BinaryIntOp<"mod"> { let summary = "integer remainder"; }
+
+def IntPredicateLT : I64EnumAttrCase<"lt", 0>;
+def IntPredicateLE : I64EnumAttrCase<"le", 1>;
+def IntPredicateGT : I64EnumAttrCase<"gt", 2>;
+def IntPredicateGE : I64EnumAttrCase<"ge", 3>;
+let cppNamespace = "mlir::smt" in
+def IntPredicate : I64EnumAttr<
+ "IntPredicate",
+ "smt comparison predicate for integers",
+ [IntPredicateLT, IntPredicateLE, IntPredicateGT, IntPredicateGE]>;
+
+def IntCmpOp : SMTIntOp<"cmp", [Pure]> {
+ let summary = "integer comparison";
+ let description = [{
+ This operation represents the comparison of (infinite-precision) integers.
+ The semantics are equivalent to the `<= (le)`, `< (lt)`, `>= (ge)`, or
+ `> (gt)` operator depending on the predicate (indicated in parentheses) as
+ described in the
+ [SMT Ints theory](https://smtlib.cs.uiowa.edu/Theories/Ints.smt2) of the
+ SMT-LIB 2.6 standard.
+ }];
+
+ let arguments = (ins IntPredicate:$pred, IntType:$lhs, IntType:$rhs);
+ let results = (outs BoolType:$result);
+ let assemblyFormat = "$pred $lhs `,` $rhs attr-dict";
+}
+
+def Int2BVOp : SMTOp<"int2bv", [Pure]> {
+ let summary = "Convert an integer to an inferred-width bitvector.";
+ let description = [{
+ Designed to lower directly to an operation of the same name in Z3. The Z3
+ C API describes the semantics as follows:
+ Create an n bit bit-vector from the integer argument t1.
+ The resulting bit-vector has n bits, where the i'th bit (counting from 0
+ to n-1) is 1 if (t1 div 2^i) mod 2 is 1.
+ The node t1 must have integer sort.
+ }];
+ let arguments = (ins IntType:$input);
+ let results = (outs BitVectorType:$result);
+ let assemblyFormat = "$input attr-dict `:` qualified(type($result))";
+}
+
+#endif // MLIR_DIALECT_SMT_SMTINTOPS_TD
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTOps.h b/mlir/include/mlir/Dialect/SMT/IR/SMTOps.h
new file mode 100644
index 0000000000000..859566ec6dbdb
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTOps.h
@@ -0,0 +1,25 @@
+//===- SMTOps.h - SMT dialect operations ------------------------*- 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
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef MLIR_DIALECT_SMT_SMTOPS_H
+#define MLIR_DIALECT_SMT_SMTOPS_H
+
+#include "mlir/IR/OpImplementation.h"
+#include "mlir/IR/SymbolTable.h"
+#include "mlir/Interfaces/ControlFlowInterfaces.h"
+#include "mlir/Interfaces/InferTypeOpInterface.h"
+#include "mlir/Interfaces/SideEffectInterfaces.h"
+
+#include "mlir/Dialect/SMT/IR/SMTAttributes.h"
+#include "mlir/Dialect/SMT/IR/SMTDialect.h"
+#include "mlir/Dialect/SMT/IR/SMTTypes.h"
+
+#define GET_OP_CLASSES
+#include "mlir/Dialect/SMT/IR/SMT.h.inc"
+
+#endif // MLIR_DIALECT_SMT_SMTOPS_H
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTOps.td b/mlir/include/mlir/Dialect/SMT/IR/SMTOps.td
new file mode 100644
index 0000000000000..18a1483f1dab1
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTOps.td
@@ -0,0 +1,477 @@
+//===- SMTOps.td - SMT dialect operations ------------------*- tablegen -*-===//
+//
+// 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
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef MLIR_DIALECT_SMT_SMTOPS_TD
+#define MLIR_DIALECT_SMT_SMTOPS_TD
+
+include "mlir/Dialect/SMT/IR/SMTDialect.td"
+include "mlir/Dialect/SMT/IR/SMTAttributes.td"
+include "mlir/Dialect/SMT/IR/SMTTypes.td"
+include "mlir/IR/EnumAttr.td"
+include "mlir/IR/OpAsmInterface.td"
+include "mlir/Interfaces/InferTypeOpInterface.td"
+include "mlir/Interfaces/SideEffectInterfaces.td"
+include "mlir/Interfaces/ControlFlowInterfaces.td"
+
+class SMTOp<string mnemonic, list<Trait> traits = []> :
+ Op<SMTDialect, mnemonic, traits>;
+
+def DeclareFunOp : SMTOp<"declare_fun", [
+ DeclareOpInterfaceMethods<OpAsmOpInterface, ["getAsmResultNames"]>
+]> {
+ let summary = "declare a symbolic value of a given sort";
+ let description = [{
+ This operation declares a symbolic value just as the `declare-const` and
+ `declare-func` statements in SMT-LIB 2.6. The result type determines the SMT
+ sort of the symbolic value. The returned value can then be used to refer to
+ the symbolic value instead of using the identifier like in SMT-LIB.
+
+ The optionally provided string will be used as a prefix for the newly
+ generated identifier (useful for easier readability when exporting to
+ SMT-LIB). Each `declare` will always provide a unique new symbolic value
+ even if the identifier strings are the same.
+
+ Note that there does not exist a separate operation equivalent to
+ SMT-LIBs `define-fun` since
+ ```
+ (define-fun f (a Int) Int (-a))
+ ```
+ is only syntactic sugar for
+ ```
+ %f = smt.declare_fun : !smt.func<(!smt.int) !smt.int>
+ %0 = smt.forall {
+ ^bb0(%arg0: !smt.int):
+ %1 = smt.apply_func %f(%arg0) : !smt.func<(!smt.int) !smt.int>
+ %2 = smt.int.neg %arg0
+ %3 = smt.eq %1, %2 : !smt.int
+ smt.yield %3 : !smt.bool
+ }
+ smt.assert %0
+ ```
+
+ Note that this operation cannot be marked as Pure since two operations (even
+ with the same identifier string) could then be CSEd, leading to incorrect
+ behavior.
+ }];
+
+ let arguments = (ins OptionalAttr<StrAttr>:$namePrefix);
+ let results = (outs Res<AnySMTType, "a symbolic value", [MemAlloc]>:$result);
+
+ let assemblyFormat = [{
+ ($namePrefix^)? attr-dict `:` qualified(type($result))
+ }];
+
+ let builders = [
+ OpBuilder<(ins "mlir::Type":$type), [{
+ build($_builder, $_state, type, nullptr);
+ }]>
+ ];
+}
+
+def BoolConstantOp : SMTOp<"constant", [
+ Pure,
+ ConstantLike,
+ DeclareOpInterfaceMethods<OpAsmOpInterface, ["getAsmResultNames"]>,
+]> {
+ let summary = "Produce a constant boolean";
+ let description = [{
+ Produces the constant expressions 'true' and 'false' as described in the
+ [Core theory](https://smtlib.cs.uiowa.edu/Theories/Core.smt2) of the SMT-LIB
+ Standard 2.6.
+ }];
+
+ let arguments = (ins BoolAttr:$value);
+ let results = (outs BoolType:$result);
+ let assemblyFormat = "$value attr-dict";
+
+ let hasFolder = true;
+}
+
+def SolverOp : SMTOp<"solver", [
+ IsolatedFromAbove,
+ SingleBlockImplicitTerminator<"smt::YieldOp">,
+]> {
+ let summary = "create a solver instance within a lifespan";
+ let description = [{
+ This operation defines an SMT context with a solver instance. SMT operations
+ are only valid when being executed between the start and end of the region
+ of this operation. Any invocation outside is undefined. However, they do not
+ have to be direct children of this operation. For example, it is allowed to
+ have SMT operations in a `func.func` which is only called from within this
+ region. No SMT value may enter or exit the lifespan of this region (such
+ that no value created from another SMT context can be used in this scope and
+ the solver can deallocate all state required to keep track of SMT values at
+ the end).
+
+ As a result, the region is comparable to an entire SMT-LIB script, but
+ allows for concrete operations and control-flow. Concrete values may be
+ passed in and returned to influence the computations after the `smt.solver`
+ operation.
+
+ Example:
+ ```mlir
+ %0:2 = smt.solver (%in) {smt.some_attr} : (i8) -> (i8, i32) {
+ ^bb0(%arg0: i8):
+ %c = smt.declare_fun "c" : !smt.bool
+ smt.assert %c
+ %1 = smt.check sat {
+ %c1_i32 = arith.constant 1 : i32
+ smt.yield %c1_i32 : i32
+ } unknown {
+ %c0_i32 = arith.constant 0 : i32
+ smt.yield %c0_i32 : i32
+ } unsat {
+ %c-1_i32 = arith.constant -1 : i32
+ smt.yield %c-1_i32 : i32
+ } -> i32
+ smt.yield %arg0, %1 : i8, i32
+ }
+ ```
+
+ TODO: solver configuration attributes
+ }];
+
+ let arguments = (ins Variadic<AnyNonSMTType>:$inputs);
+ let regions = (region SizedRegion<1>:$bodyRegion);
+ let results = (outs Variadic<AnyNonSMTType>:$results);
+
+ let assemblyFormat = [{
+ `(` $inputs `)` attr-dict `:` functional-type($inputs, $results) $bodyRegion
+ }];
+
+ let hasRegionVerifier = true;
+}
+
+def SetLogicOp : SMTOp<"set_logic", [
+ HasParent<"smt::SolverOp">,
+]> {
+ let summary = "set the logic for the SMT solver";
+ let arguments = (ins StrAttr:$logic);
+ let assemblyFormat = "$logic attr-dict";
+}
+
+def AssertOp : SMTOp<"assert", []> {
+ let summary = "assert that a boolean expression holds";
+ let arguments = (ins BoolType:$input);
+ let assemblyFormat = "$input attr-dict";
+}
+
+def ResetOp : SMTOp<"reset", []> {
+ let summary = "reset the solver";
+ let assemblyFormat = "attr-dict";
+}
+
+def PushOp : SMTOp<"push", []> {
+ let summary = "push a given number of levels onto the assertion stack";
+ let arguments = (ins ConfinedAttr<I32Attr, [IntNonNegative]>:$count);
+ let assemblyFormat = "$count attr-dict";
+}
+
+def PopOp : SMTOp<"pop", []> {
+ let summary = "pop a given number of levels from the assertion stack";
+ let arguments = (ins ConfinedAttr<I32Attr, [IntNonNegative]>:$count);
+ let assemblyFormat = "$count attr-dict";
+}
+
+def CheckOp : SMTOp<"check", [
+ NoRegionArguments,
+ SingleBlockImplicitTerminator<"smt::YieldOp">,
+]> {
+ let summary = "check if the current set of assertions is satisfiable";
+ let description = [{
+ This operation checks if all the assertions in the solver defined by the
+ nearest ancestor operation of type `smt.solver` are consistent. The outcome
+ an be 'satisfiable', 'unknown', or 'unsatisfiable' and the corresponding
+ region will be executed. It is the corresponding construct to the
+ `check-sat` in SMT-LIB.
+
+ Example:
+ ```mlir
+ %0 = smt.check sat {
+ %c1_i32 = arith.constant 1 : i32
+ smt.yield %c1_i32 : i32
+ } unknown {
+ %c0_i32 = arith.constant 0 : i32
+ smt.yield %c0_i32 : i32
+ } unsat {
+ %c-1_i32 = arith.constant -1 : i32
+ smt.yield %c-1_i32 : i32
+ } -> i32
+ ```
+ }];
+
+ let regions = (region SizedRegion<1>:$satRegion,
+ SizedRegion<1>:$unknownRegion,
+ SizedRegion<1>:$unsatRegion);
+ let results = (outs Variadic<AnyType>:$results);
+
+ let assemblyFormat = [{
+ attr-dict `sat` $satRegion `unknown` $unknownRegion `unsat` $unsatRegion
+ (`->` qualified(type($results))^ )?
+ }];
+
+ let hasRegionVerifier = true;
+}
+
+def YieldOp : SMTOp<"yield", [
+ Pure,
+ Terminator,
+ ReturnLike,
+ ParentOneOf<["smt::SolverOp", "smt::CheckOp",
+ "smt::ForallOp", "smt::ExistsOp"]>,
+]> {
+ let summary = "terminator operation for various regions of SMT operations";
+ let arguments = (ins Variadic<AnyType>:$values);
+ let assemblyFormat = "($values^ `:` qualified(type($values)))? attr-dict";
+ let builders = [OpBuilder<(ins), [{
+ build($_builder, $_state, std::nullopt);
+ }]>];
+}
+
+def ApplyFuncOp : SMTOp<"apply_func", [
+ Pure,
+ TypesMatchWith<"summary", "func", "result",
+ "cast<SMTFuncType>($_self).getRangeType()">,
+ RangedTypesMatchWith<"summary", "func", "args",
+ "cast<SMTFuncType>($_self).getDomainTypes()">
+]> {
+ let summary = "apply a function";
+ let description = [{
+ This operation performs a function application as described in the
+ [SMT-LIB 2.6 standard](https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf).
+ It is part of the language itself rather than a theory or logic.
+ }];
+
+ let arguments = (ins SMTFuncType:$func,
+ Variadic<AnyNonFuncSMTType>:$args);
+ let results = (outs AnyNonFuncSMTType:$result);
+
+ let assemblyFormat = [{
+ $func `(` $args `)` attr-dict `:` qualified(type($func))
+ }];
+}
+
+def EqOp : SMTOp<"eq", [Pure, SameTypeOperands]> {
+ let summary = "returns true iff all operands are identical";
+ let description = [{
+ This operation compares the operands and returns true iff all operands are
+ identical. The semantics are equivalent to the `=` operator defined in the
+ SMT-LIB Standard 2.6 in the
+ [Core theory](https://smtlib.cs.uiowa.edu/Theories/Core.smt2).
+
+ Any SMT sort/type is allowed for the operands and it supports a variadic
+ number of operands, but requires at least two. This is because the `=`
+ operator is annotated with `:chainable` which means that `= a b c d` is
+ equivalent to `and (= a b) (= b c) (= c d)` where `and` is annotated
+ `:left-assoc`, i.e., it can be further rewritten to
+ `and (and (= a b) (= b c)) (= c d)`.
+ }];
+
+ let arguments = (ins Variadic<AnyNonFuncSMTType>:$inputs);
+ let results = (outs BoolType:$result);
+
+ let builders = [
+ OpBuilder<(ins "mlir::Value":$lhs, "mlir::Value":$rhs), [{
+ build($_builder, $_state, ValueRange{lhs, rhs});
+ }]>
+ ];
+
+ let hasCustomAssemblyFormat = true;
+ let hasVerifier = true;
+}
+
+def DistinctOp : SMTOp<"distinct", [Pure, SameTypeOperands]> {
+ let summary = "returns true iff all operands are not identical to any other";
+ let description = [{
+ This operation compares the operands and returns true iff all operands are
+ not identical to any of the other operands. The semantics are equivalent to
+ the `distinct` operator defined in the SMT-LIB Standard 2.6 in the
+ [Core theory](https://smtlib.cs.uiowa.edu/Theories/Core.smt2).
+
+ Any SMT sort/type is allowed for the operands and it supports a variadic
+ number of operands, but requires at least two. This is because the
+ `distinct` operator is annotated with `:pairwise` which means that
+ `distinct a b c d` is equivalent to
+ ```
+ and (distinct a b) (distinct a c) (distinct a d)
+ (distinct b c) (distinct b d)
+ (distinct c d)
+ ```
+ where `and` is annotated `:left-assoc`, i.e., it can be further rewritten to
+ ```
+ (and (and (and (and (and (distinct a b)
+ (distinct a c))
+ (distinct a d))
+ (distinct b c))
+ (distinct b d))
+ (distinct c d)
+ ```
+ }];
+
+ let arguments = (ins Variadic<AnyNonFuncSMTType>:$inputs);
+ let results = (outs BoolType:$result);
+
+ let builders = [
+ OpBuilder<(ins "mlir::Value":$lhs, "mlir::Value":$rhs), [{
+ build($_builder, $_state, ValueRange{lhs, rhs});
+ }]>
+ ];
+
+ let hasCustomAssemblyFormat = true;
+ let hasVerifier = true;
+}
+
+def IteOp : SMTOp<"ite", [
+ Pure,
+ AllTypesMatch<["thenValue", "elseValue", "result"]>
+]> {
+ let summary = "an if-then-else function";
+ let description = [{
+ This operation returns its second operand or its third operand depending on
+ whether its first operand is true or not. The semantics are equivalent to
+ the `ite` operator defined in the
+ [Core theory](https://smtlib.cs.uiowa.edu/Theories/Core.smt2) of the SMT-LIB
+ 2.6 standard.
+ }];
+
+ let arguments = (ins BoolType:$cond,
+ AnySMTType:$thenValue,
+ AnySMTType:$elseValue);
+ let results = (outs AnySMTType:$result);
+
+ let assemblyFormat = [{
+ $cond `,` $thenValue `,` $elseValue attr-dict `:` qualified(type($result))
+ }];
+}
+
+def NotOp : SMTOp<"not", [Pure]> {
+ let summary = "a boolean negation";
+ let description = [{
+ This operation performs a boolean negation. The semantics are equivalent to
+ the 'not' operator in the
+ [Core theory](https://smtlib.cs.uiowa.edu/Theories/Core.smt2) of the SMT-LIB
+ Standard 2.6.
+ }];
+
+ let arguments = (ins BoolType:$input);
+ let results = (outs BoolType:$result);
+ let assemblyFormat = "$input attr-dict";
+}
+
+class VariadicBoolOp<string mnemonic, string desc> : SMTOp<mnemonic, [Pure]> {
+ let summary = desc;
+ let description = "This operation performs " # desc # [{.
+ The semantics are equivalent to the '}] # mnemonic # [{' operator in the
+ [Core theory](https://smtlib.cs.uiowa.edu/Theories/Core.smt2).
+ of the SMT-LIB Standard 2.6.
+
+ It supports a variadic number of operands, but requires at least two.
+ This is because the operator is annotated with the `:left-assoc` attribute
+ which means that `op a b c` is equivalent to `(op (op a b) c)`.
+ }];
+
+ let arguments = (ins Variadic<BoolType>:$inputs);
+ let results = (outs BoolType:$result);
+ let assemblyFormat = "$inputs attr-dict";
+
+ let builders = [
+ OpBuilder<(ins "mlir::Value":$lhs, "mlir::Value":$rhs), [{
+ build($_builder, $_state, ValueRange{lhs, rhs});
+ }]>
+ ];
+}
+
+def AndOp : VariadicBoolOp<"and", "a boolean conjunction">;
+def OrOp : VariadicBoolOp<"or", "a boolean disjunction">;
+def XOrOp : VariadicBoolOp<"xor", "a boolean exclusive OR">;
+
+def ImpliesOp : SMTOp<"implies", [Pure]> {
+ let summary = "boolean implication";
+ let description = [{
+ This operation performs a boolean implication. The semantics are equivalent
+ to the '=>' operator in the
+ [Core theory](https://smtlib.cs.uiowa.edu/Theories/Core.smt2) of the SMT-LIB
+ Standard 2.6.
+ }];
+
+ let arguments = (ins BoolType:$lhs, BoolType:$rhs);
+ let results = (outs BoolType:$result);
+ let assemblyFormat = "$lhs `,` $rhs attr-dict";
+}
+
+class QuantifierOp<string mnemonic> : SMTOp<mnemonic, [
+ RecursivelySpeculatable,
+ RecursiveMemoryEffects,
+ SingleBlockImplicitTerminator<"smt::YieldOp">,
+]> {
+ let description = [{
+ This operation represents the }] # summary # [{ as described in the
+ [SMT-LIB 2.6 standard](https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf).
+ It is part of the language itself rather than a theory or logic.
+
+ The operation specifies the name prefixes (as an optional attribute) and
+ types (as the types of the block arguments of the regions) of bound
+ variables that may be used in the 'body' of the operation. If a 'patterns'
+ region is specified, the block arguments must match the ones of the 'body'
+ region and (other than there) must be used at least once in the 'patterns'
+ region. It may also not contain any operations that bind variables, such as
+ quantifiers. While the 'body' region must always yield exactly one
+ `!smt.bool`-typed value, the 'patterns' region can yield an arbitrary number
+ (but at least one) of SMT values.
+
+ The bound variables can be any SMT type except of functions, since SMT only
+ supports first-order logic.
+
+ The 'no_patterns' attribute is only allowed when no 'patterns' region is
+ specified and forbids the solver to generate and use patterns for this
+ quantifier.
+
+ The 'weight' attribute indicates the importance of this quantifier being
+ instantiated compared to other quantifiers that may be present. The default
+ value is zero.
+
+ Both the 'no_patterns' and 'weight' attributes are annotations to the
+ quantifiers body term. Annotations and attributes are described in the
+ standard in sections 3.4, and 3.6 (specifically 3.6.5). SMT-LIB allows
+ adding custom attributes to provide solvers with additional metadata, e.g.,
+ hints such as above mentioned attributes. They are not part of the standard
+ themselves, but supported by common SMT solvers (e.g., Z3).
+ }];
+
+ let arguments = (ins DefaultValuedAttr<I32Attr, "0">:$weight,
+ UnitAttr:$noPattern,
+ OptionalAttr<StrArrayAttr>:$boundVarNames);
+ let regions = (region SizedRegion<1>:$body,
+ VariadicRegion<SizedRegion<1>>:$patterns);
+ let results = (outs BoolType:$result);
+
+ let builders = [
+ OpBuilder<(ins
+ "TypeRange":$boundVarTypes,
+ "function_ref<Value(OpBuilder &, Location, ValueRange)>":$bodyBuilder,
+ CArg<"std::optional<ArrayRef<StringRef>>", "std::nullopt">:$boundVarNames,
+ CArg<"function_ref<ValueRange(OpBuilder &, Location, ValueRange)>",
+ "{}">:$patternBuilder,
+ CArg<"uint32_t", "0">:$weight,
+ CArg<"bool", "false">:$noPattern)>
+ ];
+ let skipDefaultBuilders = true;
+
+ let assemblyFormat = [{
+ ($boundVarNames^)? (`no_pattern` $noPattern^)? (`weight` $weight^)?
+ attr-dict-with-keyword $body (`patterns` $patterns^)?
+ }];
+
+ let hasVerifier = true;
+ let hasRegionVerifier = true;
+}
+
+def ForallOp : QuantifierOp<"forall"> { let summary = "forall quantifier"; }
+def ExistsOp : QuantifierOp<"exists"> { let summary = "exists quantifier"; }
+
+#endif // MLIR_DIALECT_SMT_SMTOPS_TD
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTTypes.h b/mlir/include/mlir/Dialect/SMT/IR/SMTTypes.h
new file mode 100644
index 0000000000000..4db28f7a07a41
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTTypes.h
@@ -0,0 +1,30 @@
+//===- SMTTypes.h - SMT dialect types ---------------------------*- 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
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef MLIR_DIALECT_SMT_SMTTYPES_H
+#define MLIR_DIALECT_SMT_SMTTYPES_H
+
+#include "mlir/IR/BuiltinTypes.h"
+#include "mlir/IR/Types.h"
+
+#define GET_TYPEDEF_CLASSES
+#include "mlir/Dialect/SMT/IR/SMTTypes.h.inc"
+
+namespace mlir {
+namespace smt {
+
+/// Returns whether the given type is an SMT value type.
+bool isAnySMTValueType(mlir::Type type);
+
+/// Returns whether the given type is an SMT value type (excluding functions).
+bool isAnyNonFuncSMTValueType(mlir::Type type);
+
+} // namespace smt
+} // namespace mlir
+
+#endif // MLIR_DIALECT_SMT_SMTTYPES_H
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTTypes.td b/mlir/include/mlir/Dialect/SMT/IR/SMTTypes.td
new file mode 100644
index 0000000000000..3032900b52178
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTTypes.td
@@ -0,0 +1,145 @@
+//===- SMTTypes.td - SMT dialect types ---------------------*- tablegen -*-===//
+//
+// 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
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef MLIR_DIALECT_SMT_SMTTYPES_TD
+#define MLIR_DIALECT_SMT_SMTTYPES_TD
+
+include "mlir/Dialect/SMT/IR/SMTDialect.td"
+include "mlir/IR/AttrTypeBase.td"
+
+class SMTTypeDef<string name> : TypeDef<SMTDialect, name> { }
+
+def BoolType : SMTTypeDef<"Bool"> {
+ let mnemonic = "bool";
+ let assemblyFormat = "";
+}
+
+def IntType : SMTTypeDef<"Int"> {
+ let mnemonic = "int";
+ let description = [{
+ This type represents the `Int` sort as described in the
+ [SMT Ints theory](https://smtlib.cs.uiowa.edu/Theories/Ints.smt2) of the
+ SMT-LIB 2.6 standard.
+ }];
+ let assemblyFormat = "";
+}
+
+def BitVectorType : SMTTypeDef<"BitVector"> {
+ let mnemonic = "bv";
+ let description = [{
+ This type represents the `(_ BitVec width)` sort as described in the
+ [SMT bit-vector
+ theory](https://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml).
+
+ The bit-width must be strictly greater than zero.
+ }];
+
+ let parameters = (ins "int64_t":$width);
+ let assemblyFormat = "`<` $width `>`";
+
+ let genVerifyDecl = true;
+}
+
+def ArrayType : SMTTypeDef<"Array"> {
+ let mnemonic = "array";
+ let description = [{
+ This type represents the `(Array X Y)` sort, where X and Y are any
+ sort/type, as described in the
+ [SMT ArrayEx theory](https://smtlib.cs.uiowa.edu/Theories/ArraysEx.smt2) of
+ the SMT-LIB standard 2.6.
+ }];
+
+ let parameters = (ins "mlir::Type":$domainType, "mlir::Type":$rangeType);
+ let assemblyFormat = "`<` `[` $domainType `->` $rangeType `]` `>`";
+
+ let genVerifyDecl = true;
+}
+
+def SMTFuncType : SMTTypeDef<"SMTFunc"> {
+ let mnemonic = "func";
+ let description = [{
+ This type represents the SMT function sort as described in the
+ [SMT-LIB 2.6 standard](https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf).
+ It is part of the language itself rather than a theory or logic.
+
+ A function in SMT can have an arbitrary domain size, but always has exactly
+ one range sort.
+
+ Since SMT only supports first-order logic, it is not possible to nest
+ function types.
+
+ Example: `!smt.func<(!smt.bool, !smt.int) !smt.bool>` is equivalent to
+ `((Bool Int) Bool)` in SMT-LIB.
+ }];
+
+ let parameters = (ins
+ ArrayRefParameter<"mlir::Type", "domain types">:$domainTypes,
+ "mlir::Type":$rangeType
+ );
+
+ // Note: We are not printing the parentheses when no domain type is present
+ // because the default MLIR parser thinks it is a builtin function type
+ // otherwise.
+ let assemblyFormat = "`<` `(` $domainTypes `)` ` ` $rangeType `>`";
+
+ let builders = [
+ TypeBuilderWithInferredContext<(ins
+ "llvm::ArrayRef<mlir::Type>":$domainTypes,
+ "mlir::Type":$rangeType), [{
+ return $_get(rangeType.getContext(), domainTypes, rangeType);
+ }]>,
+ TypeBuilderWithInferredContext<(ins "mlir::Type":$rangeType), [{
+ return $_get(rangeType.getContext(),
+ llvm::ArrayRef<mlir::Type>{}, rangeType);
+ }]>
+ ];
+
+ let genVerifyDecl = true;
+}
+
+def SortType : SMTTypeDef<"Sort"> {
+ let mnemonic = "sort";
+ let description = [{
+ This type represents uninterpreted sorts. The usage of a type like
+ `!smt.sort<"sort_name"[!smt.bool, !smt.sort<"other_sort">]>` implies a
+ `declare-sort sort_name 2` and a `declare-sort other_sort 0` in SMT-LIB.
+ This type represents concrete use-sites of such declared sorts, in this
+ particular case it would be equivalent to `(sort_name Bool other_sort)` in
+ SMT-LIB. More details about the semantics can be found in the
+ [SMT-LIB 2.6 standard](https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf).
+ }];
+
+ let parameters = (ins
+ "mlir::StringAttr":$identifier,
+ OptionalArrayRefParameter<"mlir::Type", "sort parameters">:$sortParams
+ );
+
+ let assemblyFormat = "`<` $identifier (`[` $sortParams^ `]`)? `>`";
+
+ let builders = [
+ TypeBuilder<(ins "llvm::StringRef":$identifier,
+ "llvm::ArrayRef<mlir::Type>":$sortParams), [{
+ return $_get($_ctxt, mlir::StringAttr::get($_ctxt, identifier),
+ sortParams);
+ }]>,
+ TypeBuilder<(ins "llvm::StringRef":$identifier), [{
+ return $_get($_ctxt, mlir::StringAttr::get($_ctxt, identifier),
+ llvm::ArrayRef<mlir::Type>{});
+ }]>,
+ ];
+
+ let genVerifyDecl = true;
+}
+
+def AnySMTType : Type<CPred<"smt::isAnySMTValueType($_self)">,
+ "any SMT value type">;
+def AnyNonFuncSMTType : Type<CPred<"smt::isAnyNonFuncSMTValueType($_self)">,
+ "any non-function SMT value type">;
+def AnyNonSMTType : Type<Neg<AnySMTType.predicate>, "any non-smt type">;
+
+#endif // MLIR_DIALECT_SMT_SMTTYPES_TD
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTVisitors.h b/mlir/include/mlir/Dialect/SMT/IR/SMTVisitors.h
new file mode 100644
index 0000000000000..38fad21019158
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTVisitors.h
@@ -0,0 +1,201 @@
+//===- SMTVisitors.h - SMT Dialect Visitors ---------------------*- 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 defines visitors that make it easier to work with the SMT IR.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef MLIR_DIALECT_SMT_SMTVISITORS_H
+#define MLIR_DIALECT_SMT_SMTVISITORS_H
+
+#include "mlir/Dialect/SMT/IR/SMTOps.h"
+#include "llvm/ADT/TypeSwitch.h"
+
+namespace mlir {
+namespace smt {
+
+/// This helps visit SMT nodes.
+template <typename ConcreteType, typename ResultType = void,
+ typename... ExtraArgs>
+class SMTOpVisitor {
+public:
+ ResultType dispatchSMTOpVisitor(Operation *op, ExtraArgs... args) {
+ auto *thisCast = static_cast<ConcreteType *>(this);
+ return TypeSwitch<Operation *, ResultType>(op)
+ .template Case<
+ // Constants
+ BoolConstantOp, IntConstantOp, BVConstantOp,
+ // Bit-vector arithmetic
+ BVNegOp, BVAddOp, BVMulOp, BVURemOp, BVSRemOp, BVSModOp, BVShlOp,
+ BVLShrOp, BVAShrOp, BVUDivOp, BVSDivOp,
+ // Bit-vector bitwise
+ BVNotOp, BVAndOp, BVOrOp, BVXOrOp,
+ // Other bit-vector ops
+ ConcatOp, ExtractOp, RepeatOp, BVCmpOp, BV2IntOp,
+ // Int arithmetic
+ IntAddOp, IntMulOp, IntSubOp, IntDivOp, IntModOp, IntCmpOp,
+ Int2BVOp,
+ // Core Ops
+ EqOp, DistinctOp, IteOp,
+ // Variable/symbol declaration
+ DeclareFunOp, ApplyFuncOp,
+ // solver interaction
+ SolverOp, AssertOp, ResetOp, PushOp, PopOp, CheckOp, SetLogicOp,
+ // Boolean logic
+ NotOp, AndOp, OrOp, XOrOp, ImpliesOp,
+ // Arrays
+ ArrayStoreOp, ArraySelectOp, ArrayBroadcastOp,
+ // Quantifiers
+ ForallOp, ExistsOp, YieldOp>([&](auto expr) -> ResultType {
+ return thisCast->visitSMTOp(expr, args...);
+ })
+ .Default([&](auto expr) -> ResultType {
+ return thisCast->visitInvalidSMTOp(op, args...);
+ });
+ }
+
+ /// This callback is invoked on any non-expression operations.
+ ResultType visitInvalidSMTOp(Operation *op, ExtraArgs... args) {
+ op->emitOpError("unknown SMT node");
+ abort();
+ }
+
+ /// This callback is invoked on any SMT operations that are not
+ /// handled by the concrete visitor.
+ ResultType visitUnhandledSMTOp(Operation *op, ExtraArgs... args) {
+ return ResultType();
+ }
+
+#define HANDLE(OPTYPE, OPKIND) \
+ ResultType visitSMTOp(OPTYPE op, ExtraArgs... args) { \
+ return static_cast<ConcreteType *>(this)->visit##OPKIND##SMTOp(op, \
+ args...); \
+ }
+
+ // Constants
+ HANDLE(BoolConstantOp, Unhandled);
+ HANDLE(IntConstantOp, Unhandled);
+ HANDLE(BVConstantOp, Unhandled);
+
+ // Bit-vector arithmetic
+ HANDLE(BVNegOp, Unhandled);
+ HANDLE(BVAddOp, Unhandled);
+ HANDLE(BVMulOp, Unhandled);
+ HANDLE(BVURemOp, Unhandled);
+ HANDLE(BVSRemOp, Unhandled);
+ HANDLE(BVSModOp, Unhandled);
+ HANDLE(BVShlOp, Unhandled);
+ HANDLE(BVLShrOp, Unhandled);
+ HANDLE(BVAShrOp, Unhandled);
+ HANDLE(BVUDivOp, Unhandled);
+ HANDLE(BVSDivOp, Unhandled);
+
+ // Bit-vector bitwise operations
+ HANDLE(BVNotOp, Unhandled);
+ HANDLE(BVAndOp, Unhandled);
+ HANDLE(BVOrOp, Unhandled);
+ HANDLE(BVXOrOp, Unhandled);
+
+ // Other bit-vector operations
+ HANDLE(ConcatOp, Unhandled);
+ HANDLE(ExtractOp, Unhandled);
+ HANDLE(RepeatOp, Unhandled);
+ HANDLE(BVCmpOp, Unhandled);
+ HANDLE(BV2IntOp, Unhandled);
+
+ // Int arithmetic
+ HANDLE(IntAddOp, Unhandled);
+ HANDLE(IntMulOp, Unhandled);
+ HANDLE(IntSubOp, Unhandled);
+ HANDLE(IntDivOp, Unhandled);
+ HANDLE(IntModOp, Unhandled);
+
+ HANDLE(IntCmpOp, Unhandled);
+ HANDLE(Int2BVOp, Unhandled);
+
+ HANDLE(EqOp, Unhandled);
+ HANDLE(DistinctOp, Unhandled);
+ HANDLE(IteOp, Unhandled);
+
+ HANDLE(DeclareFunOp, Unhandled);
+ HANDLE(ApplyFuncOp, Unhandled);
+
+ HANDLE(SolverOp, Unhandled);
+ HANDLE(AssertOp, Unhandled);
+ HANDLE(ResetOp, Unhandled);
+ HANDLE(PushOp, Unhandled);
+ HANDLE(PopOp, Unhandled);
+ HANDLE(CheckOp, Unhandled);
+ HANDLE(SetLogicOp, Unhandled);
+
+ // Boolean logic operations
+ HANDLE(NotOp, Unhandled);
+ HANDLE(AndOp, Unhandled);
+ HANDLE(OrOp, Unhandled);
+ HANDLE(XOrOp, Unhandled);
+ HANDLE(ImpliesOp, Unhandled);
+
+ // Array operations
+ HANDLE(ArrayStoreOp, Unhandled);
+ HANDLE(ArraySelectOp, Unhandled);
+ HANDLE(ArrayBroadcastOp, Unhandled);
+
+ // Quantifier operations
+ HANDLE(ForallOp, Unhandled);
+ HANDLE(ExistsOp, Unhandled);
+ HANDLE(YieldOp, Unhandled);
+
+#undef HANDLE
+};
+
+/// This helps visit SMT types.
+template <typename ConcreteType, typename ResultType = void,
+ typename... ExtraArgs>
+class SMTTypeVisitor {
+public:
+ ResultType dispatchSMTTypeVisitor(Type type, ExtraArgs... args) {
+ auto *thisCast = static_cast<ConcreteType *>(this);
+ return TypeSwitch<Type, ResultType>(type)
+ .template Case<BoolType, IntType, BitVectorType, ArrayType, SMTFuncType,
+ SortType>([&](auto expr) -> ResultType {
+ return thisCast->visitSMTType(expr, args...);
+ })
+ .Default([&](auto expr) -> ResultType {
+ return thisCast->visitInvalidSMTType(type, args...);
+ });
+ }
+
+ /// This callback is invoked on any non-expression types.
+ ResultType visitInvalidSMTType(Type type, ExtraArgs... args) { abort(); }
+
+ /// This callback is invoked on any SMT type that are not
+ /// handled by the concrete visitor.
+ ResultType visitUnhandledSMTType(Type type, ExtraArgs... args) {
+ return ResultType();
+ }
+
+#define HANDLE(TYPE, KIND) \
+ ResultType visitSMTType(TYPE op, ExtraArgs... args) { \
+ return static_cast<ConcreteType *>(this)->visit##KIND##SMTType(op, \
+ args...); \
+ }
+
+ HANDLE(BoolType, Unhandled);
+ HANDLE(IntegerType, Unhandled);
+ HANDLE(BitVectorType, Unhandled);
+ HANDLE(ArrayType, Unhandled);
+ HANDLE(SMTFuncType, Unhandled);
+ HANDLE(SortType, Unhandled);
+
+#undef HANDLE
+};
+
+} // namespace smt
+} // namespace mlir
+
+#endif // MLIR_DIALECT_SMT_SMTVISITORS_H
diff --git a/mlir/include/mlir/InitAllDialects.h b/mlir/include/mlir/InitAllDialects.h
index 33bc89279c08c..e83be7b40eded 100644
--- a/mlir/include/mlir/InitAllDialects.h
+++ b/mlir/include/mlir/InitAllDialects.h
@@ -73,6 +73,7 @@
#include "mlir/Dialect/SCF/TransformOps/SCFTransformOps.h"
#include "mlir/Dialect/SCF/Transforms/BufferDeallocationOpInterfaceImpl.h"
#include "mlir/Dialect/SCF/Transforms/BufferizableOpInterfaceImpl.h"
+#include "mlir/Dialect/SMT/IR/SMTDialect.h"
#include "mlir/Dialect/SPIRV/IR/SPIRVDialect.h"
#include "mlir/Dialect/Shape/IR/Shape.h"
#include "mlir/Dialect/Shape/Transforms/BufferizableOpInterfaceImpl.h"
@@ -143,6 +144,7 @@ inline void registerAllDialects(DialectRegistry ®istry) {
ROCDL::ROCDLDialect,
scf::SCFDialect,
shape::ShapeDialect,
+ smt::SMTDialect,
sparse_tensor::SparseTensorDialect,
spirv::SPIRVDialect,
tensor::TensorDialect,
diff --git a/mlir/lib/Dialect/CMakeLists.txt b/mlir/lib/Dialect/CMakeLists.txt
index 80b0ef068d96d..a473f2ff317c9 100644
--- a/mlir/lib/Dialect/CMakeLists.txt
+++ b/mlir/lib/Dialect/CMakeLists.txt
@@ -33,6 +33,7 @@ add_subdirectory(Ptr)
add_subdirectory(Quant)
add_subdirectory(SCF)
add_subdirectory(Shape)
+add_subdirectory(SMT)
add_subdirectory(SparseTensor)
add_subdirectory(SPIRV)
add_subdirectory(Tensor)
diff --git a/mlir/lib/Dialect/SMT/CMakeLists.txt b/mlir/lib/Dialect/SMT/CMakeLists.txt
new file mode 100644
index 0000000000000..f33061b2d87cf
--- /dev/null
+++ b/mlir/lib/Dialect/SMT/CMakeLists.txt
@@ -0,0 +1 @@
+add_subdirectory(IR)
diff --git a/mlir/lib/Dialect/SMT/IR/CMakeLists.txt b/mlir/lib/Dialect/SMT/IR/CMakeLists.txt
new file mode 100644
index 0000000000000..e287613da9fd0
--- /dev/null
+++ b/mlir/lib/Dialect/SMT/IR/CMakeLists.txt
@@ -0,0 +1,27 @@
+add_mlir_dialect_library(MLIRSMT
+ SMTAttributes.cpp
+ SMTDialect.cpp
+ SMTOps.cpp
+ SMTTypes.cpp
+
+ ADDITIONAL_HEADER_DIRS
+ ${MLIR_MAIN_INCLUDE_DIR}/mlir/Dialect/SMT
+
+ DEPENDS
+ MLIRSMTAttrIncGen
+ MLIRSMTEnumsIncGen
+ MLIRSMTIncGen
+
+ LINK_COMPONENTS
+ Support
+
+ LINK_LIBS PUBLIC
+ MLIRIR
+ MLIRInferTypeOpInterface
+ MLIRSideEffectInterfaces
+ MLIRControlFlowInterfaces
+)
+
+add_dependencies(mlir-headers
+ MLIRSMTIncGen
+)
diff --git a/mlir/lib/Dialect/SMT/IR/SMTAttributes.cpp b/mlir/lib/Dialect/SMT/IR/SMTAttributes.cpp
new file mode 100644
index 0000000000000..c28f3558a02d2
--- /dev/null
+++ b/mlir/lib/Dialect/SMT/IR/SMTAttributes.cpp
@@ -0,0 +1,201 @@
+//===- SMTAttributes.cpp - Implement SMT attributes -----------------------===//
+//
+// 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
+//
+//===----------------------------------------------------------------------===//
+
+#include "mlir/Dialect/SMT/IR/SMTAttributes.h"
+#include "mlir/Dialect/SMT/IR/SMTDialect.h"
+#include "mlir/Dialect/SMT/IR/SMTTypes.h"
+#include "mlir/IR/Builders.h"
+#include "mlir/IR/DialectImplementation.h"
+#include "llvm/ADT/TypeSwitch.h"
+#include "llvm/Support/Format.h"
+
+using namespace mlir;
+using namespace mlir::smt;
+
+//===----------------------------------------------------------------------===//
+// BitVectorAttr
+//===----------------------------------------------------------------------===//
+
+namespace mlir {
+namespace smt {
+namespace detail {
+struct BitVectorAttrStorage : public mlir::AttributeStorage {
+ using KeyTy = APInt;
+ BitVectorAttrStorage(APInt value) : value(std::move(value)) {}
+
+ KeyTy getAsKey() const { return value; }
+
+ // NOTE: the implementation of this operator is the reason we need to define
+ // the storage manually. The auto-generated version would just do the direct
+ // equality check of the APInt, but that asserts the bitwidth of both to be
+ // the same, leading to a crash. This implementation, therefore, checks for
+ // matching bit-width beforehand.
+ bool operator==(const KeyTy &key) const {
+ return (value.getBitWidth() == key.getBitWidth() && value == key);
+ }
+
+ static llvm::hash_code hashKey(const KeyTy &key) {
+ return llvm::hash_value(key);
+ }
+
+ static BitVectorAttrStorage *
+ construct(mlir::AttributeStorageAllocator &allocator, KeyTy &&key) {
+ return new (allocator.allocate<BitVectorAttrStorage>())
+ BitVectorAttrStorage(std::move(key));
+ }
+
+ APInt value;
+};
+} // namespace detail
+} // namespace smt
+} // namespace mlir
+
+APInt BitVectorAttr::getValue() const { return getImpl()->value; }
+
+LogicalResult BitVectorAttr::verify(
+ function_ref<InFlightDiagnostic()> emitError,
+ APInt value) { // NOLINT(performance-unnecessary-value-param)
+ if (value.getBitWidth() < 1)
+ return emitError() << "bit-width must be at least 1, but got "
+ << value.getBitWidth();
+ return success();
+}
+
+std::string BitVectorAttr::getValueAsString(bool prefix) const {
+ unsigned width = getValue().getBitWidth();
+ SmallVector<char> toPrint;
+ StringRef pref = prefix ? "#" : "";
+ if (width % 4 == 0) {
+ getValue().toString(toPrint, 16, false, false, false);
+ // APInt's 'toString' omits leading zeros. However, those are critical here
+ // because they determine the bit-width of the bit-vector.
+ SmallVector<char> leadingZeros(width / 4 - toPrint.size(), '0');
+ return (pref + "x" + Twine(leadingZeros) + toPrint).str();
+ }
+
+ getValue().toString(toPrint, 2, false, false, false);
+ // APInt's 'toString' omits leading zeros
+ SmallVector<char> leadingZeros(width - toPrint.size(), '0');
+ return (pref + "b" + Twine(leadingZeros) + toPrint).str();
+}
+
+/// Parse an SMT-LIB formatted bit-vector string.
+static FailureOr<APInt>
+parseBitVectorString(function_ref<InFlightDiagnostic()> emitError,
+ StringRef value) {
+ if (value[0] != '#')
+ return emitError() << "expected '#'";
+
+ if (value.size() < 3)
+ return emitError() << "expected at least one digit";
+
+ if (value[1] == 'b')
+ return APInt(value.size() - 2, std::string(value.begin() + 2, value.end()),
+ 2);
+
+ if (value[1] == 'x')
+ return APInt((value.size() - 2) * 4,
+ std::string(value.begin() + 2, value.end()), 16);
+
+ return emitError() << "expected either 'b' or 'x'";
+}
+
+BitVectorAttr BitVectorAttr::get(MLIRContext *context, StringRef value) {
+ auto maybeValue = parseBitVectorString(nullptr, value);
+
+ assert(succeeded(maybeValue) && "string must have SMT-LIB format");
+ return Base::get(context, *maybeValue);
+}
+
+BitVectorAttr
+BitVectorAttr::getChecked(function_ref<InFlightDiagnostic()> emitError,
+ MLIRContext *context, StringRef value) {
+ auto maybeValue = parseBitVectorString(emitError, value);
+ if (failed(maybeValue))
+ return {};
+
+ return Base::getChecked(emitError, context, *maybeValue);
+}
+
+BitVectorAttr BitVectorAttr::get(MLIRContext *context, uint64_t value,
+ unsigned width) {
+ return Base::get(context, APInt(width, value));
+}
+
+BitVectorAttr
+BitVectorAttr::getChecked(function_ref<InFlightDiagnostic()> emitError,
+ MLIRContext *context, uint64_t value,
+ unsigned width) {
+ if (width < 64 && value >= (UINT64_C(1) << width)) {
+ emitError() << "value does not fit in a bit-vector of desired width";
+ return {};
+ }
+ return Base::getChecked(emitError, context, APInt(width, value));
+}
+
+Attribute BitVectorAttr::parse(AsmParser &odsParser, Type odsType) {
+ llvm::SMLoc loc = odsParser.getCurrentLocation();
+
+ APInt val;
+ if (odsParser.parseLess() || odsParser.parseInteger(val) ||
+ odsParser.parseGreater())
+ return {};
+
+ // Requires the use of `quantified(<attr>)` in operation assembly formats.
+ if (!odsType || !llvm::isa<BitVectorType>(odsType)) {
+ odsParser.emitError(loc) << "explicit bit-vector type required";
+ return {};
+ }
+
+ unsigned width = llvm::cast<BitVectorType>(odsType).getWidth();
+
+ if (width > val.getBitWidth()) {
+ // sext is always safe here, even for unsigned values, because the
+ // parseOptionalInteger method will return something with a zero in the
+ // top bits if it is a positive number.
+ val = val.sext(width);
+ } else if (width < val.getBitWidth()) {
+ // The parser can return an unnecessarily wide result.
+ // This isn't a problem, but truncating off bits is bad.
+ unsigned neededBits =
+ val.isNegative() ? val.getSignificantBits() : val.getActiveBits();
+ if (width < neededBits) {
+ odsParser.emitError(loc)
+ << "integer value out of range for given bit-vector type " << odsType;
+ return {};
+ }
+ val = val.trunc(width);
+ }
+
+ return BitVectorAttr::get(odsParser.getContext(), val);
+}
+
+void BitVectorAttr::print(AsmPrinter &odsPrinter) const {
+ // This printer only works for the extended format where the MLIR
+ // infrastructure prints the type for us. This means, the attribute should
+ // never be used without `quantified` in an assembly format.
+ odsPrinter << "<" << getValue() << ">";
+}
+
+Type BitVectorAttr::getType() const {
+ return BitVectorType::get(getContext(), getValue().getBitWidth());
+}
+
+//===----------------------------------------------------------------------===//
+// ODS Boilerplate
+//===----------------------------------------------------------------------===//
+
+#define GET_ATTRDEF_CLASSES
+#include "mlir/Dialect/SMT/IR/SMTAttributes.cpp.inc"
+
+void SMTDialect::registerAttributes() {
+ addAttributes<
+#define GET_ATTRDEF_LIST
+#include "mlir/Dialect/SMT/IR/SMTAttributes.cpp.inc"
+ >();
+}
diff --git a/mlir/lib/Dialect/SMT/IR/SMTDialect.cpp b/mlir/lib/Dialect/SMT/IR/SMTDialect.cpp
new file mode 100644
index 0000000000000..66eed861b2bb7
--- /dev/null
+++ b/mlir/lib/Dialect/SMT/IR/SMTDialect.cpp
@@ -0,0 +1,47 @@
+//===- SMTDialect.cpp - SMT dialect implementation ------------------------===//
+//
+// 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
+//
+//===----------------------------------------------------------------------===//
+
+#include "mlir/Dialect/SMT/IR/SMTDialect.h"
+#include "mlir/Dialect/SMT/IR/SMTAttributes.h"
+#include "mlir/Dialect/SMT/IR/SMTOps.h"
+#include "mlir/Dialect/SMT/IR/SMTTypes.h"
+
+using namespace mlir;
+using namespace smt;
+
+void SMTDialect::initialize() {
+ registerAttributes();
+ registerTypes();
+ addOperations<
+#define GET_OP_LIST
+#include "mlir/Dialect/SMT/IR/SMT.cpp.inc"
+ >();
+}
+
+Operation *SMTDialect::materializeConstant(OpBuilder &builder, Attribute value,
+ Type type, Location loc) {
+ // BitVectorType constants can materialize into smt.bv.constant
+ if (auto bvType = dyn_cast<BitVectorType>(type)) {
+ if (auto attrValue = dyn_cast<BitVectorAttr>(value)) {
+ assert(bvType == attrValue.getType() &&
+ "attribute and desired result types have to match");
+ return builder.create<BVConstantOp>(loc, attrValue);
+ }
+ }
+
+ // BoolType constants can materialize into smt.constant
+ if (auto boolType = dyn_cast<BoolType>(type)) {
+ if (auto attrValue = dyn_cast<BoolAttr>(value))
+ return builder.create<BoolConstantOp>(loc, attrValue);
+ }
+
+ return nullptr;
+}
+
+#include "mlir/Dialect/SMT/IR/SMTDialect.cpp.inc"
+#include "mlir/Dialect/SMT/IR/SMTEnums.cpp.inc"
diff --git a/mlir/lib/Dialect/SMT/IR/SMTOps.cpp b/mlir/lib/Dialect/SMT/IR/SMTOps.cpp
new file mode 100644
index 0000000000000..8977a3abc125d
--- /dev/null
+++ b/mlir/lib/Dialect/SMT/IR/SMTOps.cpp
@@ -0,0 +1,472 @@
+//===- SMTOps.cpp ---------------------------------------------------------===//
+//
+// 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
+//
+//===----------------------------------------------------------------------===//
+
+#include "mlir/Dialect/SMT/IR/SMTOps.h"
+#include "mlir/IR/Builders.h"
+#include "mlir/IR/OpImplementation.h"
+#include "llvm/ADT/APSInt.h"
+
+using namespace mlir;
+using namespace smt;
+using namespace mlir;
+
+//===----------------------------------------------------------------------===//
+// BVConstantOp
+//===----------------------------------------------------------------------===//
+
+LogicalResult BVConstantOp::inferReturnTypes(
+ mlir::MLIRContext *context, std::optional<mlir::Location> location,
+ ::mlir::ValueRange operands, ::mlir::DictionaryAttr attributes,
+ ::mlir::OpaqueProperties properties, ::mlir::RegionRange regions,
+ ::llvm::SmallVectorImpl<::mlir::Type> &inferredReturnTypes) {
+ inferredReturnTypes.push_back(
+ properties.as<Properties *>()->getValue().getType());
+ return success();
+}
+
+void BVConstantOp::getAsmResultNames(
+ function_ref<void(Value, StringRef)> setNameFn) {
+ SmallVector<char, 128> specialNameBuffer;
+ llvm::raw_svector_ostream specialName(specialNameBuffer);
+ specialName << "c" << getValue().getValue() << "_bv"
+ << getValue().getValue().getBitWidth();
+ setNameFn(getResult(), specialName.str());
+}
+
+OpFoldResult BVConstantOp::fold(FoldAdaptor adaptor) {
+ assert(adaptor.getOperands().empty() && "constant has no operands");
+ return getValueAttr();
+}
+
+//===----------------------------------------------------------------------===//
+// DeclareFunOp
+//===----------------------------------------------------------------------===//
+
+void DeclareFunOp::getAsmResultNames(
+ function_ref<void(Value, StringRef)> setNameFn) {
+ setNameFn(getResult(), getNamePrefix().has_value() ? *getNamePrefix() : "");
+}
+
+//===----------------------------------------------------------------------===//
+// SolverOp
+//===----------------------------------------------------------------------===//
+
+LogicalResult SolverOp::verifyRegions() {
+ if (getBody()->getTerminator()->getOperands().getTypes() != getResultTypes())
+ return emitOpError() << "types of yielded values must match return values";
+ if (getBody()->getArgumentTypes() != getInputs().getTypes())
+ return emitOpError()
+ << "block argument types must match the types of the 'inputs'";
+
+ return success();
+}
+
+//===----------------------------------------------------------------------===//
+// CheckOp
+//===----------------------------------------------------------------------===//
+
+LogicalResult CheckOp::verifyRegions() {
+ if (getSatRegion().front().getTerminator()->getOperands().getTypes() !=
+ getResultTypes())
+ return emitOpError() << "types of yielded values in 'sat' region must "
+ "match return values";
+ if (getUnknownRegion().front().getTerminator()->getOperands().getTypes() !=
+ getResultTypes())
+ return emitOpError() << "types of yielded values in 'unknown' region must "
+ "match return values";
+ if (getUnsatRegion().front().getTerminator()->getOperands().getTypes() !=
+ getResultTypes())
+ return emitOpError() << "types of yielded values in 'unsat' region must "
+ "match return values";
+
+ return success();
+}
+
+//===----------------------------------------------------------------------===//
+// EqOp
+//===----------------------------------------------------------------------===//
+
+static LogicalResult
+parseSameOperandTypeVariadicToBoolOp(OpAsmParser &parser,
+ OperationState &result) {
+ SmallVector<OpAsmParser::UnresolvedOperand, 4> inputs;
+ SMLoc loc = parser.getCurrentLocation();
+ Type type;
+
+ if (parser.parseOperandList(inputs) ||
+ parser.parseOptionalAttrDict(result.attributes) || parser.parseColon() ||
+ parser.parseType(type))
+ return failure();
+
+ result.addTypes(BoolType::get(parser.getContext()));
+ if (parser.resolveOperands(inputs, SmallVector<Type>(inputs.size(), type),
+ loc, result.operands))
+ return failure();
+
+ return success();
+}
+
+ParseResult EqOp::parse(OpAsmParser &parser, OperationState &result) {
+ return parseSameOperandTypeVariadicToBoolOp(parser, result);
+}
+
+void EqOp::print(OpAsmPrinter &printer) {
+ printer << ' ' << getInputs();
+ printer.printOptionalAttrDict(getOperation()->getAttrs());
+ printer << " : " << getInputs().front().getType();
+}
+
+LogicalResult EqOp::verify() {
+ if (getInputs().size() < 2)
+ return emitOpError() << "'inputs' must have at least size 2, but got "
+ << getInputs().size();
+
+ return success();
+}
+
+//===----------------------------------------------------------------------===//
+// DistinctOp
+//===----------------------------------------------------------------------===//
+
+ParseResult DistinctOp::parse(OpAsmParser &parser, OperationState &result) {
+ return parseSameOperandTypeVariadicToBoolOp(parser, result);
+}
+
+void DistinctOp::print(OpAsmPrinter &printer) {
+ printer << ' ' << getInputs();
+ printer.printOptionalAttrDict(getOperation()->getAttrs());
+ printer << " : " << getInputs().front().getType();
+}
+
+LogicalResult DistinctOp::verify() {
+ if (getInputs().size() < 2)
+ return emitOpError() << "'inputs' must have at least size 2, but got "
+ << getInputs().size();
+
+ return success();
+}
+
+//===----------------------------------------------------------------------===//
+// ExtractOp
+//===----------------------------------------------------------------------===//
+
+LogicalResult ExtractOp::verify() {
+ unsigned rangeWidth = getType().getWidth();
+ unsigned inputWidth = cast<BitVectorType>(getInput().getType()).getWidth();
+ if (getLowBit() + rangeWidth > inputWidth)
+ return emitOpError("range to be extracted is too big, expected range "
+ "starting at index ")
+ << getLowBit() << " of length " << rangeWidth
+ << " requires input width of at least " << (getLowBit() + rangeWidth)
+ << ", but the input width is only " << inputWidth;
+ return success();
+}
+
+//===----------------------------------------------------------------------===//
+// ConcatOp
+//===----------------------------------------------------------------------===//
+
+LogicalResult ConcatOp::inferReturnTypes(
+ MLIRContext *context, std::optional<Location> location, ValueRange operands,
+ DictionaryAttr attributes, OpaqueProperties properties, RegionRange regions,
+ SmallVectorImpl<Type> &inferredReturnTypes) {
+ inferredReturnTypes.push_back(BitVectorType::get(
+ context, cast<BitVectorType>(operands[0].getType()).getWidth() +
+ cast<BitVectorType>(operands[1].getType()).getWidth()));
+ return success();
+}
+
+//===----------------------------------------------------------------------===//
+// RepeatOp
+//===----------------------------------------------------------------------===//
+
+LogicalResult RepeatOp::verify() {
+ unsigned inputWidth = cast<BitVectorType>(getInput().getType()).getWidth();
+ unsigned resultWidth = getType().getWidth();
+ if (resultWidth % inputWidth != 0)
+ return emitOpError() << "result bit-vector width must be a multiple of the "
+ "input bit-vector width";
+
+ return success();
+}
+
+unsigned RepeatOp::getCount() {
+ unsigned inputWidth = cast<BitVectorType>(getInput().getType()).getWidth();
+ unsigned resultWidth = getType().getWidth();
+ return resultWidth / inputWidth;
+}
+
+void RepeatOp::build(OpBuilder &builder, OperationState &state, unsigned count,
+ Value input) {
+ unsigned inputWidth = cast<BitVectorType>(input.getType()).getWidth();
+ Type resultTy = BitVectorType::get(builder.getContext(), inputWidth * count);
+ build(builder, state, resultTy, input);
+}
+
+ParseResult RepeatOp::parse(OpAsmParser &parser, OperationState &result) {
+ OpAsmParser::UnresolvedOperand input;
+ Type inputType;
+ llvm::SMLoc countLoc = parser.getCurrentLocation();
+
+ APInt count;
+ if (parser.parseInteger(count) || parser.parseKeyword("times"))
+ return failure();
+
+ if (count.isNonPositive())
+ return parser.emitError(countLoc) << "integer must be positive";
+
+ llvm::SMLoc inputLoc = parser.getCurrentLocation();
+ if (parser.parseOperand(input) ||
+ parser.parseOptionalAttrDict(result.attributes) || parser.parseColon() ||
+ parser.parseType(inputType))
+ return failure();
+
+ if (parser.resolveOperand(input, inputType, result.operands))
+ return failure();
+
+ auto bvInputTy = dyn_cast<BitVectorType>(inputType);
+ if (!bvInputTy)
+ return parser.emitError(inputLoc) << "input must have bit-vector type";
+
+ // Make sure no assertions can trigger and no silent overflows can happen
+ // Bit-width is stored as 'int64_t' parameter in 'BitVectorType'
+ const unsigned maxBw = 63;
+ if (count.getActiveBits() > maxBw)
+ return parser.emitError(countLoc)
+ << "integer must fit into " << maxBw << " bits";
+
+ // Store multiplication in an APInt twice the size to not have any overflow
+ // and check if it can be truncated to 'maxBw' bits without cutting of
+ // important bits.
+ APInt resultBw = bvInputTy.getWidth() * count.zext(2 * maxBw);
+ if (resultBw.getActiveBits() > maxBw)
+ return parser.emitError(countLoc)
+ << "result bit-width (provided integer times bit-width of the input "
+ "type) must fit into "
+ << maxBw << " bits";
+
+ Type resultTy =
+ BitVectorType::get(parser.getContext(), resultBw.getZExtValue());
+ result.addTypes(resultTy);
+ return success();
+}
+
+void RepeatOp::print(OpAsmPrinter &printer) {
+ printer << " " << getCount() << " times " << getInput();
+ printer.printOptionalAttrDict((*this)->getAttrs());
+ printer << " : " << getInput().getType();
+}
+
+//===----------------------------------------------------------------------===//
+// BoolConstantOp
+//===----------------------------------------------------------------------===//
+
+void BoolConstantOp::getAsmResultNames(
+ function_ref<void(Value, StringRef)> setNameFn) {
+ setNameFn(getResult(), getValue() ? "true" : "false");
+}
+
+OpFoldResult BoolConstantOp::fold(FoldAdaptor adaptor) {
+ assert(adaptor.getOperands().empty() && "constant has no operands");
+ return getValueAttr();
+}
+
+//===----------------------------------------------------------------------===//
+// IntConstantOp
+//===----------------------------------------------------------------------===//
+
+void IntConstantOp::getAsmResultNames(
+ function_ref<void(Value, StringRef)> setNameFn) {
+ SmallVector<char, 32> specialNameBuffer;
+ llvm::raw_svector_ostream specialName(specialNameBuffer);
+ specialName << "c" << getValue();
+ setNameFn(getResult(), specialName.str());
+}
+
+OpFoldResult IntConstantOp::fold(FoldAdaptor adaptor) {
+ assert(adaptor.getOperands().empty() && "constant has no operands");
+ return getValueAttr();
+}
+
+void IntConstantOp::print(OpAsmPrinter &p) {
+ p << " " << getValue();
+ p.printOptionalAttrDict((*this)->getAttrs(), /*elidedAttrs=*/{"value"});
+}
+
+ParseResult IntConstantOp::parse(OpAsmParser &parser, OperationState &result) {
+ APInt value;
+ if (parser.parseInteger(value))
+ return failure();
+
+ result.getOrAddProperties<Properties>().setValue(
+ IntegerAttr::get(parser.getContext(), APSInt(value)));
+
+ if (parser.parseOptionalAttrDict(result.attributes))
+ return failure();
+
+ result.addTypes(smt::IntType::get(parser.getContext()));
+ return success();
+}
+
+//===----------------------------------------------------------------------===//
+// ForallOp
+//===----------------------------------------------------------------------===//
+
+template <typename QuantifierOp>
+static LogicalResult verifyQuantifierRegions(QuantifierOp op) {
+ if (op.getBoundVarNames() &&
+ op.getBody().getNumArguments() != op.getBoundVarNames()->size())
+ return op.emitOpError(
+ "number of bound variable names must match number of block arguments");
+ if (!llvm::all_of(op.getBody().getArgumentTypes(), isAnyNonFuncSMTValueType))
+ return op.emitOpError()
+ << "bound variables must by any non-function SMT value";
+
+ if (op.getBody().front().getTerminator()->getNumOperands() != 1)
+ return op.emitOpError("must have exactly one yielded value");
+ if (!isa<BoolType>(
+ op.getBody().front().getTerminator()->getOperand(0).getType()))
+ return op.emitOpError("yielded value must be of '!smt.bool' type");
+
+ for (auto regionWithIndex : llvm::enumerate(op.getPatterns())) {
+ unsigned i = regionWithIndex.index();
+ Region ®ion = regionWithIndex.value();
+
+ if (op.getBody().getArgumentTypes() != region.getArgumentTypes())
+ return op.emitOpError()
+ << "block argument number and types of the 'body' "
+ "and 'patterns' region #"
+ << i << " must match";
+ if (region.front().getTerminator()->getNumOperands() < 1)
+ return op.emitOpError() << "'patterns' region #" << i
+ << " must have at least one yielded value";
+
+ // All operations in the 'patterns' region must be SMT operations.
+ auto result = region.walk([&](Operation *childOp) {
+ if (!isa<SMTDialect>(childOp->getDialect())) {
+ auto diag = op.emitOpError()
+ << "the 'patterns' region #" << i
+ << " may only contain SMT dialect operations";
+ diag.attachNote(childOp->getLoc()) << "first non-SMT operation here";
+ return WalkResult::interrupt();
+ }
+
+ // There may be no quantifier (or other variable binding) operations in
+ // the 'patterns' region.
+ if (isa<ForallOp, ExistsOp>(childOp)) {
+ auto diag = op.emitOpError() << "the 'patterns' region #" << i
+ << " must not contain "
+ "any variable binding operations";
+ diag.attachNote(childOp->getLoc()) << "first violating operation here";
+ return WalkResult::interrupt();
+ }
+
+ return WalkResult::advance();
+ });
+ if (result.wasInterrupted())
+ return failure();
+ }
+
+ return success();
+}
+
+template <typename Properties>
+static void buildQuantifier(
+ OpBuilder &odsBuilder, OperationState &odsState, TypeRange boundVarTypes,
+ function_ref<Value(OpBuilder &, Location, ValueRange)> bodyBuilder,
+ std::optional<ArrayRef<StringRef>> boundVarNames,
+ function_ref<ValueRange(OpBuilder &, Location, ValueRange)> patternBuilder,
+ uint32_t weight, bool noPattern) {
+ odsState.addTypes(BoolType::get(odsBuilder.getContext()));
+ if (weight != 0)
+ odsState.getOrAddProperties<Properties>().weight =
+ odsBuilder.getIntegerAttr(odsBuilder.getIntegerType(32), weight);
+ if (noPattern)
+ odsState.getOrAddProperties<Properties>().noPattern =
+ odsBuilder.getUnitAttr();
+ if (boundVarNames.has_value()) {
+ SmallVector<Attribute> boundVarNamesList;
+ for (StringRef str : *boundVarNames)
+ boundVarNamesList.emplace_back(odsBuilder.getStringAttr(str));
+ odsState.getOrAddProperties<Properties>().boundVarNames =
+ odsBuilder.getArrayAttr(boundVarNamesList);
+ }
+ {
+ OpBuilder::InsertionGuard guard(odsBuilder);
+ Region *region = odsState.addRegion();
+ Block *block = odsBuilder.createBlock(region);
+ block->addArguments(
+ boundVarTypes,
+ SmallVector<Location>(boundVarTypes.size(), odsState.location));
+ Value returnVal =
+ bodyBuilder(odsBuilder, odsState.location, block->getArguments());
+ odsBuilder.create<smt::YieldOp>(odsState.location, returnVal);
+ }
+ if (patternBuilder) {
+ Region *region = odsState.addRegion();
+ OpBuilder::InsertionGuard guard(odsBuilder);
+ Block *block = odsBuilder.createBlock(region);
+ block->addArguments(
+ boundVarTypes,
+ SmallVector<Location>(boundVarTypes.size(), odsState.location));
+ ValueRange returnVals =
+ patternBuilder(odsBuilder, odsState.location, block->getArguments());
+ odsBuilder.create<smt::YieldOp>(odsState.location, returnVals);
+ }
+}
+
+LogicalResult ForallOp::verify() {
+ if (!getPatterns().empty() && getNoPattern())
+ return emitOpError() << "patterns and the no_pattern attribute must not be "
+ "specified at the same time";
+
+ return success();
+}
+
+LogicalResult ForallOp::verifyRegions() {
+ return verifyQuantifierRegions(*this);
+}
+
+void ForallOp::build(
+ OpBuilder &odsBuilder, OperationState &odsState, TypeRange boundVarTypes,
+ function_ref<Value(OpBuilder &, Location, ValueRange)> bodyBuilder,
+ std::optional<ArrayRef<StringRef>> boundVarNames,
+ function_ref<ValueRange(OpBuilder &, Location, ValueRange)> patternBuilder,
+ uint32_t weight, bool noPattern) {
+ buildQuantifier<Properties>(odsBuilder, odsState, boundVarTypes, bodyBuilder,
+ boundVarNames, patternBuilder, weight, noPattern);
+}
+
+//===----------------------------------------------------------------------===//
+// ExistsOp
+//===----------------------------------------------------------------------===//
+
+LogicalResult ExistsOp::verify() {
+ if (!getPatterns().empty() && getNoPattern())
+ return emitOpError() << "patterns and the no_pattern attribute must not be "
+ "specified at the same time";
+
+ return success();
+}
+
+LogicalResult ExistsOp::verifyRegions() {
+ return verifyQuantifierRegions(*this);
+}
+
+void ExistsOp::build(
+ OpBuilder &odsBuilder, OperationState &odsState, TypeRange boundVarTypes,
+ function_ref<Value(OpBuilder &, Location, ValueRange)> bodyBuilder,
+ std::optional<ArrayRef<StringRef>> boundVarNames,
+ function_ref<ValueRange(OpBuilder &, Location, ValueRange)> patternBuilder,
+ uint32_t weight, bool noPattern) {
+ buildQuantifier<Properties>(odsBuilder, odsState, boundVarTypes, bodyBuilder,
+ boundVarNames, patternBuilder, weight, noPattern);
+}
+
+#define GET_OP_CLASSES
+#include "mlir/Dialect/SMT/IR/SMT.cpp.inc"
diff --git a/mlir/lib/Dialect/SMT/IR/SMTTypes.cpp b/mlir/lib/Dialect/SMT/IR/SMTTypes.cpp
new file mode 100644
index 0000000000000..6188719bb1ab5
--- /dev/null
+++ b/mlir/lib/Dialect/SMT/IR/SMTTypes.cpp
@@ -0,0 +1,92 @@
+//===- SMTTypes.cpp -------------------------------------------------------===//
+//
+// 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
+//
+//===----------------------------------------------------------------------===//
+
+#include "mlir/Dialect/SMT/IR/SMTTypes.h"
+#include "mlir/Dialect/SMT/IR/SMTDialect.h"
+#include "mlir/IR/Builders.h"
+#include "mlir/IR/DialectImplementation.h"
+#include "llvm/ADT/TypeSwitch.h"
+
+using namespace mlir;
+using namespace smt;
+using namespace mlir;
+
+#define GET_TYPEDEF_CLASSES
+#include "mlir/Dialect/SMT/IR/SMTTypes.cpp.inc"
+
+void SMTDialect::registerTypes() {
+ addTypes<
+#define GET_TYPEDEF_LIST
+#include "mlir/Dialect/SMT/IR/SMTTypes.cpp.inc"
+ >();
+}
+
+bool smt::isAnyNonFuncSMTValueType(Type type) {
+ return isAnySMTValueType(type) && !isa<SMTFuncType>(type);
+}
+
+bool smt::isAnySMTValueType(Type type) {
+ return isa<BoolType, BitVectorType, ArrayType, IntType, SortType,
+ SMTFuncType>(type);
+}
+
+//===----------------------------------------------------------------------===//
+// BitVectorType
+//===----------------------------------------------------------------------===//
+
+LogicalResult
+BitVectorType::verify(function_ref<InFlightDiagnostic()> emitError,
+ int64_t width) {
+ if (width <= 0U)
+ return emitError() << "bit-vector must have at least a width of one";
+ return success();
+}
+
+//===----------------------------------------------------------------------===//
+// ArrayType
+//===----------------------------------------------------------------------===//
+
+LogicalResult ArrayType::verify(function_ref<InFlightDiagnostic()> emitError,
+ Type domainType, Type rangeType) {
+ if (!isAnySMTValueType(domainType))
+ return emitError() << "domain must be any SMT value type";
+ if (!isAnySMTValueType(rangeType))
+ return emitError() << "range must be any SMT value type";
+
+ return success();
+}
+
+//===----------------------------------------------------------------------===//
+// SMTFuncType
+//===----------------------------------------------------------------------===//
+
+LogicalResult SMTFuncType::verify(function_ref<InFlightDiagnostic()> emitError,
+ ArrayRef<Type> domainTypes, Type rangeType) {
+ if (domainTypes.empty())
+ return emitError() << "domain must not be empty";
+ if (!llvm::all_of(domainTypes, isAnyNonFuncSMTValueType))
+ return emitError() << "domain types must be any non-function SMT type";
+ if (!isAnyNonFuncSMTValueType(rangeType))
+ return emitError() << "range type must be any non-function SMT type";
+
+ return success();
+}
+
+//===----------------------------------------------------------------------===//
+// SortType
+//===----------------------------------------------------------------------===//
+
+LogicalResult SortType::verify(function_ref<InFlightDiagnostic()> emitError,
+ StringAttr identifier,
+ ArrayRef<Type> sortParams) {
+ if (!llvm::all_of(sortParams, isAnyNonFuncSMTValueType))
+ return emitError()
+ << "sort parameter types must be any non-function SMT type";
+
+ return success();
+}
diff --git a/mlir/test/Dialect/SMT/array-errors.mlir b/mlir/test/Dialect/SMT/array-errors.mlir
new file mode 100644
index 0000000000000..4e90948eed848
--- /dev/null
+++ b/mlir/test/Dialect/SMT/array-errors.mlir
@@ -0,0 +1,13 @@
+// RUN: mlir-opt %s --split-input-file --verify-diagnostics
+
+// expected-error @below {{domain must be any SMT value type}}
+func.func @array_domain_no_smt_type(%arg0: !smt.array<[i32 -> !smt.bool]>) {
+ return
+}
+
+// -----
+
+// expected-error @below {{range must be any SMT value type}}
+func.func @array_range_no_smt_type(%arg0: !smt.array<[!smt.bool -> i32]>) {
+ return
+}
diff --git a/mlir/test/Dialect/SMT/array.mlir b/mlir/test/Dialect/SMT/array.mlir
new file mode 100644
index 0000000000000..89cb45c5e878a
--- /dev/null
+++ b/mlir/test/Dialect/SMT/array.mlir
@@ -0,0 +1,14 @@
+// RUN: mlir-opt %s | mlir-opt | FileCheck %s
+
+// CHECK-LABEL: func @arrayOperations
+// CHECK-SAME: ([[A0:%.+]]: !smt.bool)
+func.func @arrayOperations(%arg0: !smt.bool) {
+ // CHECK-NEXT: [[V0:%.+]] = smt.array.broadcast [[A0]] {smt.some_attr} : !smt.array<[!smt.bool -> !smt.bool]>
+ %0 = smt.array.broadcast %arg0 {smt.some_attr} : !smt.array<[!smt.bool -> !smt.bool]>
+ // CHECK-NEXT: [[V1:%.+]] = smt.array.select [[V0]][[[A0]]] {smt.some_attr} : !smt.array<[!smt.bool -> !smt.bool]>
+ %1 = smt.array.select %0[%arg0] {smt.some_attr} : !smt.array<[!smt.bool -> !smt.bool]>
+ // CHECK-NEXT: [[V2:%.+]] = smt.array.store [[V0]][[[A0]]], [[A0]] {smt.some_attr} : !smt.array<[!smt.bool -> !smt.bool]>
+ %2 = smt.array.store %0[%arg0], %arg0 {smt.some_attr} : !smt.array<[!smt.bool -> !smt.bool]>
+
+ return
+}
diff --git a/mlir/test/Dialect/SMT/basic.mlir b/mlir/test/Dialect/SMT/basic.mlir
new file mode 100644
index 0000000000000..a4975d66e9769
--- /dev/null
+++ b/mlir/test/Dialect/SMT/basic.mlir
@@ -0,0 +1,200 @@
+// RUN: mlir-opt %s | mlir-opt | FileCheck %s
+
+// CHECK-LABEL: func @types
+// CHECK-SAME: (%{{.*}}: !smt.bool, %{{.*}}: !smt.bv<32>, %{{.*}}: !smt.int, %{{.*}}: !smt.sort<"uninterpreted_sort">, %{{.*}}: !smt.sort<"uninterpreted_sort"[!smt.bool, !smt.int]>, %{{.*}}: !smt.func<(!smt.bool, !smt.bool) !smt.bool>)
+func.func @types(%arg0: !smt.bool, %arg1: !smt.bv<32>, %arg2: !smt.int, %arg3: !smt.sort<"uninterpreted_sort">, %arg4: !smt.sort<"uninterpreted_sort"[!smt.bool, !smt.int]>, %arg5: !smt.func<(!smt.bool, !smt.bool) !smt.bool>) {
+ return
+}
+
+func.func @core(%in: i8) {
+ // CHECK: %a = smt.declare_fun "a" {smt.some_attr} : !smt.bool
+ %a = smt.declare_fun "a" {smt.some_attr} : !smt.bool
+ // CHECK: smt.declare_fun {smt.some_attr} : !smt.bv<32>
+ %b = smt.declare_fun {smt.some_attr} : !smt.bv<32>
+ // CHECK: smt.declare_fun {smt.some_attr} : !smt.int
+ %c = smt.declare_fun {smt.some_attr} : !smt.int
+ // CHECK: smt.declare_fun {smt.some_attr} : !smt.sort<"uninterpreted_sort">
+ %d = smt.declare_fun {smt.some_attr} : !smt.sort<"uninterpreted_sort">
+ // CHECK: smt.declare_fun {smt.some_attr} : !smt.func<(!smt.int, !smt.bool) !smt.bool>
+ %e = smt.declare_fun {smt.some_attr} : !smt.func<(!smt.int, !smt.bool) !smt.bool>
+
+ // CHECK: smt.constant true {smt.some_attr}
+ %true = smt.constant true {smt.some_attr}
+ // CHECK: smt.constant false {smt.some_attr}
+ %false = smt.constant false {smt.some_attr}
+
+ // CHECK: smt.assert %a {smt.some_attr}
+ smt.assert %a {smt.some_attr}
+
+ // CHECK: smt.reset {smt.some_attr}
+ smt.reset {smt.some_attr}
+
+ // CHECK: smt.push 1 {smt.some_attr}
+ smt.push 1 {smt.some_attr}
+
+ // CHECK: smt.pop 1 {smt.some_attr}
+ smt.pop 1 {smt.some_attr}
+
+ // CHECK: %{{.*}} = smt.solver(%{{.*}}) {smt.some_attr} : (i8) -> (i8, i32) {
+ // CHECK: ^bb0(%{{.*}}: i8)
+ // CHECK: %{{.*}} = smt.check {smt.some_attr} sat {
+ // CHECK: smt.yield %{{.*}} : i32
+ // CHECK: } unknown {
+ // CHECK: smt.yield %{{.*}} : i32
+ // CHECK: } unsat {
+ // CHECK: smt.yield %{{.*}} : i32
+ // CHECK: } -> i32
+ // CHECK: smt.yield %{{.*}}, %{{.*}} : i8, i32
+ // CHECK: }
+ %0:2 = smt.solver(%in) {smt.some_attr} : (i8) -> (i8, i32) {
+ ^bb0(%arg0: i8):
+ %1 = smt.check {smt.some_attr} sat {
+ %c1_i32 = arith.constant 1 : i32
+ smt.yield %c1_i32 : i32
+ } unknown {
+ %c0_i32 = arith.constant 0 : i32
+ smt.yield %c0_i32 : i32
+ } unsat {
+ %c-1_i32 = arith.constant -1 : i32
+ smt.yield %c-1_i32 : i32
+ } -> i32
+ smt.yield %arg0, %1 : i8, i32
+ }
+
+ // CHECK: smt.solver() : () -> () {
+ // CHECK-NEXT: }
+ smt.solver() : () -> () { }
+
+ // CHECK: smt.solver() : () -> () {
+ // CHECK-NEXT: smt.set_logic "AUFLIA"
+ // CHECK-NEXT: }
+ smt.solver() : () -> () {
+ smt.set_logic "AUFLIA"
+ }
+
+ // CHECK: smt.check sat {
+ // CHECK-NEXT: } unknown {
+ // CHECK-NEXT: } unsat {
+ // CHECK-NEXT: }
+ smt.check sat { } unknown { } unsat { }
+
+ // CHECK: %{{.*}} = smt.eq %{{.*}}, %{{.*}} {smt.some_attr} : !smt.bv<32>
+ %1 = smt.eq %b, %b {smt.some_attr} : !smt.bv<32>
+ // CHECK: %{{.*}} = smt.distinct %{{.*}}, %{{.*}} {smt.some_attr} : !smt.bv<32>
+ %2 = smt.distinct %b, %b {smt.some_attr} : !smt.bv<32>
+
+ // CHECK: %{{.*}} = smt.eq %{{.*}}, %{{.*}}, %{{.*}} : !smt.bool
+ %3 = smt.eq %a, %a, %a : !smt.bool
+ // CHECK: %{{.*}} = smt.distinct %{{.*}}, %{{.*}}, %{{.*}} : !smt.bool
+ %4 = smt.distinct %a, %a, %a : !smt.bool
+
+ // CHECK: %{{.*}} = smt.ite %{{.*}}, %{{.*}}, %{{.*}} {smt.some_attr} : !smt.bv<32>
+ %5 = smt.ite %a, %b, %b {smt.some_attr} : !smt.bv<32>
+
+ // CHECK: %{{.*}} = smt.not %{{.*}} {smt.some_attr}
+ %6 = smt.not %a {smt.some_attr}
+ // CHECK: %{{.*}} = smt.and %{{.*}}, %{{.*}}, %{{.*}} {smt.some_attr}
+ %7 = smt.and %a, %a, %a {smt.some_attr}
+ // CHECK: %{{.*}} = smt.or %{{.*}}, %{{.*}}, %{{.*}} {smt.some_attr}
+ %8 = smt.or %a, %a, %a {smt.some_attr}
+ // CHECK: %{{.*}} = smt.xor %{{.*}}, %{{.*}}, %{{.*}} {smt.some_attr}
+ %9 = smt.xor %a, %a, %a {smt.some_attr}
+ // CHECK: %{{.*}} = smt.implies %{{.*}}, %{{.*}} {smt.some_attr}
+ %10 = smt.implies %a, %a {smt.some_attr}
+
+ // CHECK: smt.apply_func %{{.*}}(%{{.*}}, %{{.*}}) {smt.some_attr} : !smt.func<(!smt.int, !smt.bool) !smt.bool>
+ %11 = smt.apply_func %e(%c, %a) {smt.some_attr} : !smt.func<(!smt.int, !smt.bool) !smt.bool>
+
+ return
+}
+
+// CHECK-LABEL: func @quantifiers
+func.func @quantifiers() {
+ // CHECK-NEXT: smt.forall ["a", "b"] weight 2 attributes {smt.some_attr} {
+ // CHECK-NEXT: ^bb0({{.*}}: !smt.bool, {{.*}}: !smt.bool):
+ // CHECK-NEXT: smt.eq
+ // CHECK-NEXT: smt.yield %{{.*}}
+ // CHECK-NEXT: } patterns {
+ // CHECK-NEXT: ^bb0(%{{.*}}: !smt.bool, %{{.*}}: !smt.bool):
+ // CHECK-NEXT: smt.yield %{{.*}}
+ // CHECK-NEXT: }, {
+ // CHECK-NEXT: ^bb0(%{{.*}}: !smt.bool):
+ // CHECK-NEXT: smt.yield %{{.*}}
+ // CHECK-NEXT: }
+ %0 = smt.forall ["a", "b"] weight 2 attributes {smt.some_attr} {
+ ^bb0(%arg2: !smt.bool, %arg3: !smt.bool):
+ %1 = smt.eq %arg2, %arg3 : !smt.bool
+ smt.yield %1 : !smt.bool
+ } patterns {
+ ^bb0(%arg2: !smt.bool, %arg3: !smt.bool):
+ smt.yield %arg2, %arg3 : !smt.bool, !smt.bool
+ }, {
+ ^bb0(%arg2: !smt.bool, %arg3: !smt.bool):
+ smt.yield %arg2, %arg3 : !smt.bool, !smt.bool
+ }
+
+ // CHECK-NEXT: smt.forall ["a", "b"] no_pattern attributes {smt.some_attr} {
+ // CHECK-NEXT: ^bb0({{.*}}: !smt.bool, {{.*}}: !smt.bool):
+ // CHECK-NEXT: smt.eq
+ // CHECK-NEXT: smt.yield %{{.*}}
+ // CHECK-NEXT: }
+ %1 = smt.forall ["a", "b"] no_pattern attributes {smt.some_attr} {
+ ^bb0(%arg2: !smt.bool, %arg3: !smt.bool):
+ %2 = smt.eq %arg2, %arg3 : !smt.bool
+ smt.yield %2 : !smt.bool
+ }
+
+ // CHECK-NEXT: smt.forall {
+ // CHECK-NEXT: smt.constant
+ // CHECK-NEXT: smt.yield %{{.*}}
+ // CHECK-NEXT: }
+ %2 = smt.forall {
+ %3 = smt.constant true
+ smt.yield %3 : !smt.bool
+ }
+
+ // CHECK-NEXT: smt.exists ["a", "b"] weight 2 attributes {smt.some_attr} {
+ // CHECK-NEXT: ^bb0({{.*}}: !smt.bool, {{.*}}: !smt.bool):
+ // CHECK-NEXT: smt.eq
+ // CHECK-NEXT: smt.yield %{{.*}}
+ // CHECK-NEXT: } patterns {
+ // CHECK-NEXT: ^bb0(%{{.*}}: !smt.bool, %{{.*}}: !smt.bool):
+ // CHECK-NEXT: smt.yield %{{.*}}
+ // CHECK-NEXT: }, {
+ // CHECK-NEXT: ^bb0(%{{.*}}: !smt.bool):
+ // CHECK-NEXT: smt.yield %{{.*}}
+ // CHECK-NEXT: }
+ %3 = smt.exists ["a", "b"] weight 2 attributes {smt.some_attr} {
+ ^bb0(%arg2: !smt.bool, %arg3: !smt.bool):
+ %4 = smt.eq %arg2, %arg3 : !smt.bool
+ smt.yield %4 : !smt.bool {smt.some_attr}
+ } patterns {
+ ^bb0(%arg2: !smt.bool, %arg3: !smt.bool):
+ smt.yield %arg2, %arg3 : !smt.bool, !smt.bool
+ }, {
+ ^bb0(%arg2: !smt.bool, %arg3: !smt.bool):
+ smt.yield %arg2, %arg3 : !smt.bool, !smt.bool
+ }
+
+ // CHECK-NEXT: smt.exists no_pattern attributes {smt.some_attr} {
+ // CHECK-NEXT: ^bb0({{.*}}: !smt.bool, {{.*}}: !smt.bool):
+ // CHECK-NEXT: smt.eq
+ // CHECK-NEXT: smt.yield %{{.*}}
+ // CHECK-NEXT: }
+ %4 = smt.exists no_pattern attributes {smt.some_attr} {
+ ^bb0(%arg2: !smt.bool, %arg3: !smt.bool):
+ %5 = smt.eq %arg2, %arg3 : !smt.bool
+ smt.yield %5 : !smt.bool {smt.some_attr}
+ }
+
+ // CHECK-NEXT: smt.exists [] {
+ // CHECK-NEXT: smt.constant
+ // CHECK-NEXT: smt.yield %{{.*}}
+ // CHECK-NEXT: }
+ %5 = smt.exists [] {
+ %6 = smt.constant true
+ smt.yield %6 : !smt.bool
+ }
+
+ return
+}
diff --git a/mlir/test/Dialect/SMT/bitvector-errors.mlir b/mlir/test/Dialect/SMT/bitvector-errors.mlir
new file mode 100644
index 0000000000000..58226f4d55f62
--- /dev/null
+++ b/mlir/test/Dialect/SMT/bitvector-errors.mlir
@@ -0,0 +1,112 @@
+// RUN: mlir-opt %s --split-input-file --verify-diagnostics
+
+// expected-error @below {{bit-vector must have at least a width of one}}
+func.func @at_least_size_one(%arg0: !smt.bv<0>) {
+ return
+}
+
+// -----
+
+// expected-error @below {{bit-vector must have at least a width of one}}
+func.func @positive_width(%arg0: !smt.bv<-1>) {
+ return
+}
+
+// -----
+
+func.func @attr_type_and_return_type_match() {
+ // expected-error @below {{inferred type(s) '!smt.bv<1>' are incompatible with return type(s) of operation '!smt.bv<32>'}}
+ // expected-error @below {{failed to infer returned types}}
+ %c0_bv32 = "smt.bv.constant"() <{value = #smt.bv<0> : !smt.bv<1>}> : () -> !smt.bv<32>
+ return
+}
+
+// -----
+
+func.func @invalid_bitvector_attr() {
+ // expected-error @below {{explicit bit-vector type required}}
+ smt.bv.constant #smt.bv<5>
+}
+
+// -----
+
+func.func @invalid_bitvector_attr() {
+ // expected-error @below {{integer value out of range for given bit-vector type}}
+ smt.bv.constant #smt.bv<32> : !smt.bv<2>
+}
+
+// -----
+
+func.func @invalid_bitvector_attr() {
+ // expected-error @below {{integer value out of range for given bit-vector type}}
+ smt.bv.constant #smt.bv<-4> : !smt.bv<2>
+}
+
+// -----
+
+func.func @extraction(%arg0: !smt.bv<32>) {
+ // expected-error @below {{range to be extracted is too big, expected range starting at index 20 of length 16 requires input width of at least 36, but the input width is only 32}}
+ smt.bv.extract %arg0 from 20 : (!smt.bv<32>) -> !smt.bv<16>
+ return
+}
+
+// -----
+
+func.func @concat(%arg0: !smt.bv<32>) {
+ // expected-error @below {{inferred type(s) '!smt.bv<64>' are incompatible with return type(s) of operation '!smt.bv<33>'}}
+ // expected-error @below {{failed to infer returned types}}
+ "smt.bv.concat"(%arg0, %arg0) {} : (!smt.bv<32>, !smt.bv<32>) -> !smt.bv<33>
+ return
+}
+
+// -----
+
+func.func @repeat_result_type_no_multiple_of_input_type(%arg0: !smt.bv<32>) {
+ // expected-error @below {{result bit-vector width must be a multiple of the input bit-vector width}}
+ "smt.bv.repeat"(%arg0) : (!smt.bv<32>) -> !smt.bv<65>
+ return
+}
+
+// -----
+
+func.func @repeat_negative_count(%arg0: !smt.bv<32>) {
+ // expected-error @below {{integer must be positive}}
+ smt.bv.repeat -2 times %arg0 : !smt.bv<32>
+ return
+}
+
+// -----
+
+// The parser has to extract the bit-width of the input and thus we need to
+// test that this is handled correctly in the parser, we cannot just rely on the
+// verifier.
+func.func @repeat_wrong_input_type(%arg0: !smt.bool) {
+ // expected-error @below {{input must have bit-vector type}}
+ smt.bv.repeat 2 times %arg0 : !smt.bool
+ return
+}
+
+// -----
+
+func.func @repeat_count_too_large(%arg0: !smt.bv<32>) {
+ // expected-error @below {{integer must fit into 63 bits}}
+ smt.bv.repeat 18446744073709551617 times %arg0 : !smt.bv<32>
+ return
+}
+
+// -----
+
+func.func @repeat_result_type_bitwidth_too_large(%arg0: !smt.bv<9223372036854775807>) {
+ // expected-error @below {{result bit-width (provided integer times bit-width of the input type) must fit into 63 bits}}
+ smt.bv.repeat 2 times %arg0 : !smt.bv<9223372036854775807>
+ return
+}
+
+// -----
+
+func.func @invalid_bv2int_signedness() {
+ %c5_bv32 = smt.bv.constant #smt.bv<5> : !smt.bv<32>
+ // expected-error @below {{expected ':'}}
+ %bv2int = smt.bv2int %c5_bv32 unsigned : !smt.bv<32>
+ return
+}
diff --git a/mlir/test/Dialect/SMT/bitvectors.mlir b/mlir/test/Dialect/SMT/bitvectors.mlir
new file mode 100644
index 0000000000000..2482f55b5ed31
--- /dev/null
+++ b/mlir/test/Dialect/SMT/bitvectors.mlir
@@ -0,0 +1,81 @@
+// RUN: mlir-opt %s | mlir-opt | FileCheck %s
+
+// CHECK-LABEL: func @bitvectors
+func.func @bitvectors() {
+ // CHECK: %c5_bv32 = smt.bv.constant #smt.bv<5> : !smt.bv<32> {smt.some_attr}
+ %c5_bv32 = smt.bv.constant #smt.bv<5> : !smt.bv<32> {smt.some_attr}
+ // CHECK: %c92_bv8 = smt.bv.constant #smt.bv<92> : !smt.bv<8> {smt.some_attr}
+ %c92_bv8 = smt.bv.constant #smt.bv<0x5c> : !smt.bv<8> {smt.some_attr}
+ // CHECK: %c-1_bv8 = smt.bv.constant #smt.bv<-1> : !smt.bv<8>
+ %c-1_bv8 = smt.bv.constant #smt.bv<-1> : !smt.bv<8>
+ // CHECK: %c-1_bv1{{(_[0-9]+)?}} = smt.bv.constant #smt.bv<-1> : !smt.bv<1>
+ %c-1_bv1_neg = smt.bv.constant #smt.bv<-1> : !smt.bv<1>
+ // CHECK: %c-1_bv1{{(_[0-9]+)?}} = smt.bv.constant #smt.bv<-1> : !smt.bv<1>
+ %c-1_bv1_pos = smt.bv.constant #smt.bv<1> : !smt.bv<1>
+
+ // CHECK: [[C0:%.+]] = smt.bv.constant #smt.bv<0> : !smt.bv<32>
+ %c = smt.bv.constant #smt.bv<0> : !smt.bv<32>
+
+ // CHECK: %{{.*}} = smt.bv.neg [[C0]] {smt.some_attr} : !smt.bv<32>
+ %0 = smt.bv.neg %c {smt.some_attr} : !smt.bv<32>
+ // CHECK: %{{.*}} = smt.bv.add [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
+ %1 = smt.bv.add %c, %c {smt.some_attr} : !smt.bv<32>
+ // CHECK: %{{.*}} = smt.bv.mul [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
+ %3 = smt.bv.mul %c, %c {smt.some_attr} : !smt.bv<32>
+ // CHECK: %{{.*}} = smt.bv.urem [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
+ %4 = smt.bv.urem %c, %c {smt.some_attr} : !smt.bv<32>
+ // CHECK: %{{.*}} = smt.bv.srem [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
+ %5 = smt.bv.srem %c, %c {smt.some_attr} : !smt.bv<32>
+ // CHECK: %{{.*}} = smt.bv.smod [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
+ %7 = smt.bv.smod %c, %c {smt.some_attr} : !smt.bv<32>
+ // CHECK: %{{.*}} = smt.bv.shl [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
+ %8 = smt.bv.shl %c, %c {smt.some_attr} : !smt.bv<32>
+ // CHECK: %{{.*}} = smt.bv.lshr [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
+ %9 = smt.bv.lshr %c, %c {smt.some_attr} : !smt.bv<32>
+ // CHECK: %{{.*}} = smt.bv.ashr [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
+ %10 = smt.bv.ashr %c, %c {smt.some_attr} : !smt.bv<32>
+ // CHECK: %{{.*}} = smt.bv.udiv [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
+ %11 = smt.bv.udiv %c, %c {smt.some_attr} : !smt.bv<32>
+ // CHECK: %{{.*}} = smt.bv.sdiv [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
+ %12 = smt.bv.sdiv %c, %c {smt.some_attr} : !smt.bv<32>
+
+ // CHECK: %{{.*}} = smt.bv.not [[C0]] {smt.some_attr} : !smt.bv<32>
+ %13 = smt.bv.not %c {smt.some_attr} : !smt.bv<32>
+ // CHECK: %{{.*}} = smt.bv.and [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
+ %14 = smt.bv.and %c, %c {smt.some_attr} : !smt.bv<32>
+ // CHECK: %{{.*}} = smt.bv.or [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
+ %15 = smt.bv.or %c, %c {smt.some_attr} : !smt.bv<32>
+ // CHECK: %{{.*}} = smt.bv.xor [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
+ %16 = smt.bv.xor %c, %c {smt.some_attr} : !smt.bv<32>
+
+ // CHECK: %{{.*}} = smt.bv.cmp slt [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
+ %17 = smt.bv.cmp slt %c, %c {smt.some_attr} : !smt.bv<32>
+ // CHECK: %{{.*}} = smt.bv.cmp sle [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
+ %18 = smt.bv.cmp sle %c, %c {smt.some_attr} : !smt.bv<32>
+ // CHECK: %{{.*}} = smt.bv.cmp sgt [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
+ %19 = smt.bv.cmp sgt %c, %c {smt.some_attr} : !smt.bv<32>
+ // CHECK: %{{.*}} = smt.bv.cmp sge [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
+ %20 = smt.bv.cmp sge %c, %c {smt.some_attr} : !smt.bv<32>
+ // CHECK: %{{.*}} = smt.bv.cmp ult [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
+ %21 = smt.bv.cmp ult %c, %c {smt.some_attr} : !smt.bv<32>
+ // CHECK: %{{.*}} = smt.bv.cmp ule [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
+ %22 = smt.bv.cmp ule %c, %c {smt.some_attr} : !smt.bv<32>
+ // CHECK: %{{.*}} = smt.bv.cmp ugt [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
+ %23 = smt.bv.cmp ugt %c, %c {smt.some_attr} : !smt.bv<32>
+ // CHECK: %{{.*}} = smt.bv.cmp uge [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
+ %24 = smt.bv.cmp uge %c, %c {smt.some_attr} : !smt.bv<32>
+
+ // CHECK: %{{.*}} = smt.bv.concat [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>, !smt.bv<32>
+ %25 = smt.bv.concat %c, %c {smt.some_attr} : !smt.bv<32>, !smt.bv<32>
+ // CHECK: %{{.*}} = smt.bv.extract [[C0]] from 8 {smt.some_attr} : (!smt.bv<32>) -> !smt.bv<16>
+ %26 = smt.bv.extract %c from 8 {smt.some_attr} : (!smt.bv<32>) -> !smt.bv<16>
+ // CHECK: %{{.*}} = smt.bv.repeat 2 times [[C0]] {smt.some_attr} : !smt.bv<32>
+ %27 = smt.bv.repeat 2 times %c {smt.some_attr} : !smt.bv<32>
+
+ // CHECK: %{{.*}} = smt.bv2int [[C0]] {smt.some_attr} : !smt.bv<32>
+ %29 = smt.bv2int %c {smt.some_attr} : !smt.bv<32>
+ // CHECK: %{{.*}} = smt.bv2int [[C0]] signed {smt.some_attr} : !smt.bv<32>
+ %28 = smt.bv2int %c signed {smt.some_attr} : !smt.bv<32>
+
+ return
+}
diff --git a/mlir/test/Dialect/SMT/core-errors.mlir b/mlir/test/Dialect/SMT/core-errors.mlir
new file mode 100644
index 0000000000000..67bebda56b68e
--- /dev/null
+++ b/mlir/test/Dialect/SMT/core-errors.mlir
@@ -0,0 +1,497 @@
+// RUN: mlir-opt %s --split-input-file --verify-diagnostics
+
+func.func @solver_isolated_from_above(%arg0: !smt.bool) {
+ // expected-note @below {{required by region isolation constraints}}
+ smt.solver() : () -> () {
+ // expected-error @below {{using value defined outside the region}}
+ smt.assert %arg0
+ }
+ return
+}
+
+// -----
+
+func.func @no_smt_value_enters_solver(%arg0: !smt.bool) {
+ // expected-error @below {{operand #0 must be variadic of any non-smt type, but got '!smt.bool'}}
+ smt.solver(%arg0) : (!smt.bool) -> () {
+ ^bb0(%arg1: !smt.bool):
+ smt.assert %arg1
+ }
+ return
+}
+
+// -----
+
+func.func @no_smt_value_exits_solver() {
+ // expected-error @below {{result #0 must be variadic of any non-smt type, but got '!smt.bool'}}
+ %0 = smt.solver() : () -> !smt.bool {
+ %a = smt.declare_fun "a" : !smt.bool
+ smt.yield %a : !smt.bool
+ }
+ return
+}
+
+// -----
+
+func.func @block_args_and_inputs_match() {
+ // expected-error @below {{block argument types must match the types of the 'inputs'}}
+ smt.solver() : () -> () {
+ ^bb0(%arg0: i32):
+ }
+ return
+}
+
+// -----
+
+func.func @solver_yield_operands_and_results_match() {
+ // expected-error @below {{types of yielded values must match return values}}
+ smt.solver() : () -> () {
+ %1 = arith.constant 0 : i32
+ smt.yield %1 : i32
+ }
+ return
+}
+
+// -----
+
+func.func @check_yield_operands_and_results_match() {
+ // expected-error @below {{types of yielded values in 'unsat' region must match return values}}
+ %0 = smt.check sat {
+ %1 = arith.constant 0 : i32
+ smt.yield %1 : i32
+ } unknown {
+ %1 = arith.constant 0 : i32
+ smt.yield %1 : i32
+ } unsat { } -> i32
+ return
+}
+
+// -----
+
+func.func @check_yield_operands_and_results_match() {
+ // expected-error @below {{types of yielded values in 'unknown' region must match return values}}
+ %0 = smt.check sat {
+ %1 = arith.constant 0 : i32
+ smt.yield %1 : i32
+ } unknown {
+ } unsat {
+ %1 = arith.constant 0 : i32
+ smt.yield %1 : i32
+ } -> i32
+ return
+}
+
+// -----
+
+func.func @check_yield_operands_and_results_match() {
+ // expected-error @below {{types of yielded values in 'sat' region must match return values}}
+ %0 = smt.check sat {
+ } unknown {
+ %1 = arith.constant 0 : i32
+ smt.yield %1 : i32
+ } unsat {
+ %1 = arith.constant 0 : i32
+ smt.yield %1 : i32
+ } -> i32
+ return
+}
+
+// -----
+
+func.func @check_no_block_arguments() {
+ // expected-error @below {{region #0 should have no arguments}}
+ smt.check sat {
+ ^bb0(%arg0: i32):
+ } unknown {
+ } unsat {
+ }
+ return
+}
+
+// -----
+
+func.func @check_no_block_arguments() {
+ // expected-error @below {{region #1 should have no arguments}}
+ smt.check sat {
+ } unknown {
+ ^bb0(%arg0: i32):
+ } unsat {
+ }
+ return
+}
+
+// -----
+
+func.func @check_no_block_arguments() {
+ // expected-error @below {{region #2 should have no arguments}}
+ smt.check sat {
+ } unknown {
+ } unsat {
+ ^bb0(%arg0: i32):
+ }
+ return
+}
+
+// -----
+
+func.func @too_few_operands() {
+ // expected-error @below {{'inputs' must have at least size 2, but got 0}}
+ smt.eq : !smt.bool
+ return
+}
+
+// -----
+
+func.func @too_few_operands(%a: !smt.bool) {
+ // expected-error @below {{'inputs' must have at least size 2, but got 1}}
+ smt.distinct %a : !smt.bool
+ return
+}
+
+// -----
+
+func.func @ite_type_mismatch(%a: !smt.bool, %b: !smt.bv<32>) {
+ // expected-error @below {{failed to verify that all of {thenValue, elseValue, result} have same type}}
+ "smt.ite"(%a, %a, %b) {} : (!smt.bool, !smt.bool, !smt.bv<32>) -> !smt.bool
+ return
+}
+
+// -----
+
+func.func @forall_number_of_decl_names_must_match_num_args() {
+ // expected-error @below {{number of bound variable names must match number of block arguments}}
+ %1 = smt.forall ["a"] {
+ ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+ %2 = smt.eq %arg2, %arg3 : !smt.int
+ smt.yield %2 : !smt.bool
+ }
+ return
+}
+
+// -----
+
+func.func @exists_number_of_decl_names_must_match_num_args() {
+ // expected-error @below {{number of bound variable names must match number of block arguments}}
+ %1 = smt.exists ["a"] {
+ ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+ %2 = smt.eq %arg2, %arg3 : !smt.int
+ smt.yield %2 : !smt.bool
+ }
+ return
+}
+
+// -----
+
+func.func @forall_yield_must_have_exactly_one_bool_value() {
+ // expected-error @below {{yielded value must be of '!smt.bool' type}}
+ %1 = smt.forall ["a", "b"] {
+ ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+ %2 = smt.int.add %arg2, %arg3
+ smt.yield %2 : !smt.int
+ }
+ return
+}
+
+// -----
+
+func.func @forall_yield_must_have_exactly_one_bool_value() {
+ // expected-error @below {{must have exactly one yielded value}}
+ %1 = smt.forall ["a", "b"] {
+ ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+ smt.yield
+ }
+ return
+}
+
+// -----
+
+func.func @exists_yield_must_have_exactly_one_bool_value() {
+ // expected-error @below {{yielded value must be of '!smt.bool' type}}
+ %1 = smt.exists ["a", "b"] {
+ ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+ %2 = smt.int.add %arg2, %arg3
+ smt.yield %2 : !smt.int
+ }
+ return
+}
+
+// -----
+
+func.func @exists_yield_must_have_exactly_one_bool_value() {
+ // expected-error @below {{must have exactly one yielded value}}
+ %1 = smt.exists ["a", "b"] {
+ ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+ smt.yield
+ }
+ return
+}
+
+// -----
+
+func.func @exists_patterns_region_and_no_patterns_attr_are_mutually_exclusive() {
+ // expected-error @below {{patterns and the no_pattern attribute must not be specified at the same time}}
+ %1 = smt.exists ["a"] no_pattern {
+ ^bb0(%arg2: !smt.bool):
+ smt.yield %arg2 : !smt.bool
+ } patterns {
+ ^bb0(%arg2: !smt.bool):
+ smt.yield %arg2 : !smt.bool
+ }
+ return
+}
+
+// -----
+
+func.func @forall_patterns_region_and_no_patterns_attr_are_mutually_exclusive() {
+ // expected-error @below {{patterns and the no_pattern attribute must not be specified at the same time}}
+ %1 = smt.forall ["a"] no_pattern {
+ ^bb0(%arg2: !smt.bool):
+ smt.yield %arg2 : !smt.bool
+ } patterns {
+ ^bb0(%arg2: !smt.bool):
+ smt.yield %arg2 : !smt.bool
+ }
+ return
+}
+
+// -----
+
+func.func @exists_patterns_region_num_args() {
+ // expected-error @below {{block argument number and types of the 'body' and 'patterns' region #0 must match}}
+ %1 = smt.exists ["a"] {
+ ^bb0(%arg2: !smt.bool):
+ smt.yield %arg2 : !smt.bool
+ } patterns {
+ ^bb0(%arg2: !smt.bool, %arg3: !smt.bool):
+ smt.yield %arg2, %arg3 : !smt.bool, !smt.bool
+ }
+ return
+}
+
+// -----
+
+func.func @forall_patterns_region_num_args() {
+ // expected-error @below {{block argument number and types of the 'body' and 'patterns' region #0 must match}}
+ %1 = smt.forall ["a"] {
+ ^bb0(%arg2: !smt.bool):
+ smt.yield %arg2 : !smt.bool
+ } patterns {
+ ^bb0(%arg2: !smt.bool, %arg3: !smt.bool):
+ smt.yield %arg2, %arg3 : !smt.bool, !smt.bool
+ }
+ return
+}
+
+// -----
+
+func.func @exists_patterns_region_at_least_one_yielded_value() {
+ // expected-error @below {{'patterns' region #0 must have at least one yielded value}}
+ %1 = smt.exists ["a"] {
+ ^bb0(%arg2: !smt.bool):
+ smt.yield %arg2 : !smt.bool
+ } patterns {
+ ^bb0(%arg2: !smt.bool):
+ smt.yield
+ }
+ return
+}
+
+// -----
+
+func.func @forall_patterns_region_at_least_one_yielded_value() {
+ // expected-error @below {{'patterns' region #0 must have at least one yielded value}}
+ %1 = smt.forall ["a"] {
+ ^bb0(%arg2: !smt.bool):
+ smt.yield %arg2 : !smt.bool
+ } patterns {
+ ^bb0(%arg2: !smt.bool):
+ smt.yield
+ }
+ return
+}
+
+// -----
+
+func.func @exists_all_pattern_regions_tested() {
+ // expected-error @below {{'patterns' region #1 must have at least one yielded value}}
+ %1 = smt.exists ["a"] {
+ ^bb0(%arg2: !smt.bool):
+ smt.yield %arg2 : !smt.bool
+ } patterns {
+ ^bb0(%arg2: !smt.bool):
+ smt.yield %arg2 : !smt.bool
+ }, {
+ ^bb0(%arg2: !smt.bool):
+ smt.yield
+ }
+ return
+}
+
+// -----
+
+func.func @forall_all_pattern_regions_tested() {
+ // expected-error @below {{'patterns' region #1 must have at least one yielded value}}
+ %1 = smt.forall ["a"] {
+ ^bb0(%arg2: !smt.bool):
+ smt.yield %arg2 : !smt.bool
+ } patterns {
+ ^bb0(%arg2: !smt.bool):
+ smt.yield %arg2 : !smt.bool
+ }, {
+ ^bb0(%arg2: !smt.bool):
+ smt.yield
+ }
+ return
+}
+
+// -----
+
+func.func @exists_patterns_region_no_non_smt_operations() {
+ // expected-error @below {{'patterns' region #0 may only contain SMT dialect operations}}
+ %1 = smt.exists ["a"] {
+ ^bb0(%arg2: !smt.bool):
+ smt.yield %arg2 : !smt.bool
+ } patterns {
+ ^bb0(%arg2: !smt.bool):
+ // expected-note @below {{first non-SMT operation here}}
+ arith.constant 0 : i32
+ smt.yield %arg2 : !smt.bool
+ }
+ return
+}
+
+// -----
+
+func.func @forall_patterns_region_no_non_smt_operations() {
+ // expected-error @below {{'patterns' region #0 may only contain SMT dialect operations}}
+ %1 = smt.forall ["a"] {
+ ^bb0(%arg2: !smt.bool):
+ smt.yield %arg2 : !smt.bool
+ } patterns {
+ ^bb0(%arg2: !smt.bool):
+ // expected-note @below {{first non-SMT operation here}}
+ arith.constant 0 : i32
+ smt.yield %arg2 : !smt.bool
+ }
+ return
+}
+
+// -----
+
+func.func @exists_patterns_region_no_var_binding_operations() {
+ // expected-error @below {{'patterns' region #0 must not contain any variable binding operations}}
+ %1 = smt.exists ["a"] {
+ ^bb0(%arg2: !smt.bool):
+ smt.yield %arg2 : !smt.bool
+ } patterns {
+ ^bb0(%arg2: !smt.bool):
+ // expected-note @below {{first violating operation here}}
+ smt.exists ["b"] {
+ ^bb0(%arg3: !smt.bool):
+ smt.yield %arg3 : !smt.bool
+ }
+ smt.yield %arg2 : !smt.bool
+ }
+ return
+}
+
+// -----
+
+func.func @forall_patterns_region_no_var_binding_operations() {
+ // expected-error @below {{'patterns' region #0 must not contain any variable binding operations}}
+ %1 = smt.forall ["a"] {
+ ^bb0(%arg2: !smt.bool):
+ smt.yield %arg2 : !smt.bool
+ } patterns {
+ ^bb0(%arg2: !smt.bool):
+ // expected-note @below {{first violating operation here}}
+ smt.forall ["b"] {
+ ^bb0(%arg3: !smt.bool):
+ smt.yield %arg3 : !smt.bool
+ }
+ smt.yield %arg2 : !smt.bool
+ }
+ return
+}
+
+// -----
+
+func.func @exists_bound_variable_type_invalid() {
+ // expected-error @below {{bound variables must by any non-function SMT value}}
+ %1 = smt.exists ["a", "b"] {
+ ^bb0(%arg2: !smt.func<(!smt.int) !smt.int>, %arg3: !smt.bool):
+ smt.yield %arg3 : !smt.bool
+ }
+ return
+}
+
+// -----
+
+func.func @forall_bound_variable_type_invalid() {
+ // expected-error @below {{bound variables must by any non-function SMT value}}
+ %1 = smt.forall ["a", "b"] {
+ ^bb0(%arg2: !smt.func<(!smt.int) !smt.int>, %arg3: !smt.bool):
+ smt.yield %arg3 : !smt.bool
+ }
+ return
+}
+
+// -----
+
+// expected-error @below {{domain types must be any non-function SMT type}}
+func.func @func_domain_no_smt_type(%arg0: !smt.func<(i32) !smt.bool>) {
+ return
+}
+
+// -----
+
+// expected-error @below {{range type must be any non-function SMT type}}
+func.func @func_range_no_smt_type(%arg0: !smt.func<(!smt.bool) i32>) {
+ return
+}
+
+// -----
+
+// expected-error @below {{range type must be any non-function SMT type}}
+func.func @func_range_no_smt_type(%arg0: !smt.func<(!smt.bool) !smt.func<(!smt.bool) !smt.bool>>) {
+ return
+}
+
+// -----
+
+func.func @func_range_no_smt_type(%arg0: !smt.func<(!smt.bool) !smt.bool>) {
+ // expected-error @below {{got 0 operands and 1 types}}
+ smt.apply_func %arg0() : !smt.func<(!smt.bool) !smt.bool>
+ return
+}
+
+// -----
+
+// expected-error @below {{sort parameter types must be any non-function SMT type}}
+func.func @sort_type_no_smt_type(%arg0: !smt.sort<"sortname"[i32]>) {
+ return
+}
+
+// -----
+
+func.func @negative_push() {
+ // expected-error @below {{smt.push' op attribute 'count' failed to satisfy constraint: 32-bit signless integer attribute whose value is non-negative}}
+ smt.push -1
+ return
+}
+
+// -----
+
+func.func @negative_pop() {
+ // expected-error @below {{smt.pop' op attribute 'count' failed to satisfy constraint: 32-bit signless integer attribute whose value is non-negative}}
+ smt.pop -1
+ return
+}
+
+// -----
+
+func.func @set_logic_outside_solver() {
+ // expected-error @below {{'smt.set_logic' op expects parent op 'smt.solver'}}
+ smt.set_logic "AUFLIA"
+ return
+}
diff --git a/mlir/test/Dialect/SMT/cse-test.mlir b/mlir/test/Dialect/SMT/cse-test.mlir
new file mode 100644
index 0000000000000..ff254857f3b33
--- /dev/null
+++ b/mlir/test/Dialect/SMT/cse-test.mlir
@@ -0,0 +1,12 @@
+// RUN: mlir-opt %s --cse | FileCheck %s
+
+func.func @declare_const_cse(%in: i8) -> (!smt.bool, !smt.bool){
+ // CHECK: smt.declare_fun "a" : !smt.bool
+ %a = smt.declare_fun "a" : !smt.bool
+ // CHECK-NEXT: smt.declare_fun "a" : !smt.bool
+ %b = smt.declare_fun "a" : !smt.bool
+ // CHECK-NEXT: return
+ %c = smt.declare_fun "a" : !smt.bool
+
+ return %a, %b : !smt.bool, !smt.bool
+}
diff --git a/mlir/test/Dialect/SMT/integers.mlir b/mlir/test/Dialect/SMT/integers.mlir
new file mode 100644
index 0000000000000..f5133c8c72b5d
--- /dev/null
+++ b/mlir/test/Dialect/SMT/integers.mlir
@@ -0,0 +1,36 @@
+// RUN: mlir-opt %s | mlir-opt | FileCheck %s
+
+// CHECK-LABEL: func @integer_operations
+func.func @integer_operations() {
+ // CHECK-NEXT: [[V0:%.+]] = smt.int.constant -123 {smt.some_attr}
+ %0 = smt.int.constant -123 {smt.some_attr}
+ // CHECK-NEXT: %c184467440737095516152 = smt.int.constant 184467440737095516152 {smt.some_attr}
+ %1 = smt.int.constant 184467440737095516152 {smt.some_attr}
+
+
+ // CHECK-NEXT: smt.int.add [[V0]], [[V0]], [[V0]] {smt.some_attr}
+ %2 = smt.int.add %0, %0, %0 {smt.some_attr}
+ // CHECK-NEXT: smt.int.mul [[V0]], [[V0]], [[V0]] {smt.some_attr}
+ %3 = smt.int.mul %0, %0, %0 {smt.some_attr}
+ // CHECK-NEXT: smt.int.sub [[V0]], [[V0]] {smt.some_attr}
+ %4 = smt.int.sub %0, %0 {smt.some_attr}
+ // CHECK-NEXT: smt.int.div [[V0]], [[V0]] {smt.some_attr}
+ %5 = smt.int.div %0, %0 {smt.some_attr}
+ // CHECK-NEXT: smt.int.mod [[V0]], [[V0]] {smt.some_attr}
+ %6 = smt.int.mod %0, %0 {smt.some_attr}
+ // CHECK-NEXT: smt.int.abs [[V0]] {smt.some_attr}
+ %7 = smt.int.abs %0 {smt.some_attr}
+
+ // CHECK-NEXT: smt.int.cmp le [[V0]], [[V0]] {smt.some_attr}
+ %9 = smt.int.cmp le %0, %0 {smt.some_attr}
+ // CHECK-NEXT: smt.int.cmp lt [[V0]], [[V0]] {smt.some_attr}
+ %10 = smt.int.cmp lt %0, %0 {smt.some_attr}
+ // CHECK-NEXT: smt.int.cmp ge [[V0]], [[V0]] {smt.some_attr}
+ %11 = smt.int.cmp ge %0, %0 {smt.some_attr}
+ // CHECK-NEXT: smt.int.cmp gt [[V0]], [[V0]] {smt.some_attr}
+ %12 = smt.int.cmp gt %0, %0 {smt.some_attr}
+ // CHECK-NEXT: smt.int2bv [[V0]] {smt.some_attr} : !smt.bv<4>
+ %13 = smt.int2bv %0 {smt.some_attr} : !smt.bv<4>
+
+ return
+}
>From 86a8cc60cd4eff9a684bb248f7accdd7437fb54e 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 2/2] [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