[mlir][SMT] upstream SMT dialect

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)

mlir/include/mlir/Dialect/SMT/CMakeLists.txt

@@ -0,0 +1 @@
+add_subdirectory(IR)

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)

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_IR_SMT_TD
+#define MLIR_DIALECT_SMT_IR_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_IR_SMT_TD

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_IR_SMTARRAYOPS_TD
+#define MLIR_DIALECT_SMT_IR_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.7.
+  }];
+
+  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.7.
+  }];
+
+  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_IR_SMTARRAYOPS_TD

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_IR_SMTATTRIBUTES_H
+#define MLIR_DIALECT_SMT_IR_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_IR_SMTATTRIBUTES_H

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_IR_SMTATTRIBUTES_TD
+#define MLIR_DIALECT_SMT_IR_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 non-negative
+    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_IR_SMTATTRIBUTES_TD