using namespace mlir in CombToSMT.cpp

Author: makslevental

lib/Conversion/CombToSMT/CombToSMT.cpp

@@ -19,6 +19,7 @@ namespace circt {
 #include "circt/Conversion/Passes.h.inc"
 } // namespace circt
 
+using namespace mlir;
 using namespace circt;
 using namespace comb;
 
@@ -34,8 +35,8 @@ struct CombReplicateOpConversion : OpConversionPattern<ReplicateOp> {
   LogicalResult
   matchAndRewrite(ReplicateOp op, OpAdaptor adaptor,
                   ConversionPatternRewriter &rewriter) const override {
-    rewriter.replaceOpWithNewOp<mlir::smt::RepeatOp>(op, op.getMultiple(),
-                                                     adaptor.getInput());
+    rewriter.replaceOpWithNewOp<smt::RepeatOp>(op, op.getMultiple(),
+                                               adaptor.getInput());
     return success();
   }
 };
@@ -56,49 +57,49 @@ struct IcmpOpConversion : OpConversionPattern<ICmpOp> {
                                          "comparison predicate not supported");
 
     if (adaptor.getPredicate() == ICmpPredicate::eq) {
-      rewriter.replaceOpWithNewOp<mlir::smt::EqOp>(op, adaptor.getLhs(),
-                                                   adaptor.getRhs());
+      rewriter.replaceOpWithNewOp<smt::EqOp>(op, adaptor.getLhs(),
+                                             adaptor.getRhs());
       return success();
     }
 
     if (adaptor.getPredicate() == ICmpPredicate::ne) {
-      rewriter.replaceOpWithNewOp<mlir::smt::DistinctOp>(op, adaptor.getLhs(),
-                                                         adaptor.getRhs());
+      rewriter.replaceOpWithNewOp<smt::DistinctOp>(op, adaptor.getLhs(),
+                                                   adaptor.getRhs());
       return success();
     }
 
-    mlir::smt::BVCmpPredicate pred;
+    smt::BVCmpPredicate pred;
     switch (adaptor.getPredicate()) {
     case ICmpPredicate::sge:
-      pred = mlir::smt::BVCmpPredicate::sge;
+      pred = smt::BVCmpPredicate::sge;
       break;
     case ICmpPredicate::sgt:
-      pred = mlir::smt::BVCmpPredicate::sgt;
+      pred = smt::BVCmpPredicate::sgt;
       break;
     case ICmpPredicate::sle:
-      pred = mlir::smt::BVCmpPredicate::sle;
+      pred = smt::BVCmpPredicate::sle;
       break;
     case ICmpPredicate::slt:
-      pred = mlir::smt::BVCmpPredicate::slt;
+      pred = smt::BVCmpPredicate::slt;
       break;
     case ICmpPredicate::uge:
-      pred = mlir::smt::BVCmpPredicate::uge;
+      pred = smt::BVCmpPredicate::uge;
       break;
     case ICmpPredicate::ugt:
-      pred = mlir::smt::BVCmpPredicate::ugt;
+      pred = smt::BVCmpPredicate::ugt;
       break;
     case ICmpPredicate::ule:
-      pred = mlir::smt::BVCmpPredicate::ule;
+      pred = smt::BVCmpPredicate::ule;
       break;
     case ICmpPredicate::ult:
-      pred = mlir::smt::BVCmpPredicate::ult;
+      pred = smt::BVCmpPredicate::ult;
       break;
     default:
       llvm_unreachable("all cases handled above");
     }
 
-    rewriter.replaceOpWithNewOp<mlir::smt::BVCmpOp>(op, pred, adaptor.getLhs(),
-                                                    adaptor.getRhs());
+    rewriter.replaceOpWithNewOp<smt::BVCmpOp>(op, pred, adaptor.getLhs(),
+                                              adaptor.getRhs());
     return success();
   }
 };
