[mlir][SMT] remove custom forall/exists builder because of asan memory leak

Author: makslevental

mlir/include/mlir/Dialect/SMT/IR/SMTOps.td

@@ -448,18 +448,6 @@ class QuantifierOp<string mnemonic> : SMTOp<mnemonic, [
                         VariadicRegion<SizedRegion<1>>:$patterns);
   let results = (outs BoolType:$result);
 
-  let builders = [
-    OpBuilder<(ins
-      "TypeRange":$boundVarTypes,
-      "function_ref<Value(OpBuilder &, Location, ValueRange)>":$bodyBuilder,
-      CArg<"std::optional<ArrayRef<StringRef>>", "std::nullopt">:$boundVarNames,
-      CArg<"function_ref<ValueRange(OpBuilder &, Location, ValueRange)>",
-           "{}">:$patternBuilder,
-      CArg<"uint32_t", "0">:$weight,
-      CArg<"bool", "false">:$noPattern)>
-  ];
-  let skipDefaultBuilders = true;
-
   let assemblyFormat = [{
     ($boundVarNames^)? (`no_pattern` $noPattern^)? (`weight` $weight^)?
     attr-dict-with-keyword $body (`patterns` $patterns^)?

mlir/lib/Dialect/SMT/IR/SMTOps.cpp

@@ -432,16 +432,6 @@ LogicalResult ForallOp::verifyRegions() {
   return verifyQuantifierRegions(*this);
 }
 
-void ForallOp::build(
-    OpBuilder &odsBuilder, OperationState &odsState, TypeRange boundVarTypes,
-    function_ref<Value(OpBuilder &, Location, ValueRange)> bodyBuilder,
-    std::optional<ArrayRef<StringRef>> boundVarNames,
-    function_ref<ValueRange(OpBuilder &, Location, ValueRange)> patternBuilder,
-    uint32_t weight, bool noPattern) {
-  buildQuantifier<Properties>(odsBuilder, odsState, boundVarTypes, bodyBuilder,
-                              boundVarNames, patternBuilder, weight, noPattern);
-}
-
 //===----------------------------------------------------------------------===//
 // ExistsOp
 //===----------------------------------------------------------------------===//
@@ -458,15 +448,5 @@ LogicalResult ExistsOp::verifyRegions() {
   return verifyQuantifierRegions(*this);
 }
 
-void ExistsOp::build(
-    OpBuilder &odsBuilder, OperationState &odsState, TypeRange boundVarTypes,
-    function_ref<Value(OpBuilder &, Location, ValueRange)> bodyBuilder,
-    std::optional<ArrayRef<StringRef>> boundVarNames,
-    function_ref<ValueRange(OpBuilder &, Location, ValueRange)> patternBuilder,
-    uint32_t weight, bool noPattern) {
-  buildQuantifier<Properties>(odsBuilder, odsState, boundVarTypes, bodyBuilder,
-                              boundVarNames, patternBuilder, weight, noPattern);
-}
-
 #define GET_OP_CLASSES
 #include "mlir/Dialect/SMT/IR/SMT.cpp.inc"

mlir/unittests/Dialect/SMT/CMakeLists.txt

@@ -1,6 +1,5 @@
 add_mlir_unittest(MLIRSMTTests
   AttributeTest.cpp
-  QuantifierTest.cpp
   TypeTest.cpp
 )