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

[Fehr Mathieu]

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

```suggestion
    `declare-fun` statements in SMT-LIB 2.6. The result type determines the SMT
```

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