1//===- SMTTypes.cpp -------------------------------------------------------===//
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/SMTTypes.h"
10#include "mlir/Dialect/SMT/IR/SMTDialect.h"
11#include "mlir/IR/Builders.h"
12#include "mlir/IR/DialectImplementation.h"
13#include "llvm/ADT/TypeSwitch.h"
14
15using namespace mlir;
16using namespace smt;
17using namespace mlir;
18
19#define GET_TYPEDEF_CLASSES
20#include "mlir/Dialect/SMT/IR/SMTTypes.cpp.inc"
21
22void SMTDialect::registerTypes() {
23 addTypes<
24#define GET_TYPEDEF_LIST
25#include "mlir/Dialect/SMT/IR/SMTTypes.cpp.inc"
26 >();
27}
28
29bool smt::isAnyNonFuncSMTValueType(Type type) {
30 return isAnySMTValueType(type) && !isa<SMTFuncType>(type);
31}
32
33bool smt::isAnySMTValueType(Type type) {
34 return isa<BoolType, BitVectorType, ArrayType, IntType, SortType,
35 SMTFuncType>(type);
36}
37
38//===----------------------------------------------------------------------===//
39// BitVectorType
40//===----------------------------------------------------------------------===//
41
42LogicalResult
43BitVectorType::verify(function_ref<InFlightDiagnostic()> emitError,
44 int64_t width) {
45 if (width <= 0U)
46 return emitError() << "bit-vector must have at least a width of one";
47 return success();
48}
49
50//===----------------------------------------------------------------------===//
51// ArrayType
52//===----------------------------------------------------------------------===//
53
54LogicalResult ArrayType::verify(function_ref<InFlightDiagnostic()> emitError,
55 Type domainType, Type rangeType) {
56 if (!isAnySMTValueType(domainType))
57 return emitError() << "domain must be any SMT value type";
58 if (!isAnySMTValueType(rangeType))
59 return emitError() << "range must be any SMT value type";
60
61 return success();
62}
63
64//===----------------------------------------------------------------------===//
65// SMTFuncType
66//===----------------------------------------------------------------------===//
67
68LogicalResult SMTFuncType::verify(function_ref<InFlightDiagnostic()> emitError,
69 ArrayRef<Type> domainTypes, Type rangeType) {
70 if (domainTypes.empty())
71 return emitError() << "domain must not be empty";
72 if (!llvm::all_of(domainTypes, isAnyNonFuncSMTValueType))
73 return emitError() << "domain types must be any non-function SMT type";
74 if (!isAnyNonFuncSMTValueType(rangeType))
75 return emitError() << "range type must be any non-function SMT type";
76
77 return success();
78}
79
80//===----------------------------------------------------------------------===//
81// SortType
82//===----------------------------------------------------------------------===//
83
84LogicalResult SortType::verify(function_ref<InFlightDiagnostic()> emitError,
85 StringAttr identifier,
86 ArrayRef<Type> sortParams) {
87 if (!llvm::all_of(sortParams, isAnyNonFuncSMTValueType))
88 return emitError()
89 << "sort parameter types must be any non-function SMT type";
90
91 return success();
92}
93

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