[Mlir-commits] [mlir] [mlir][smt] Allow empty function domains (PR #193732)

[Bea Healy]

https://github.com/TaoBi22 created https://github.com/llvm/llvm-project/pull/193732

Currently the SMT dialect doesn't allow SMT functions with an empty domain. Not sure if the intention behind this was because it makes the parsing/printing a little more complex or because it's semantically equivalent to declaring a const, but since it's legal SMTLIB it would be nice to allow it (especially since declare-const isn't actually part of the SMTLIB 2.0 spec, just Z3 syntactic sugar). 

>From c670d10a2793131bec4523a16301fb93d4531a00 Mon Sep 17 00:00:00 2001
From: Bea Healy <beahealy22 at gmail.com>
Date: Thu, 23 Apr 2026 14:07:47 +0100
Subject: [PATCH] [mlir][smt] Allow empty function domains

---
 mlir/include/mlir/Dialect/SMT/IR/SMTTypes.td |  5 +---
 mlir/lib/Dialect/SMT/IR/SMTTypes.cpp         | 17 +++++++++--
 mlir/test/Dialect/SMT/basic.mlir             |  6 ++++
 mlir/unittests/Dialect/SMT/CMakeLists.txt    |  1 -
 mlir/unittests/Dialect/SMT/TypeTest.cpp      | 31 --------------------
 5 files changed, 22 insertions(+), 38 deletions(-)
 delete mode 100644 mlir/unittests/Dialect/SMT/TypeTest.cpp

diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTTypes.td b/mlir/include/mlir/Dialect/SMT/IR/SMTTypes.td
index 19fee9756e5f5..b22fb0a6e7234 100644
--- a/mlir/include/mlir/Dialect/SMT/IR/SMTTypes.td
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTTypes.td
@@ -82,10 +82,7 @@ def SMTFuncType : SMTTypeDef<"SMTFunc"> {
     "mlir::Type":$rangeType
   );
 
