[mlir][smt] add arith-to-smt

Author: makslevental

mlir/include/mlir/Conversion/ArithToSMT/ArithToSMT.h

@@ -0,0 +1,30 @@
+//===- ArithToSMT.h - Arith to SMT dialect conversion ---------*- C++ -*-===//
+//
+// 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
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef MLIR_CONVERSION_ARITHTOSMT_H
+#define MLIR_CONVERSION_ARITHTOSMT_H
+
+#include "mlir/Pass/Pass.h"
+#include <memory>
+
+namespace mlir {
+
+class TypeConverter;
+class RewritePatternSet;
+
+#define GEN_PASS_DECL_CONVERTARITHTOSMT
+#include "mlir/Conversion/Passes.h.inc"
+
+namespace arith {
+/// Get the Arith to SMT conversion patterns.
+void populateArithToSMTConversionPatterns(TypeConverter &converter,
+                                          RewritePatternSet &patterns);
+} // namespace arith
+} // namespace mlir
+
+#endif // MLIR_CONVERSION_ARITHTOSMT_H

mlir/include/mlir/Conversion/Passes.h

@@ -15,6 +15,7 @@
 #include "mlir/Conversion/ArithToArmSME/ArithToArmSME.h"
 #include "mlir/Conversion/ArithToEmitC/ArithToEmitCPass.h"
 #include "mlir/Conversion/ArithToLLVM/ArithToLLVM.h"
+#include "mlir/Conversion/ArithToSMT/ArithToSMT.h"
 #include "mlir/Conversion/ArithToSPIRV/ArithToSPIRV.h"
 #include "mlir/Conversion/ArmNeon2dToIntr/ArmNeon2dToIntr.h"
 #include "mlir/Conversion/ArmSMEToLLVM/ArmSMEToLLVM.h"

mlir/include/mlir/Conversion/Passes.td

@@ -1493,4 +1493,17 @@ def ConvertVectorToXeGPU : Pass<"convert-vector-to-xegpu"> {
   ];
 }
 
+//===----------------------------------------------------------------------===//
+// ConvertArithToSMT
+//===----------------------------------------------------------------------===//
+
+def ConvertArithToSMT : Pass<"convert-arith-to-smt"> {
+  let summary = "Convert arith ops and constants to SMT ops";
+  let dependentDialects = [
+    "smt::SMTDialect",
+    "arith::ArithDialect",
+    "mlir::func::FuncDialect"
+  ];
+}
+
 #endif // MLIR_CONVERSION_PASSES

mlir/include/mlir/InitAllPasses.h

@@ -95,6 +95,7 @@ inline void registerAllPasses() {
   arm_sve::registerArmSVEPasses();
   emitc::registerEmitCPasses();
   xegpu::registerXeGPUPasses();
+  registerConvertArithToSMTPass();
 
   // Dialect pipelines
   bufferization::registerBufferizationPipelines();