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

[Martin Erhart]

================
@@ -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";
----------------
maerhart wrote:

My understanding is that `declare-const` is just syntactic sugar for `declare-fun` for 0-ary functions. I think it wasn't even part of v2.0 and only added later for that purpose.

I don't really see a benefit in having two separate ops for that in an IR.
* it makes iterating over/pattern matching on symbolic values more annoying because now you would need to consider 2 ops instead of 1,
* when declaring symbolic values for values you'd need to check if they map to a constant to build the right op whereas otherwise you could just get the target type from the type converter and build the op directly,
* you'd end up being able to declare constants in two ways (declare-const and 0-ary function via declare-fun) but for an IR it's usually better to have a single canonical form (currently you can also declare them with the plain type and a 0-ary function though, so we already have a bit of syntactic sugar)

It's not complicated to pattern match on declare-fun ops that can be represented as declare-const and just emit/lower them like that in the backend.

Regarding the naming, `declare_fun` and `declare` both sound fine to me. I think `declare` is probably slightly better, but whatever you prefer.

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