48 lines · cpp
1//===- SMTDialect.cpp - SMT dialect implementation ------------------------===//2//3// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.4// See https://llvm.org/LICENSE.txt for license information.5// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception6//7//===----------------------------------------------------------------------===//8 9#include "mlir/Dialect/SMT/IR/SMTDialect.h"10#include "mlir/Dialect/SMT/IR/SMTAttributes.h"11#include "mlir/Dialect/SMT/IR/SMTOps.h"12#include "mlir/Dialect/SMT/IR/SMTTypes.h"13 14using namespace mlir;15using namespace smt;16 17void SMTDialect::initialize() {18 registerAttributes();19 registerTypes();20 addOperations<21#define GET_OP_LIST22#include "mlir/Dialect/SMT/IR/SMT.cpp.inc"23 >();24}25 26Operation *SMTDialect::materializeConstant(OpBuilder &builder, Attribute value,27 Type type, Location loc) {28 // BitVectorType constants can materialize into smt.bv.constant29 if (auto bvType = dyn_cast<BitVectorType>(type)) {30 if (auto attrValue = dyn_cast<BitVectorAttr>(value)) {31 assert(bvType == attrValue.getType() &&32 "attribute and desired result types have to match");33 return BVConstantOp::create(builder, loc, attrValue);34 }35 }36 37 // BoolType constants can materialize into smt.constant38 if (auto boolType = dyn_cast<BoolType>(type)) {39 if (auto attrValue = dyn_cast<BoolAttr>(value))40 return BoolConstantOp::create(builder, loc, attrValue);41 }42 43 return nullptr;44}45 46#include "mlir/Dialect/SMT/IR/SMTDialect.cpp.inc"47#include "mlir/Dialect/SMT/IR/SMTEnums.cpp.inc"48