[Mlir-commits] [mlir] [mlir][SMT] upstream `SMT` dialect (PR #131480)
Maksim Levental
llvmlistbot at llvm.org
Wed Apr 9 16:28:08 PDT 2025
https://github.com/makslevental updated https://github.com/llvm/llvm-project/pull/131480
>From 632011ed8983ae68dd3863ed35d33ecd555609a6 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/7] [mlir][smt] upstream SMT dialect
Co-authored-by: Bea Healy <beahealy22 at gmail.com>
Co-authored-by: Martin Erhart <maerhart at outlook.com>
Co-authored-by: Mike Urbach <mikeurbach at gmail.com>
Co-authored-by: Will Dietz <will.dietz at sifive.com>
Co-authored-by: fzi-hielscher <hielscher at fzi.de>
---
mlir/include/mlir/Dialect/CMakeLists.txt | 1 +
mlir/include/mlir/Dialect/SMT/CMakeLists.txt | 1 +
.../mlir/Dialect/SMT/IR/CMakeLists.txt | 15 +
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 | 475 +++++++++++++++++
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, 3367 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..1455551f93fb2
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/IR/CMakeLists.txt
@@ -0,0 +1,15 @@
+add_mlir_dialect(SMT 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)
+
+add_mlir_doc(SMT SMT Dialects/ -gen-dialect-doc)
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..c7793b9b36be7
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTOps.td
@@ -0,0 +1,475 @@
+//===- 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
+ }
+ ```
+ }];
+
+ 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 edf0f55c83fbbb2a9085ae25f503614f33c38cb7 Mon Sep 17 00:00:00 2001
From: Maksim Levental <maksim.levental at gmail.com>
Date: Wed, 9 Apr 2025 18:46:19 -0400
Subject: [PATCH 2/7] Update mlir/include/mlir/Dialect/SMT/IR/SMTOps.td
Co-authored-by: Fehr Mathieu <mathieu.fehr at gmail.com>
---
mlir/include/mlir/Dialect/SMT/IR/SMTOps.td | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTOps.td b/mlir/include/mlir/Dialect/SMT/IR/SMTOps.td
index c7793b9b36be7..03833497af1f9 100644
--- a/mlir/include/mlir/Dialect/SMT/IR/SMTOps.td
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTOps.td
@@ -27,7 +27,7 @@ def DeclareFunOp : SMTOp<"declare_fun", [
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
+ `declare-fun` 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.
>From 8b7ad0ed01be79259e23d88ac7620cd859c9bb6f Mon Sep 17 00:00:00 2001
From: Maksim Levental <maksim.levental at gmail.com>
Date: Wed, 9 Apr 2025 18:46:47 -0400
Subject: [PATCH 3/7] Update mlir/include/mlir/Dialect/SMT/IR/SMTOps.h
Co-authored-by: Martin Erhart <maerhart at outlook.com>
---
mlir/include/mlir/Dialect/SMT/IR/SMTOps.h | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTOps.h b/mlir/include/mlir/Dialect/SMT/IR/SMTOps.h
index 859566ec6dbdb..869ebdc93a395 100644
--- a/mlir/include/mlir/Dialect/SMT/IR/SMTOps.h
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTOps.h
@@ -6,7 +6,7 @@
//
//===----------------------------------------------------------------------===//
-#ifndef MLIR_DIALECT_SMT_SMTOPS_H
+#ifndef MLIR_DIALECT_SMT_IR_SMTOPS_H
#define MLIR_DIALECT_SMT_SMTOPS_H
#include "mlir/IR/OpImplementation.h"
>From bf5521ddefdf0e243f8e969aea7a69f452b16335 Mon Sep 17 00:00:00 2001
From: Maksim Levental <maksim.levental at gmail.com>
Date: Wed, 9 Apr 2025 18:51:01 -0400
Subject: [PATCH 4/7] smt-lib 2.7 standard
---
.../mlir/Dialect/SMT/IR/SMTArrayOps.td | 4 ++--
.../mlir/Dialect/SMT/IR/SMTBitVectorOps.td | 10 +++++-----
mlir/include/mlir/Dialect/SMT/IR/SMTIntOps.td | 10 +++++-----
mlir/include/mlir/Dialect/SMT/IR/SMTOps.td | 20 +++++++++----------
mlir/include/mlir/Dialect/SMT/IR/SMTTypes.td | 8 ++++----
5 files changed, 26 insertions(+), 26 deletions(-)
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTArrayOps.td b/mlir/include/mlir/Dialect/SMT/IR/SMTArrayOps.td
index 05b5398b6a7f9..7e405cd9dd4d6 100644
--- a/mlir/include/mlir/Dialect/SMT/IR/SMTArrayOps.td
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTArrayOps.td
@@ -31,7 +31,7 @@ def ArrayStoreOp : SMTArrayOp<"store", [
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.
+ the SMT-LIB standard 2.7.
}];
let arguments = (ins ArrayType:$array, AnySMTType:$index, AnySMTType:$value);
@@ -54,7 +54,7 @@ def ArraySelectOp : SMTArrayOp<"select", [
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.
+ the SMT-LIB standard 2.7.
}];
let arguments = (ins ArrayType:$array, AnySMTType:$index);
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTBitVectorOps.td b/mlir/include/mlir/Dialect/SMT/IR/SMTBitVectorOps.td
index b6ca34e142d82..a4948f2b518ec 100644
--- a/mlir/include/mlir/Dialect/SMT/IR/SMTBitVectorOps.td
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTBitVectorOps.td
@@ -65,7 +65,7 @@ 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
+ equivalent to the `bv}] # mnemonic # [{` operator defined in the SMT-LIB 2.7
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
@@ -128,7 +128,7 @@ def BVCmpOp : SMTBVOp<"cmp", [Pure, SameTypeOperands]> {
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
+ `bvuge` operator defined in the SMT-LIB 2.7 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)
@@ -153,7 +153,7 @@ def ConcatOp : SMTBVOp<"concat", [
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 `concat` operator defined in the SMT-LIB 2.7 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
@@ -177,7 +177,7 @@ def ExtractOp : SMTBVOp<"extract", [Pure]> {
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
+ 2.7 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
@@ -215,7 +215,7 @@ def RepeatOp : SMTBVOp<"repeat", [Pure]> {
```
The semantics are equivalent to the `repeat` operator defined in the SMT-LIB
- 2.6 standard. More precisely in the
+ 2.7 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
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTIntOps.td b/mlir/include/mlir/Dialect/SMT/IR/SMTIntOps.td
index 6606c9608ef55..c9b5d6bf5055a 100644
--- a/mlir/include/mlir/Dialect/SMT/IR/SMTIntOps.td
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTIntOps.td
@@ -31,7 +31,7 @@ def IntConstantOp : SMTIntOp<"constant", [
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.
+ SMT-LIB 2.7 standard.
}];
let arguments = (ins APIntAttr:$value);
@@ -46,7 +46,7 @@ class VariadicIntOp<string mnemonic> : SMTIntOp<mnemonic, [Pure, Commutative]> {
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.
+ SMT-LIB 2.7 standard.
}];
let arguments = (ins Variadic<IntType>:$inputs);
@@ -65,7 +65,7 @@ class BinaryIntOp<string mnemonic> : SMTIntOp<mnemonic, [Pure]> {
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.
+ SMT-LIB 2.7 standard.
}];
let arguments = (ins IntType:$lhs, IntType:$rhs);
@@ -79,7 +79,7 @@ def IntAbsOp : SMTIntOp<"abs", [Pure]> {
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.
+ SMT-LIB 2.7 standard.
}];
let arguments = (ins IntType:$input);
@@ -111,7 +111,7 @@ def IntCmpOp : SMTIntOp<"cmp", [Pure]> {
`> (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.
+ SMT-LIB 2.7 standard.
}];
let arguments = (ins IntPredicate:$pred, IntType:$lhs, IntType:$rhs);
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTOps.td b/mlir/include/mlir/Dialect/SMT/IR/SMTOps.td
index 03833497af1f9..d606a78b3cef8 100644
--- a/mlir/include/mlir/Dialect/SMT/IR/SMTOps.td
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTOps.td
@@ -27,7 +27,7 @@ def DeclareFunOp : SMTOp<"declare_fun", [
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-fun` statements in SMT-LIB 2.6. The result type determines the SMT
+ `declare-fun` statements in SMT-LIB 2.7. 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.
@@ -82,7 +82,7 @@ def BoolConstantOp : SMTOp<"constant", [
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.
+ Standard 2.7.
}];
let arguments = (ins BoolAttr:$value);
@@ -241,7 +241,7 @@ def ApplyFuncOp : SMTOp<"apply_func", [
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).
+ [SMT-LIB 2.7 standard](https://smt-lib.org/papers/smt-lib-reference-v2.7-r2025-02-05.pdf).
It is part of the language itself rather than a theory or logic.
}];
@@ -259,7 +259,7 @@ def EqOp : SMTOp<"eq", [Pure, SameTypeOperands]> {
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
+ SMT-LIB Standard 2.7 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
@@ -288,7 +288,7 @@ def DistinctOp : SMTOp<"distinct", [Pure, SameTypeOperands]> {
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
+ the `distinct` operator defined in the SMT-LIB Standard 2.7 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
@@ -334,7 +334,7 @@ def IteOp : SMTOp<"ite", [
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.
+ 2.7 standard.
}];
let arguments = (ins BoolType:$cond,
@@ -353,7 +353,7 @@ def NotOp : SMTOp<"not", [Pure]> {
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.
+ Standard 2.7.
}];
let arguments = (ins BoolType:$input);
@@ -366,7 +366,7 @@ class VariadicBoolOp<string mnemonic, string desc> : SMTOp<mnemonic, [Pure]> {
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.
+ of the SMT-LIB Standard 2.7.
It supports a variadic number of operands, but requires at least two.
This is because the operator is annotated with the `:left-assoc` attribute
@@ -394,7 +394,7 @@ def ImpliesOp : SMTOp<"implies", [Pure]> {
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.
+ Standard 2.7.
}];
let arguments = (ins BoolType:$lhs, BoolType:$rhs);
@@ -409,7 +409,7 @@ class QuantifierOp<string mnemonic> : SMTOp<mnemonic, [
]> {
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).
+ [SMT-LIB 2.7 standard](https://smt-lib.org/papers/smt-lib-reference-v2.7-r2025-02-05.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
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTTypes.td b/mlir/include/mlir/Dialect/SMT/IR/SMTTypes.td
index 3032900b52178..f17a1a0e6fa1b 100644
--- a/mlir/include/mlir/Dialect/SMT/IR/SMTTypes.td
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTTypes.td
@@ -24,7 +24,7 @@ def IntType : SMTTypeDef<"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.
+ SMT-LIB 2.7 standard.
}];
let assemblyFormat = "";
}
@@ -51,7 +51,7 @@ def ArrayType : SMTTypeDef<"Array"> {
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.
+ the SMT-LIB standard 2.7.
}];
let parameters = (ins "mlir::Type":$domainType, "mlir::Type":$rangeType);
@@ -64,7 +64,7 @@ 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).
+ [SMT-LIB 2.7 standard](https://smt-lib.org/papers/smt-lib-reference-v2.7-r2025-02-05.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
@@ -111,7 +111,7 @@ def SortType : SMTTypeDef<"Sort"> {
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).
+ [SMT-LIB 2.7 standard](https://smt-lib.org/papers/smt-lib-reference-v2.7-r2025-02-05.pdf).
}];
let parameters = (ins
>From 784540cfb226b03753934041de0387aa1cb5ad39 Mon Sep 17 00:00:00 2001
From: Maksim Levental <maksim.levental at gmail.com>
Date: Wed, 9 Apr 2025 18:52:54 -0400
Subject: [PATCH 5/7] bv integer non-negative
---
mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.td | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.td b/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.td
index 4231363fdf05b..f77b306e4ec45 100644
--- a/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.td
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.td
@@ -28,8 +28,8 @@ def BitVectorAttr : AttrDef<SMTDialect, "BitVector", [
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.
+ prefixing. Here, the bit-vector constant is given as a regular non-negative
+ integer literal and the associated bit-vector type indicating the bit-width.
Examples:
```mlir
>From 3f372378b9eafe8f1834f2b90a8d8fe256160044 Mon Sep 17 00:00:00 2001
From: Maksim Levental <maksim.levental at gmail.com>
Date: Wed, 9 Apr 2025 19:27:33 -0400
Subject: [PATCH 6/7] header guard
---
mlir/include/mlir/Dialect/SMT/IR/SMT.td | 6 +++---
mlir/include/mlir/Dialect/SMT/IR/SMTArrayOps.td | 6 +++---
mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.h | 6 +++---
mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.td | 6 +++---
mlir/include/mlir/Dialect/SMT/IR/SMTBitVectorOps.td | 6 +++---
mlir/include/mlir/Dialect/SMT/IR/SMTDialect.h | 6 +++---
mlir/include/mlir/Dialect/SMT/IR/SMTDialect.td | 6 +++---
mlir/include/mlir/Dialect/SMT/IR/SMTIntOps.td | 6 +++---
mlir/include/mlir/Dialect/SMT/IR/SMTOps.h | 4 ++--
mlir/include/mlir/Dialect/SMT/IR/SMTOps.td | 6 +++---
mlir/include/mlir/Dialect/SMT/IR/SMTTypes.h | 6 +++---
mlir/include/mlir/Dialect/SMT/IR/SMTTypes.td | 6 +++---
mlir/include/mlir/Dialect/SMT/IR/SMTVisitors.h | 6 +++---
13 files changed, 38 insertions(+), 38 deletions(-)
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMT.td b/mlir/include/mlir/Dialect/SMT/IR/SMT.td
index dd7bd033c9fa5..6d0e0532ebe24 100644
--- a/mlir/include/mlir/Dialect/SMT/IR/SMT.td
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMT.td
@@ -6,8 +6,8 @@
//
//===----------------------------------------------------------------------===//
-#ifndef MLIR_DIALECT_SMT_SMT_TD
-#define MLIR_DIALECT_SMT_SMT_TD
+#ifndef MLIR_DIALECT_SMT_IR_SMT_TD
+#define MLIR_DIALECT_SMT_IR_SMT_TD
include "mlir/IR/OpBase.td"
@@ -19,4 +19,4 @@ 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
+#endif // MLIR_DIALECT_SMT_IR_SMT_TD
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTArrayOps.td b/mlir/include/mlir/Dialect/SMT/IR/SMTArrayOps.td
index 7e405cd9dd4d6..1869f4ae81595 100644
--- a/mlir/include/mlir/Dialect/SMT/IR/SMTArrayOps.td
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTArrayOps.td
@@ -6,8 +6,8 @@
//
//===----------------------------------------------------------------------===//
-#ifndef MLIR_DIALECT_SMT_SMTARRAYOPS_TD
-#define MLIR_DIALECT_SMT_SMTARRAYOPS_TD
+#ifndef MLIR_DIALECT_SMT_IR_SMTARRAYOPS_TD
+#define MLIR_DIALECT_SMT_IR_SMTARRAYOPS_TD
include "mlir/Dialect/SMT/IR/SMTDialect.td"
include "mlir/Dialect/SMT/IR/SMTAttributes.td"
@@ -96,4 +96,4 @@ def ArrayBroadcastOp : SMTArrayOp<"broadcast", [
let assemblyFormat = "$value attr-dict `:` qualified(type($result))";
}
-#endif // MLIR_DIALECT_SMT_SMTARRAYOPS_TD
+#endif // MLIR_DIALECT_SMT_IR_SMTARRAYOPS_TD
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.h b/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.h
index 590364d572699..8db8a1f198cf9 100644
--- a/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.h
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.h
@@ -6,8 +6,8 @@
//
//===----------------------------------------------------------------------===//
-#ifndef MLIR_DIALECT_SMT_SMTATTRIBUTES_H
-#define MLIR_DIALECT_SMT_SMTATTRIBUTES_H
+#ifndef MLIR_DIALECT_SMT_IR_SMTATTRIBUTES_H
+#define MLIR_DIALECT_SMT_IR_SMTATTRIBUTES_H
#include "mlir/IR/Attributes.h"
#include "mlir/IR/BuiltinAttributeInterfaces.h"
@@ -26,4 +26,4 @@ struct BitVectorAttrStorage;
#define GET_ATTRDEF_CLASSES
#include "mlir/Dialect/SMT/IR/SMTAttributes.h.inc"
-#endif // MLIR_DIALECT_SMT_SMTATTRIBUTES_H
+#endif // MLIR_DIALECT_SMT_IR_SMTATTRIBUTES_H
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.td b/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.td
index f77b306e4ec45..0909c9abad951 100644
--- a/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.td
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.td
@@ -10,8 +10,8 @@
//
//===----------------------------------------------------------------------===//
-#ifndef MLIR_DIALECT_SMT_SMTATTRIBUTES_TD
-#define MLIR_DIALECT_SMT_SMTATTRIBUTES_TD
+#ifndef MLIR_DIALECT_SMT_IR_SMTATTRIBUTES_TD
+#define MLIR_DIALECT_SMT_IR_SMTATTRIBUTES_TD
include "mlir/Dialect/SMT/IR/SMTDialect.td"
include "mlir/IR/EnumAttr.td"
@@ -71,4 +71,4 @@ def BitVectorAttr : AttrDef<SMTDialect, "BitVector", [
}];
}
-#endif // MLIR_DIALECT_SMT_SMTATTRIBUTES_TD
+#endif // MLIR_DIALECT_SMT_IR_SMTATTRIBUTES_TD
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTBitVectorOps.td b/mlir/include/mlir/Dialect/SMT/IR/SMTBitVectorOps.td
index a4948f2b518ec..c7422dd11f634 100644
--- a/mlir/include/mlir/Dialect/SMT/IR/SMTBitVectorOps.td
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTBitVectorOps.td
@@ -6,8 +6,8 @@
//
//===----------------------------------------------------------------------===//
-#ifndef MLIR_DIALECT_SMT_SMTBITVECTOROPS_TD
-#define MLIR_DIALECT_SMT_SMTBITVECTOROPS_TD
+#ifndef MLIR_DIALECT_SMT_IR_SMTBITVECTOROPS_TD
+#define MLIR_DIALECT_SMT_IR_SMTBITVECTOROPS_TD
include "mlir/Dialect/SMT/IR/SMTDialect.td"
include "mlir/Dialect/SMT/IR/SMTAttributes.td"
@@ -252,4 +252,4 @@ def BV2IntOp : SMTOp<"bv2int", [Pure]> {
qualified(type($input))}];
}
-#endif // MLIR_DIALECT_SMT_SMTBITVECTOROPS_TD
+#endif // MLIR_DIALECT_SMT_IR_SMTBITVECTOROPS_TD
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTDialect.h b/mlir/include/mlir/Dialect/SMT/IR/SMTDialect.h
index e808583a9e593..2c44ca802a2d5 100644
--- a/mlir/include/mlir/Dialect/SMT/IR/SMTDialect.h
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTDialect.h
@@ -6,8 +6,8 @@
//
//===----------------------------------------------------------------------===//
-#ifndef MLIR_DIALECT_SMT_SMTDIALECT_H
-#define MLIR_DIALECT_SMT_SMTDIALECT_H
+#ifndef MLIR_DIALECT_SMT_IR_SMTDIALECT_H
+#define MLIR_DIALECT_SMT_IR_SMTDIALECT_H
#include "mlir/IR/BuiltinOps.h"
#include "mlir/IR/Dialect.h"
@@ -17,4 +17,4 @@
#include "mlir/Dialect/SMT/IR/SMTDialect.h.inc"
#include "mlir/Dialect/SMT/IR/SMTEnums.h.inc"
-#endif // MLIR_DIALECT_SMT_SMTDIALECT_H
+#endif // MLIR_DIALECT_SMT_IR_SMTDIALECT_H
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTDialect.td b/mlir/include/mlir/Dialect/SMT/IR/SMTDialect.td
index 4b74187e85b87..00f170659946e 100644
--- a/mlir/include/mlir/Dialect/SMT/IR/SMTDialect.td
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTDialect.td
@@ -6,8 +6,8 @@
//
//===----------------------------------------------------------------------===//
-#ifndef MLIR_DIALECT_SMT_SMTDIALECT_TD
-#define MLIR_DIALECT_SMT_SMTDIALECT_TD
+#ifndef MLIR_DIALECT_SMT_IR_SMTDIALECT_TD
+#define MLIR_DIALECT_SMT_IR_SMTDIALECT_TD
include "mlir/IR/DialectBase.td"
@@ -27,4 +27,4 @@ def SMTDialect : Dialect {
}];
}
-#endif // MLIR_DIALECT_SMT_SMTDIALECT_TD
+#endif // MLIR_DIALECT_SMT_IR_SMTDIALECT_TD
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTIntOps.td b/mlir/include/mlir/Dialect/SMT/IR/SMTIntOps.td
index c9b5d6bf5055a..ea94dfd8fbd2a 100644
--- a/mlir/include/mlir/Dialect/SMT/IR/SMTIntOps.td
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTIntOps.td
@@ -6,8 +6,8 @@
//
//===----------------------------------------------------------------------===//
-#ifndef MLIR_DIALECT_SMT_SMTINTOPS_TD
-#define MLIR_DIALECT_SMT_SMTINTOPS_TD
+#ifndef MLIR_DIALECT_SMT_IR_SMTINTOPS_TD
+#define MLIR_DIALECT_SMT_IR_SMTINTOPS_TD
include "mlir/Dialect/SMT/IR/SMTDialect.td"
include "mlir/Dialect/SMT/IR/SMTAttributes.td"
@@ -134,4 +134,4 @@ def Int2BVOp : SMTOp<"int2bv", [Pure]> {
let assemblyFormat = "$input attr-dict `:` qualified(type($result))";
}
-#endif // MLIR_DIALECT_SMT_SMTINTOPS_TD
+#endif // MLIR_DIALECT_SMT_IR_SMTINTOPS_TD
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTOps.h b/mlir/include/mlir/Dialect/SMT/IR/SMTOps.h
index 869ebdc93a395..1be7db605d911 100644
--- a/mlir/include/mlir/Dialect/SMT/IR/SMTOps.h
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTOps.h
@@ -7,7 +7,7 @@
//===----------------------------------------------------------------------===//
#ifndef MLIR_DIALECT_SMT_IR_SMTOPS_H
-#define MLIR_DIALECT_SMT_SMTOPS_H
+#define MLIR_DIALECT_SMT_IR_SMTOPS_H
#include "mlir/IR/OpImplementation.h"
#include "mlir/IR/SymbolTable.h"
@@ -22,4 +22,4 @@
#define GET_OP_CLASSES
#include "mlir/Dialect/SMT/IR/SMT.h.inc"
-#endif // MLIR_DIALECT_SMT_SMTOPS_H
+#endif // MLIR_DIALECT_SMT_IR_SMTOPS_H
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTOps.td b/mlir/include/mlir/Dialect/SMT/IR/SMTOps.td
index d606a78b3cef8..1872c00b74f1a 100644
--- a/mlir/include/mlir/Dialect/SMT/IR/SMTOps.td
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTOps.td
@@ -6,8 +6,8 @@
//
//===----------------------------------------------------------------------===//
-#ifndef MLIR_DIALECT_SMT_SMTOPS_TD
-#define MLIR_DIALECT_SMT_SMTOPS_TD
+#ifndef MLIR_DIALECT_SMT_IR_SMTOPS_TD
+#define MLIR_DIALECT_SMT_IR_SMTOPS_TD
include "mlir/Dialect/SMT/IR/SMTDialect.td"
include "mlir/Dialect/SMT/IR/SMTAttributes.td"
@@ -472,4 +472,4 @@ class QuantifierOp<string mnemonic> : SMTOp<mnemonic, [
def ForallOp : QuantifierOp<"forall"> { let summary = "forall quantifier"; }
def ExistsOp : QuantifierOp<"exists"> { let summary = "exists quantifier"; }
-#endif // MLIR_DIALECT_SMT_SMTOPS_TD
+#endif // MLIR_DIALECT_SMT_IR_SMTOPS_TD
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTTypes.h b/mlir/include/mlir/Dialect/SMT/IR/SMTTypes.h
index 4db28f7a07a41..7e50c8bb51f72 100644
--- a/mlir/include/mlir/Dialect/SMT/IR/SMTTypes.h
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTTypes.h
@@ -6,8 +6,8 @@
//
//===----------------------------------------------------------------------===//
-#ifndef MLIR_DIALECT_SMT_SMTTYPES_H
-#define MLIR_DIALECT_SMT_SMTTYPES_H
+#ifndef MLIR_DIALECT_SMT_IR_SMTTYPES_H
+#define MLIR_DIALECT_SMT_IR_SMTTYPES_H
#include "mlir/IR/BuiltinTypes.h"
#include "mlir/IR/Types.h"
@@ -27,4 +27,4 @@ bool isAnyNonFuncSMTValueType(mlir::Type type);
} // namespace smt
} // namespace mlir
-#endif // MLIR_DIALECT_SMT_SMTTYPES_H
+#endif // MLIR_DIALECT_SMT_IR_SMTTYPES_H
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTTypes.td b/mlir/include/mlir/Dialect/SMT/IR/SMTTypes.td
index f17a1a0e6fa1b..19fee9756e5f5 100644
--- a/mlir/include/mlir/Dialect/SMT/IR/SMTTypes.td
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTTypes.td
@@ -6,8 +6,8 @@
//
//===----------------------------------------------------------------------===//
-#ifndef MLIR_DIALECT_SMT_SMTTYPES_TD
-#define MLIR_DIALECT_SMT_SMTTYPES_TD
+#ifndef MLIR_DIALECT_SMT_IR_SMTTYPES_TD
+#define MLIR_DIALECT_SMT_IR_SMTTYPES_TD
include "mlir/Dialect/SMT/IR/SMTDialect.td"
include "mlir/IR/AttrTypeBase.td"
@@ -142,4 +142,4 @@ 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
+#endif // MLIR_DIALECT_SMT_IR_SMTTYPES_TD
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTVisitors.h b/mlir/include/mlir/Dialect/SMT/IR/SMTVisitors.h
index 38fad21019158..e6b1fe8e71a20 100644
--- a/mlir/include/mlir/Dialect/SMT/IR/SMTVisitors.h
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTVisitors.h
@@ -10,8 +10,8 @@
//
//===----------------------------------------------------------------------===//
-#ifndef MLIR_DIALECT_SMT_SMTVISITORS_H
-#define MLIR_DIALECT_SMT_SMTVISITORS_H
+#ifndef MLIR_DIALECT_SMT_IR_SMTVISITORS_H
+#define MLIR_DIALECT_SMT_IR_SMTVISITORS_H
#include "mlir/Dialect/SMT/IR/SMTOps.h"
#include "llvm/ADT/TypeSwitch.h"
@@ -198,4 +198,4 @@ class SMTTypeVisitor {
} // namespace smt
} // namespace mlir
-#endif // MLIR_DIALECT_SMT_SMTVISITORS_H
+#endif // MLIR_DIALECT_SMT_IR_SMTVISITORS_H
>From 040695c62c3b5a643dd40eef7fd0c03bb26ad3af Mon Sep 17 00:00:00 2001
From: Maksim Levental <maksim.levental at gmail.com>
Date: Wed, 9 Apr 2025 19:27:54 -0400
Subject: [PATCH 7/7] verify roundtrip
---
mlir/test/Dialect/SMT/array.mlir | 2 +-
mlir/test/Dialect/SMT/basic.mlir | 2 +-
mlir/test/Dialect/SMT/bitvectors.mlir | 2 +-
mlir/test/Dialect/SMT/integers.mlir | 2 +-
4 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/mlir/test/Dialect/SMT/array.mlir b/mlir/test/Dialect/SMT/array.mlir
index 89cb45c5e878a..bbfe58cac1bfa 100644
--- a/mlir/test/Dialect/SMT/array.mlir
+++ b/mlir/test/Dialect/SMT/array.mlir
@@ -1,4 +1,4 @@
-// RUN: mlir-opt %s | mlir-opt | FileCheck %s
+// RUN: mlir-opt %s --verify-roundtrip | FileCheck %s
// CHECK-LABEL: func @arrayOperations
// CHECK-SAME: ([[A0:%.+]]: !smt.bool)
diff --git a/mlir/test/Dialect/SMT/basic.mlir b/mlir/test/Dialect/SMT/basic.mlir
index a4975d66e9769..44bf0d6faa00d 100644
--- a/mlir/test/Dialect/SMT/basic.mlir
+++ b/mlir/test/Dialect/SMT/basic.mlir
@@ -1,4 +1,4 @@
-// RUN: mlir-opt %s | mlir-opt | FileCheck %s
+// RUN: mlir-opt %s --verify-roundtrip | 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>)
diff --git a/mlir/test/Dialect/SMT/bitvectors.mlir b/mlir/test/Dialect/SMT/bitvectors.mlir
index 2482f55b5ed31..c6b8fb097404b 100644
--- a/mlir/test/Dialect/SMT/bitvectors.mlir
+++ b/mlir/test/Dialect/SMT/bitvectors.mlir
@@ -1,4 +1,4 @@
-// RUN: mlir-opt %s | mlir-opt | FileCheck %s
+// RUN: mlir-opt %s --verify-roundtrip | FileCheck %s
// CHECK-LABEL: func @bitvectors
func.func @bitvectors() {
diff --git a/mlir/test/Dialect/SMT/integers.mlir b/mlir/test/Dialect/SMT/integers.mlir
index f5133c8c72b5d..8e1a355278eb0 100644
--- a/mlir/test/Dialect/SMT/integers.mlir
+++ b/mlir/test/Dialect/SMT/integers.mlir
@@ -1,4 +1,4 @@
-// RUN: mlir-opt %s | mlir-opt | FileCheck %s
+// RUN: mlir-opt %s --verify-roundtrip | FileCheck %s
// CHECK-LABEL: func @integer_operations
func.func @integer_operations() {
More information about the Mlir-commits
mailing list