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

[Fehr Mathieu]

================
@@ -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
----------------
math-fehr wrote:

SMT-LIB 2.7 came out recently, and all these operators are unchanged.
Should we replace all 2.6 with 2.7?

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