@@ -111,7 +112,7 @@ struct ExtractOpConversion : OpConversionPattern<ExtractOp> {
   matchAndRewrite(ExtractOp op, OpAdaptor adaptor,
                   ConversionPatternRewriter &rewriter) const override {
 
-    rewriter.replaceOpWithNewOp<mlir::smt::ExtractOp>(
+    rewriter.replaceOpWithNewOp<smt::ExtractOp>(
         op, typeConverter->convertType(op.getResult().getType()),
         adaptor.getLowBitAttr(), adaptor.getInput());
     return success();
@@ -126,9 +127,9 @@ struct MuxOpConversion : OpConversionPattern<MuxOp> {
   matchAndRewrite(MuxOp op, OpAdaptor adaptor,
                   ConversionPatternRewriter &rewriter) const override {
     Value condition = typeConverter->materializeTargetConversion(
-        rewriter, op.getLoc(), mlir::smt::BoolType::get(getContext()),
+        rewriter, op.getLoc(), smt::BoolType::get(getContext()),
         adaptor.getCond());
-    rewriter.replaceOpWithNewOp<mlir::smt::IteOp>(
+    rewriter.replaceOpWithNewOp<smt::IteOp>(
         op, condition, adaptor.getTrueValue(), adaptor.getFalseValue());
     return success();
   }
@@ -141,10 +142,8 @@ struct SubOpConversion : OpConversionPattern<SubOp> {
   LogicalResult
   matchAndRewrite(SubOp op, OpAdaptor adaptor,
                   ConversionPatternRewriter &rewriter) const override {
-    Value negRhs =
-        rewriter.create<mlir::smt::BVNegOp>(op.getLoc(), adaptor.getRhs());
-    rewriter.replaceOpWithNewOp<mlir::smt::BVAddOp>(op, adaptor.getLhs(),
-                                                    negRhs);
+    Value negRhs = rewriter.create<smt::BVNegOp>(op.getLoc(), adaptor.getRhs());
+    rewriter.replaceOpWithNewOp<smt::BVAddOp>(op, adaptor.getLhs(), negRhs);
     return success();
   }
 };
@@ -158,17 +157,17 @@ struct ParityOpConversion : OpConversionPattern<ParityOp> {
                   ConversionPatternRewriter &rewriter) const override {
     Location loc = op.getLoc();
     unsigned bitwidth =
-        cast<mlir::smt::BitVectorType>(adaptor.getInput().getType()).getWidth();
+        cast<smt::BitVectorType>(adaptor.getInput().getType()).getWidth();
 
     // Note: the SMT bitvector type does not support 0 bitwidth vectors and thus
     // the type conversion should already fail.
-    Type oneBitTy = mlir::smt::BitVectorType::get(getContext(), 1);
-    Value runner = rewriter.create<mlir::smt::ExtractOp>(loc, oneBitTy, 0,
-                                                         adaptor.getInput());
+    Type oneBitTy = smt::BitVectorType::get(getContext(), 1);
+    Value runner =
+        rewriter.create<smt::ExtractOp>(loc, oneBitTy, 0, adaptor.getInput());
     for (unsigned i = 1; i < bitwidth; ++i) {
-      Value ext = rewriter.create<mlir::smt::ExtractOp>(loc, oneBitTy, i,
-                                                        adaptor.getInput());
-      runner = rewriter.create<mlir::smt::BVXOrOp>(loc, runner, ext);
+      Value ext =
+          rewriter.create<smt::ExtractOp>(loc, oneBitTy, i, adaptor.getInput());
+      runner = rewriter.create<smt::BVXOrOp>(loc, runner, ext);
     }
 
     rewriter.replaceOp(op, runner);
@@ -206,22 +205,19 @@ struct DivisionOpConversion : OpConversionPattern<SourceOp> {
   matchAndRewrite(SourceOp op, OpAdaptor adaptor,
                   ConversionPatternRewriter &rewriter) const override {
     Location loc = op.getLoc();
-    auto type = dyn_cast<mlir::smt::BitVectorType>(adaptor.getRhs().getType());
+    auto type = dyn_cast<smt::BitVectorType>(adaptor.getRhs().getType());
     if (!type)
       return failure();
 
     auto resultType = OpConversionPattern<SourceOp>::typeConverter->convertType(
         op.getResult().getType());
-    Value zero = rewriter.create<mlir::smt::BVConstantOp>(
-        loc, APInt(type.getWidth(), 0));
-    Value isZero =
-        rewriter.create<mlir::smt::EqOp>(loc, adaptor.getRhs(), zero);
-    Value symbolicVal =
-        rewriter.create<mlir::smt::DeclareFunOp>(loc, resultType);
+    Value zero =
+        rewriter.create<smt::BVConstantOp>(loc, APInt(type.getWidth(), 0));
+    Value isZero = rewriter.create<smt::EqOp>(loc, adaptor.getRhs(), zero);
+    Value symbolicVal = rewriter.create<smt::DeclareFunOp>(loc, resultType);
     Value division =
         rewriter.create<TargetOp>(loc, resultType, adaptor.getOperands());
-    rewriter.replaceOpWithNewOp<mlir::smt::IteOp>(op, isZero, symbolicVal,
-                                                  division);
+    rewriter.replaceOpWithNewOp<smt::IteOp>(op, isZero, symbolicVal, division);
     return success();
   }
 };
@@ -267,19 +263,19 @@ void circt::populateCombToSMTConversionPatterns(TypeConverter &converter,
                                                 RewritePatternSet &patterns) {
   patterns.add<CombReplicateOpConversion, IcmpOpConversion, ExtractOpConversion,
                SubOpConversion, MuxOpConversion, ParityOpConversion,
-               OneToOneOpConversion<ShlOp, mlir::smt::BVShlOp>,
-               OneToOneOpConversion<ShrUOp, mlir::smt::BVLShrOp>,
-               OneToOneOpConversion<ShrSOp, mlir::smt::BVAShrOp>,
-               DivisionOpConversion<DivSOp, mlir::smt::BVSDivOp>,
-               DivisionOpConversion<DivUOp, mlir::smt::BVUDivOp>,
-               DivisionOpConversion<ModSOp, mlir::smt::BVSRemOp>,
-               DivisionOpConversion<ModUOp, mlir::smt::BVURemOp>,
-               VariadicToBinaryOpConversion<ConcatOp, mlir::smt::ConcatOp>,
-               VariadicToBinaryOpConversion<AddOp, mlir::smt::BVAddOp>,
-               VariadicToBinaryOpConversion<MulOp, mlir::smt::BVMulOp>,
-               VariadicToBinaryOpConversion<AndOp, mlir::smt::BVAndOp>,
-               VariadicToBinaryOpConversion<OrOp, mlir::smt::BVOrOp>,
-               VariadicToBinaryOpConversion<XorOp, mlir::smt::BVXOrOp>>(
+               OneToOneOpConversion<ShlOp, smt::BVShlOp>,
+               OneToOneOpConversion<ShrUOp, smt::BVLShrOp>,
+               OneToOneOpConversion<ShrSOp, smt::BVAShrOp>,
+               DivisionOpConversion<DivSOp, smt::BVSDivOp>,
+               DivisionOpConversion<DivUOp, smt::BVUDivOp>,
+               DivisionOpConversion<ModSOp, smt::BVSRemOp>,
+               DivisionOpConversion<ModUOp, smt::BVURemOp>,
+               VariadicToBinaryOpConversion<ConcatOp, smt::ConcatOp>,
+               VariadicToBinaryOpConversion<AddOp, smt::BVAddOp>,
+               VariadicToBinaryOpConversion<MulOp, smt::BVMulOp>,
+               VariadicToBinaryOpConversion<AndOp, smt::BVAndOp>,
+               VariadicToBinaryOpConversion<OrOp, smt::BVOrOp>,
+               VariadicToBinaryOpConversion<XorOp, smt::BVXOrOp>>(
       converter, patterns.getContext());
 
   // TODO: there are two unsupported operations in the comb dialect: 'parity'
@@ -289,7 +285,7 @@ void circt::populateCombToSMTConversionPatterns(TypeConverter &converter,
 void ConvertCombToSMTPass::runOnOperation() {
   ConversionTarget target(getContext());
   target.addIllegalDialect<comb::CombDialect>();
-  target.addLegalDialect<mlir::smt::SMTDialect>();
+  target.addLegalDialect<smt::SMTDialect>();
 
   RewritePatternSet patterns(&getContext());
   TypeConverter converter;