1//===- QuantifierTest.cpp - SMT quantifier operation unit tests -----------===//
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/SMTOps.h"
10#include "gtest/gtest.h"
11
12using namespace mlir;
13using namespace smt;
14
15namespace {
16
17//===----------------------------------------------------------------------===//
18// Test custom builders of ExistsOp
19//===----------------------------------------------------------------------===//
20
21TEST(QuantifierTest, ExistsBuilderWithPattern) {
22 MLIRContext context;
23 context.loadDialect<SMTDialect>();
24 Location loc(UnknownLoc::get(&context));
25
26 OpBuilder builder(&context);
27 auto boolTy = BoolType::get(&context);
28
29 OwningOpRef<ExistsOp> existsOp = builder.create<ExistsOp>(
30 loc, TypeRange{boolTy, boolTy},
31 [](OpBuilder &builder, Location loc, ValueRange boundVars) {
32 return builder.create<AndOp>(loc, boundVars);
33 },
34 std::nullopt,
35 [](OpBuilder &builder, Location loc, ValueRange boundVars) {
36 return boundVars;
37 },
38 /*weight=*/2);
39
40 SmallVector<char, 1024> buffer;
41 llvm::raw_svector_ostream stream(buffer);
42 existsOp->print(stream);
43
44 ASSERT_STREQ(
45 stream.str().str().c_str(),
46 "%0 = smt.exists weight 2 {\n^bb0(%arg0: !smt.bool, "
47 "%arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n smt.yield %0 : "
48 "!smt.bool\n} patterns {\n^bb0(%arg0: !smt.bool, %arg1: !smt.bool):\n "
49 "smt.yield %arg0, %arg1 : !smt.bool, !smt.bool\n}\n");
50}
51
52TEST(QuantifierTest, ExistsBuilderNoPattern) {
53 MLIRContext context;
54 context.loadDialect<SMTDialect>();
55 Location loc(UnknownLoc::get(&context));
56
57 OpBuilder builder(&context);
58 auto boolTy = BoolType::get(&context);
59
60 OwningOpRef<ExistsOp> existsOp = builder.create<ExistsOp>(
61 loc, TypeRange{boolTy, boolTy},
62 [](OpBuilder &builder, Location loc, ValueRange boundVars) {
63 return builder.create<AndOp>(loc, boundVars);
64 },
65 ArrayRef<StringRef>{"a", "b"}, nullptr, /*weight=*/0, /*noPattern=*/true);
66
67 SmallVector<char, 1024> buffer;
68 llvm::raw_svector_ostream stream(buffer);
69 existsOp->print(stream);
70
71 ASSERT_STREQ(stream.str().str().c_str(),
72 "%0 = smt.exists [\"a\", \"b\"] no_pattern {\n^bb0(%arg0: "
73 "!smt.bool, %arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n "
74 "smt.yield %0 : !smt.bool\n}\n");
75}
76
77TEST(QuantifierTest, ExistsBuilderDefault) {
78 MLIRContext context;
79 context.loadDialect<SMTDialect>();
80 Location loc(UnknownLoc::get(&context));
81
82 OpBuilder builder(&context);
83 auto boolTy = BoolType::get(&context);
84
85 OwningOpRef<ExistsOp> existsOp = builder.create<ExistsOp>(
86 loc, TypeRange{boolTy, boolTy},
87 [](OpBuilder &builder, Location loc, ValueRange boundVars) {
88 return builder.create<AndOp>(loc, boundVars);
89 },
90 ArrayRef<StringRef>{"a", "b"});
91
92 SmallVector<char, 1024> buffer;
93 llvm::raw_svector_ostream stream(buffer);
94 existsOp->print(stream);
95
96 ASSERT_STREQ(stream.str().str().c_str(),
97 "%0 = smt.exists [\"a\", \"b\"] {\n^bb0(%arg0: !smt.bool, "
98 "%arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n smt.yield "
99 "%0 : !smt.bool\n}\n");
100}
101
102//===----------------------------------------------------------------------===//
103// Test custom builders of ForallOp
104//===----------------------------------------------------------------------===//
105
106TEST(QuantifierTest, ForallBuilderWithPattern) {
107 MLIRContext context;
108 context.loadDialect<SMTDialect>();
109 Location loc(UnknownLoc::get(&context));
110
111 OpBuilder builder(&context);
112 auto boolTy = BoolType::get(&context);
113
114 OwningOpRef<ForallOp> forallOp = builder.create<ForallOp>(
115 loc, TypeRange{boolTy, boolTy},
116 [](OpBuilder &builder, Location loc, ValueRange boundVars) {
117 return builder.create<AndOp>(loc, boundVars);
118 },
119 ArrayRef<StringRef>{"a", "b"},
120 [](OpBuilder &builder, Location loc, ValueRange boundVars) {
121 return boundVars;
122 },
123 /*weight=*/2);
124
125 SmallVector<char, 1024> buffer;
126 llvm::raw_svector_ostream stream(buffer);
127 forallOp->print(stream);
128
129 ASSERT_STREQ(
130 stream.str().str().c_str(),
131 "%0 = smt.forall [\"a\", \"b\"] weight 2 {\n^bb0(%arg0: !smt.bool, "
132 "%arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n smt.yield %0 : "
133 "!smt.bool\n} patterns {\n^bb0(%arg0: !smt.bool, %arg1: !smt.bool):\n "
134 "smt.yield %arg0, %arg1 : !smt.bool, !smt.bool\n}\n");
135}
136
137TEST(QuantifierTest, ForallBuilderNoPattern) {
138 MLIRContext context;
139 context.loadDialect<SMTDialect>();
140 Location loc(UnknownLoc::get(&context));
141
142 OpBuilder builder(&context);
143 auto boolTy = BoolType::get(&context);
144
145 OwningOpRef<ForallOp> forallOp = builder.create<ForallOp>(
146 loc, TypeRange{boolTy, boolTy},
147 [](OpBuilder &builder, Location loc, ValueRange boundVars) {
148 return builder.create<AndOp>(loc, boundVars);
149 },
150 ArrayRef<StringRef>{"a", "b"}, nullptr, /*weight=*/0, /*noPattern=*/true);
151
152 SmallVector<char, 1024> buffer;
153 llvm::raw_svector_ostream stream(buffer);
154 forallOp->print(stream);
155
156 ASSERT_STREQ(stream.str().str().c_str(),
157 "%0 = smt.forall [\"a\", \"b\"] no_pattern {\n^bb0(%arg0: "
158 "!smt.bool, %arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n "
159 "smt.yield %0 : !smt.bool\n}\n");
160}
161
162TEST(QuantifierTest, ForallBuilderDefault) {
163 MLIRContext context;
164 context.loadDialect<SMTDialect>();
165 Location loc(UnknownLoc::get(&context));
166
167 OpBuilder builder(&context);
168 auto boolTy = BoolType::get(&context);
169
170 OwningOpRef<ForallOp> forallOp = builder.create<ForallOp>(
171 loc, TypeRange{boolTy, boolTy},
172 [](OpBuilder &builder, Location loc, ValueRange boundVars) {
173 return builder.create<AndOp>(loc, boundVars);
174 },
175 std::nullopt);
176
177 SmallVector<char, 1024> buffer;
178 llvm::raw_svector_ostream stream(buffer);
179 forallOp->print(stream);
180
181 ASSERT_STREQ(stream.str().str().c_str(),
182 "%0 = smt.forall {\n^bb0(%arg0: !smt.bool, "
183 "%arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n smt.yield "
184 "%0 : !smt.bool\n}\n");
185}
186
187} // namespace
188

source code of mlir/unittests/Dialect/SMT/QuantifierTest.cpp