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-exception
6//
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_LIST
22#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.constant
29 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 builder.create<BVConstantOp>(loc, attrValue);
34 }
35 }
36
37 // BoolType constants can materialize into smt.constant
38 if (auto boolType = dyn_cast<BoolType>(type)) {
39 if (auto attrValue = dyn_cast<BoolAttr>(value))
40 return builder.create<BoolConstantOp>(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

source code of mlir/lib/Dialect/SMT/IR/SMTDialect.cpp