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

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

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))

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
 }
 

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

mlir/unittests/Dialect/SMT/TypeTest.cpp

@@ -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