-  // Note: We are not printing the parentheses when no domain type is present
-  // because the default MLIR parser thinks it is a builtin function type
-  // otherwise.
-  let assemblyFormat = "`<` `(` $domainTypes `)` ` ` $rangeType `>`";
+  let assemblyFormat = "`<` custom<DomainTypes>($domainTypes) $rangeType `>`";
 
   let builders = [
     TypeBuilderWithInferredContext<(ins
diff --git a/mlir/lib/Dialect/SMT/IR/SMTTypes.cpp b/mlir/lib/Dialect/SMT/IR/SMTTypes.cpp
index 6188719bb1ab5..d9baef98aff37 100644
--- a/mlir/lib/Dialect/SMT/IR/SMTTypes.cpp
+++ b/mlir/lib/Dialect/SMT/IR/SMTTypes.cpp
@@ -16,6 +16,21 @@ using namespace mlir;
 using namespace smt;
 using namespace mlir;
 
+static mlir::ParseResult
+parseDomainTypes(mlir::AsmParser &parser,
+                 llvm::SmallVectorImpl<mlir::Type> &types) {
+  return parser.parseCommaSeparatedList(
+      mlir::AsmParser::Delimiter::Paren,
+      [&]() { return parser.parseType(types.emplace_back()); });
+}
+
+static void printDomainTypes(mlir::AsmPrinter &printer,
+                             llvm::ArrayRef<mlir::Type> types) {
+  printer << '(';
+  llvm::interleaveComma(types, printer);
+  printer << ')';
+}
+
 #define GET_TYPEDEF_CLASSES
 #include "mlir/Dialect/SMT/IR/SMTTypes.cpp.inc"
 
@@ -67,8 +82,6 @@ LogicalResult ArrayType::verify(function_ref<InFlightDiagnostic()> emitError,
 
 LogicalResult SMTFuncType::verify(function_ref<InFlightDiagnostic()> emitError,
                                   ArrayRef<Type> domainTypes, Type rangeType) {
-  if (domainTypes.empty())
-    return emitError() << "domain must not be empty";
   if (!llvm::all_of(domainTypes, isAnyNonFuncSMTValueType))
     return emitError() << "domain types must be any non-function SMT type";
   if (!isAnyNonFuncSMTValueType(rangeType))
diff --git a/mlir/test/Dialect/SMT/basic.mlir b/mlir/test/Dialect/SMT/basic.mlir
index 44bf0d6faa00d..38d8f4e8d7fb3 100644
--- a/mlir/test/Dialect/SMT/basic.mlir
+++ b/mlir/test/Dialect/SMT/basic.mlir
@@ -17,6 +17,9 @@ func.func @core(%in: i8) {
   %d = smt.declare_fun {smt.some_attr} : !smt.sort<"uninterpreted_sort">
   // CHECK: smt.declare_fun {smt.some_attr} : !smt.func<(!smt.int, !smt.bool) !smt.bool>
   %e = smt.declare_fun {smt.some_attr} : !smt.func<(!smt.int, !smt.bool) !smt.bool>
+  // CHECK: smt.declare_fun {smt.some_attr} : !smt.func<() !smt.bool>
+  %f = smt.declare_fun {smt.some_attr} : !smt.func<() !smt.bool>
+
 
   // CHECK: smt.constant true {smt.some_attr}
   %true = smt.constant true {smt.some_attr}
@@ -105,6 +108,9 @@ func.func @core(%in: i8) {
   // CHECK: smt.apply_func %{{.*}}(%{{.*}}, %{{.*}}) {smt.some_attr} : !smt.func<(!smt.int, !smt.bool) !smt.bool>
   %11 = smt.apply_func %e(%c, %a) {smt.some_attr} : !smt.func<(!smt.int, !smt.bool) !smt.bool>
 
+  // CHECK: smt.apply_func %{{.*}}() {smt.some_attr} : !smt.func<() !smt.bool>
+  %12 = smt.apply_func %f() {smt.some_attr} : !smt.func<() !smt.bool>
+
   return
 }
 
diff --git a/mlir/unittests/Dialect/SMT/CMakeLists.txt b/mlir/unittests/Dialect/SMT/CMakeLists.txt
index a1331467febaa..184e227c40327 100644
--- a/mlir/unittests/Dialect/SMT/CMakeLists.txt
+++ b/mlir/unittests/Dialect/SMT/CMakeLists.txt
@@ -1,7 +1,6 @@
 add_mlir_unittest(MLIRSMTTests
   AttributeTest.cpp
   QuantifierTest.cpp
-  TypeTest.cpp
 )
 
 mlir_target_link_libraries(MLIRSMTTests
diff --git a/mlir/unittests/Dialect/SMT/TypeTest.cpp b/mlir/unittests/Dialect/SMT/TypeTest.cpp
deleted file mode 100644
index f3b06cd0f84e0..0000000000000
--- a/mlir/unittests/Dialect/SMT/TypeTest.cpp
+++ /dev/null
@@ -1,31 +0,0 @@
-//===- TypeTest.cpp - SMT type unit tests ---------------------------------===//
-//
-// 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
-//
-//===----------------------------------------------------------------------===//
-
-#include "mlir/Dialect/SMT/IR/SMTDialect.h"
-#include "mlir/Dialect/SMT/IR/SMTTypes.h"
-#include "gtest/gtest.h"
-
-using namespace mlir;
-using namespace smt;
-
-namespace {
-
-TEST(SMTFuncTypeTest, NonEmptyDomain) {
-  MLIRContext context;
-  context.loadDialect<SMTDialect>();
-  Location loc(UnknownLoc::get(&context));
-
-  auto boolTy = BoolType::get(&context);
-  auto funcTy = SMTFuncType::getChecked(loc, ArrayRef<Type>{}, boolTy);
-  ASSERT_EQ(funcTy, Type());
-  context.getDiagEngine().registerHandler([&](Diagnostic &diag) {
-    ASSERT_STREQ(diag.str().c_str(), "domain must not be empty");
-  });
-}
-
-} // namespace