Allow to synthesize refinements

Author: math-fehr

mlir-fuzz

@@ -1,14 +1,7 @@
 irdl.dialect @arith {
   irdl.operation @addi {
     %integer = irdl.base "!builtin.integer"
-    %ovf_none = irdl.is #arith.overflow<none>
-    %ovf_nsw = irdl.is #arith.overflow<nsw>
-    %ovf_nuw = irdl.is #arith.overflow<nuw>
-    %ovf_nsw_nuw = irdl.is #arith.overflow<nsw,nuw>
-    %ovf = irdl.any_of(%ovf_none, %ovf_nsw, %ovf_nuw, %ovf_nsw_nuw)
-
     irdl.operands(operand0: %integer, operand1: %integer)
     irdl.results(result0: %integer)
-    irdl.attributes {"overflowFlags" = %ovf}
   }
 }

tests/filecheck/superoptimize/arith.irdl

@@ -0,0 +1,11 @@
+// RUN: superoptimize %s --max-num-ops=1 --dialect=%S/arith.irdl | filecheck %s
+
+func.func @foo(%x: !smt.bv<32>, %y: !smt.bv<32>) -> !smt.bv<32> {
+  %r = "smt.bv.add"(%x, %y) : (!smt.bv<32>, !smt.bv<32>) -> !smt.bv<32>
+  func.return %r : !smt.bv<32>
+}
+
+// CHECK:       func.func @foo(%arg0 : i32) -> i32 {
+// CHECK-NEXT:    %0 = arith.constant 0 : i32
+// CHECK-NEXT:    func.return %0 : i32
+// CHECK-NEXT:  }

tests/filecheck/superoptimize/smt-to-arith.mlir

@@ -55,6 +55,7 @@ def register_all_arguments(arg_parser: argparse.ArgumentParser):
         "--dialect",
         type=str,
         help="The IRDL file defining the dialect we want to use for synthesis",
+        required=True,
     )
     arg_parser.add_argument(
         "-v",
@@ -63,6 +64,19 @@ def register_all_arguments(arg_parser: argparse.ArgumentParser):
         help="Print debugging information in stderr",
         action="store_true",
     )
+    arg_parser.add_argument(
+        "--configuration",
+        dest="configuration",
+        type=str,
+        help="The configuration to use for synthesis",
+        default="arith",
+    )
+    arg_parser.add_argument(
+        "--optimize",
+        dest="optimize",
+        help="Only generate programs with a lower cost than the input program",
+        action="store_true",
+    )
 
 
 def replace_synth_with_constants(
@@ -105,8 +119,9 @@ def main() -> None:
             f"--max-num-ops={args.max_num_ops}",
             "--pause-between-programs",
             "--mlir-print-op-generic",
-            "--configuration=arith",
+            f"--configuration={args.configuration}",
             f"--use-input-ops={args.use_input_ops}",
+            # "--optimize" if args.optimize is not None else "",
         ],
         stdin=sp.PIPE,
         stdout=sp.PIPE,