[Mlir-commits] [mlir] [mlir][SMT] upstream `SMT` dialect (PR #131480)

[Maksim Levental]

================
@@ -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.
+
----------------
makslevental wrote:

add `non-negative`

https://github.com/llvm/llvm-project/pull/131480