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

[llvmlistbot at llvm.org]

Author: Bea Healy
Date: 2026-04-28T10:27:30+01:00
New Revision: 3d1fa9ee9d95aca32e27a34e9916fc246f090543

URL: https://github.com/llvm/llvm-project/commit/3d1fa9ee9d95aca32e27a34e9916fc246f090543
DIFF: https://github.com/llvm/llvm-project/commit/3d1fa9ee9d95aca32e27a34e9916fc246f090543.diff

LOG: [mlir][smt] Allow empty function domains (#193732)

Added: 
    

Modified: 
    mlir/include/mlir/Dialect/SMT/IR/SMTTypes.td
    mlir/lib/Dialect/SMT/IR/SMTTypes.cpp
    mlir/test/Dialect/SMT/basic.mlir
    mlir/unittests/Dialect/SMT/CMakeLists.txt

Removed: 
    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