blob: d81bc77872a7a1b22f3b89026de604ff34088c8f [file] [log] [blame]
Austin Engcc2516a2023-10-17 20:57:54 +00001// Copyright 2023 The Dawn & Tint Authors
Ben Claytonec6262f2023-08-18 18:30:15 +00002//
Austin Engcc2516a2023-10-17 20:57:54 +00003// Redistribution and use in source and binary forms, with or without
4// modification, are permitted provided that the following conditions are met:
Ben Claytonec6262f2023-08-18 18:30:15 +00005//
Austin Engcc2516a2023-10-17 20:57:54 +00006// 1. Redistributions of source code must retain the above copyright notice, this
7// list of conditions and the following disclaimer.
Ben Claytonec6262f2023-08-18 18:30:15 +00008//
Austin Engcc2516a2023-10-17 20:57:54 +00009// 2. Redistributions in binary form must reproduce the above copyright notice,
10// this list of conditions and the following disclaimer in the documentation
11// and/or other materials provided with the distribution.
12//
13// 3. Neither the name of the copyright holder nor the names of its
14// contributors may be used to endorse or promote products derived from
15// this software without specific prior written permission.
16//
17// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
18// AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
19// IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
20// DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
21// FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
22// DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
23// SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
24// CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
25// OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
26// OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
Ben Claytonec6262f2023-08-18 18:30:15 +000027
28package cnf_test
29
30import (
31 "testing"
32
33 "dawn.googlesource.com/dawn/tools/src/cnf"
34 "github.com/google/go-cmp/cmp"
35)
36
37func TestAnd(t *testing.T) {
38 type E = cnf.Expr
39 for _, test := range []struct {
40 lhs, rhs cnf.Expr
41 expect cnf.Expr
42 }{
43 { // And('', '') => ''
44 lhs: E{}, rhs: E{},
45 expect: E{},
46 },
47 { // And('X', '') => 'X'
48 lhs: E{{T("X")}}, rhs: E{},
49 expect: E{{T("X")}},
50 },
51 { // And('!X', '') => '!X'
52 lhs: E{{F("X")}}, rhs: E{},
53 expect: E{{F("X")}},
54 },
55 { // And('', 'X') => 'X'
56 lhs: E{}, rhs: E{{T("X")}},
57 expect: E{{T("X")}},
58 },
59 { // And('', '!X') => '!X'
60 lhs: E{}, rhs: E{{F("X")}},
61 expect: E{{F("X")}},
62 },
63 { // And('X', 'Y') => 'X && Y'
64 lhs: E{{T("X")}}, rhs: E{{T("Y")}},
65 expect: E{{T("X")}, {T("Y")}},
66 },
67 { // And('X', '!Y') => 'X && !Y'
68 lhs: E{{T("X")}}, rhs: E{{F("Y")}},
69 expect: E{{T("X")}, {F("Y")}},
70 },
71 { // And('Y', 'X') => 'Y && X'
72 lhs: E{{T("Y")}}, rhs: E{{T("X")}},
73 expect: E{{T("Y")}, {T("X")}},
74 },
75 { // And('!Y', 'X') => '!Y && X'
76 lhs: E{{F("Y")}}, rhs: E{{T("X")}},
77 expect: E{{F("Y")}, {T("X")}},
78 },
79 { // And('X && Y', 'Z') => 'X && Y && Z'
80 lhs: E{{T("X")}, {T("Y")}}, rhs: E{{T("Z")}},
81 expect: E{{T("X")}, {T("Y")}, {T("Z")}},
82 },
83 { // And('!X && Y', 'Z') => '!X && Y && Z'
84 lhs: E{{F("X")}, {T("Y")}}, rhs: E{{T("Z")}},
85 expect: E{{F("X")}, {T("Y")}, {T("Z")}},
86 },
87 { // And('X && !Y', 'Z') => 'X && !Y && Z'
88 lhs: E{{T("X")}, {F("Y")}}, rhs: E{{T("Z")}},
89 expect: E{{T("X")}, {F("Y")}, {T("Z")}},
90 },
91 { // And('X && Y', '!Z') => 'X && Y && !Z'
92 lhs: E{{T("X")}, {T("Y")}}, rhs: E{{F("Z")}},
93 expect: E{{T("X")}, {T("Y")}, {F("Z")}},
94 },
95 { // And('X', 'Y && Z') => 'X && Y && Z'
96 lhs: E{{T("X")}}, rhs: E{{T("Y")}, {T("Z")}},
97 expect: E{{T("X")}, {T("Y")}, {T("Z")}},
98 },
99 { // And('!X', 'Y && Z') => '!X && Y && Z'
100 lhs: E{{F("X")}}, rhs: E{{T("Y")}, {T("Z")}},
101 expect: E{{F("X")}, {T("Y")}, {T("Z")}},
102 },
103 { // And('X', '!Y && Z') => 'X && !Y && Z'
104 lhs: E{{T("X")}}, rhs: E{{F("Y")}, {T("Z")}},
105 expect: E{{T("X")}, {F("Y")}, {T("Z")}},
106 },
107 { // And('X', 'Y && !Z') => 'X && Y && !Z'
108 lhs: E{{T("X")}}, rhs: E{{T("Y")}, {F("Z")}},
109 expect: E{{T("X")}, {T("Y")}, {F("Z")}},
110 },
111 { // And('X && Y', 'Y && Z') => 'X && Y && Y && Z'
112 lhs: E{{T("X")}, {T("Y")}}, rhs: E{{T("Y")}, {T("Z")}},
113 expect: E{{T("X")}, {T("Y")}, {T("Y")}, {T("Z")}},
114 },
115 { // And('!X && Y', 'Y && !Z') => '!X && Y && Y && !Z'
116 lhs: E{{F("X")}, {T("Y")}}, rhs: E{{T("Y")}, {F("Z")}},
117 expect: E{{F("X")}, {T("Y")}, {T("Y")}, {F("Z")}},
118 },
119 { // And('X || Y', 'Z') => '(X || Y) && Z'
120 lhs: E{{T("X"), T("Y")}}, rhs: E{{T("Z")}},
121 expect: E{{T("X"), T("Y")}, {T("Z")}},
122 },
123 { // And('!X || Y', 'Z') => '(!X || Y) && Z'
124 lhs: E{{F("X"), T("Y")}}, rhs: E{{T("Z")}},
125 expect: E{{F("X"), T("Y")}, {T("Z")}},
126 },
127 { // And('X || !Y', 'Z') => '(X || !Y) && Z'
128 lhs: E{{T("X"), F("Y")}}, rhs: E{{T("Z")}},
129 expect: E{{T("X"), F("Y")}, {T("Z")}},
130 },
131 { // And('X || Y', '!Z') => '(X || Y) && !Z'
132 lhs: E{{T("X"), T("Y")}}, rhs: E{{F("Z")}},
133 expect: E{{T("X"), T("Y")}, {F("Z")}},
134 },
135 { // And('X', 'Y || Z') => 'X && (Y || Z)'
136 lhs: E{{T("X")}}, rhs: E{{T("Y"), T("Z")}},
137 expect: E{{T("X")}, {T("Y"), T("Z")}},
138 },
139 { // And('!X', 'Y || Z') => '!X && (Y || Z)'
140 lhs: E{{F("X")}}, rhs: E{{T("Y"), T("Z")}},
141 expect: E{{F("X")}, {T("Y"), T("Z")}},
142 },
143 { // And('X', '!Y || Z') => 'X && (!Y || Z)'
144 lhs: E{{T("X")}}, rhs: E{{F("Y"), T("Z")}},
145 expect: E{{T("X")}, {F("Y"), T("Z")}},
146 },
147 { // And('X', 'Y || !Z') => 'X && (Y || !Z)'
148 lhs: E{{T("X")}}, rhs: E{{T("Y"), F("Z")}},
149 expect: E{{T("X")}, {T("Y"), F("Z")}},
150 },
151 { // And('X || Y', 'Y || Z') => '(X || Y) && (Y || Z)'
152 lhs: E{{T("X"), T("Y")}}, rhs: E{{T("Y"), T("Z")}},
153 expect: E{{T("X"), T("Y")}, {T("Y"), T("Z")}},
154 },
155 { // And('!X || Y', 'Y || !Z') => '(!X || Y) && (Y || !Z)'
156 lhs: E{{F("X"), T("Y")}}, rhs: E{{T("Y"), F("Z")}},
157 expect: E{{F("X"), T("Y")}, {T("Y"), F("Z")}},
158 },
159 { // And('X || Y', 'Y && Z') => '(X || Y) && Y && Z'
160 lhs: E{{T("X"), T("Y")}}, rhs: E{{T("Y")}, {T("Z")}},
161 expect: E{{T("X"), T("Y")}, {T("Y")}, {T("Z")}},
162 },
163 { // And('!X && Y', 'Y || !Z') => '!X && Y && (Y || !Z)'
164 lhs: E{{F("X")}, {T("Y")}}, rhs: E{{T("Y"), F("Z")}},
165 expect: E{{F("X")}, {T("Y")}, {T("Y"), F("Z")}},
166 },
167 } {
168 got := cnf.And(test.lhs, test.rhs)
169 if diff := cmp.Diff(test.expect, got); diff != "" {
170 t.Errorf("And('%v', '%v') returned '%v'. Diff:\n%v", test.lhs, test.rhs, got, diff)
171 }
172 }
173}
174
175func TestOr(t *testing.T) {
176 type E = cnf.Expr
177 for _, test := range []struct {
178 lhs, rhs cnf.Expr
179 expect cnf.Expr
180 }{
181 { // Or('', '') => ''
182 lhs: E{}, rhs: E{},
183 expect: E{},
184 },
185 { // Or('X', '') => 'X'
186 lhs: E{{T("X")}}, rhs: E{},
187 expect: E{{T("X")}},
188 },
189 { // Or('!X', '') => '!X'
190 lhs: E{{F("X")}}, rhs: E{},
191 expect: E{{F("X")}},
192 },
193 { // Or('', 'X') => 'X'
194 lhs: E{}, rhs: E{{T("X")}},
195 expect: E{{T("X")}},
196 },
197 { // Or('', '!X') => '!X'
198 lhs: E{}, rhs: E{{F("X")}},
199 expect: E{{F("X")}},
200 },
201 { // Or('X', 'Y') => 'X || Y'
202 lhs: E{{T("X")}}, rhs: E{{T("Y")}},
203 expect: E{{T("X"), T("Y")}},
204 },
205 { // Or('X', '!Y') => 'X || !Y'
206 lhs: E{{T("X")}}, rhs: E{{F("Y")}},
207 expect: E{{T("X"), F("Y")}},
208 },
209 { // Or('Y', 'X') => 'Y || X'
210 lhs: E{{T("Y")}}, rhs: E{{T("X")}},
211 expect: E{{T("Y"), T("X")}},
212 },
213 { // Or('!Y', 'X') => '!Y || X'
214 lhs: E{{F("Y")}}, rhs: E{{T("X")}},
215 expect: E{{F("Y"), T("X")}},
216 },
217 { // Or('X && Y', 'Z') => '(X || Z) && (Y || Z)'
218 lhs: E{{T("X")}, {T("Y")}}, rhs: E{{T("Z")}},
219 expect: E{{T("X"), T("Z")}, {T("Y"), T("Z")}},
220 },
221 { // Or('!X && Y', 'Z') => '(!X || Z) && (Y || Z)'
222 lhs: E{{F("X")}, {T("Y")}}, rhs: E{{T("Z")}},
223 expect: E{{F("X"), T("Z")}, {T("Y"), T("Z")}},
224 },
225 { // Or('X && !Y', 'Z') => '(X || Z) && (!Y || Z)'
226 lhs: E{{T("X")}, {F("Y")}}, rhs: E{{T("Z")}},
227 expect: E{{T("X"), T("Z")}, {F("Y"), T("Z")}},
228 },
229 { // Or('X && Y', '!Z') => '(X || !Z) && (Y || !Z)'
230 lhs: E{{T("X")}, {T("Y")}}, rhs: E{{F("Z")}},
231 expect: E{{T("X"), F("Z")}, {T("Y"), F("Z")}},
232 },
233 { // Or('X', 'Y && Z') => '(X || Y) && (X || Z)'
234 lhs: E{{T("X")}}, rhs: E{{T("Y")}, {T("Z")}},
235 expect: E{{T("X"), T("Y")}, {T("X"), T("Z")}},
236 },
237 { // Or('!X', 'Y && Z') => '(!X || Y) && (!X || Z)'
238 lhs: E{{F("X")}}, rhs: E{{T("Y")}, {T("Z")}},
239 expect: E{{F("X"), T("Y")}, {F("X"), T("Z")}},
240 },
241 { // Or('X', '!Y && Z') => '(X || !Y) && (X || Z)'
242 lhs: E{{T("X")}}, rhs: E{{F("Y")}, {T("Z")}},
243 expect: E{{T("X"), F("Y")}, {T("X"), T("Z")}},
244 },
245 { // Or('X', 'Y && !Z') => '(X || Y) && (X || !Z)'
246 lhs: E{{T("X")}}, rhs: E{{T("Y")}, {F("Z")}},
247 expect: E{{T("X"), T("Y")}, {T("X"), F("Z")}},
248 },
249 { // Or('X && Y', 'Z && W') => '(X || Z) && (X || W) && (Y || Z) && (Y || W)'
250 lhs: E{{T("X")}, {T("Y")}}, rhs: E{{T("Z")}, {T("W")}},
251 expect: E{{T("X"), T("Z")}, {T("X"), T("W")}, {T("Y"), T("Z")}, {T("Y"), T("W")}},
252 },
253 { // Or('!X && Y', 'Z && !W') => '(!X || Z) && (!X || !W) && (Y || Z) && (Y || !W)'
254 lhs: E{{F("X")}, {T("Y")}}, rhs: E{{T("Z")}, {F("W")}},
255 expect: E{{F("X"), T("Z")}, {F("X"), F("W")}, {T("Y"), T("Z")}, {T("Y"), F("W")}},
256 },
257 { // Or('X || Y', 'Z') => 'X || Y || Z'
258 lhs: E{{T("X"), T("Y")}}, rhs: E{{T("Z")}},
259 expect: E{{T("X"), T("Y"), T("Z")}},
260 },
261 { // Or('!X || Y', 'Z') => '!X || Y || Z'
262 lhs: E{{F("X"), T("Y")}}, rhs: E{{T("Z")}},
263 expect: E{{F("X"), T("Y"), T("Z")}},
264 },
265 { // Or('X || !Y', 'Z') => 'X || !Y || Z'
266 lhs: E{{T("X"), F("Y")}}, rhs: E{{T("Z")}},
267 expect: E{{T("X"), F("Y"), T("Z")}},
268 },
269 { // Or('X || Y', '!Z') => 'X || Y || !Z'
270 lhs: E{{T("X"), T("Y")}}, rhs: E{{F("Z")}},
271 expect: E{{T("X"), T("Y"), F("Z")}},
272 },
273 { // Or('X', 'Y || Z') => 'X || Y || Z'
274 lhs: E{{T("X")}}, rhs: E{{T("Y"), T("Z")}},
275 expect: E{{T("X"), T("Y"), T("Z")}},
276 },
277 { // Or('!X', 'Y || Z') => '!X || Y || Z'
278 lhs: E{{F("X")}}, rhs: E{{T("Y"), T("Z")}},
279 expect: E{{F("X"), T("Y"), T("Z")}},
280 },
281 { // Or('X', '!Y || Z') => 'X || !Y || Z'
282 lhs: E{{T("X")}}, rhs: E{{F("Y"), T("Z")}},
283 expect: E{{T("X"), F("Y"), T("Z")}},
284 },
285 { // Or('X', 'Y || !Z') => 'X || Y || !Z'
286 lhs: E{{T("X")}}, rhs: E{{T("Y"), F("Z")}},
287 expect: E{{T("X"), T("Y"), F("Z")}},
288 },
289 { // Or('X || Y', 'Y || Z') => 'X || Y || Y || Z'
290 lhs: E{{T("X"), T("Y")}}, rhs: E{{T("Y"), T("Z")}},
291 expect: E{{T("X"), T("Y"), T("Y"), T("Z")}},
292 },
293 { // Or('!X || Y', 'Y || !Z') => '!X || Y || Y || !Z'
294 lhs: E{{F("X"), T("Y")}}, rhs: E{{T("Y"), F("Z")}},
295 expect: E{{F("X"), T("Y"), T("Y"), F("Z")}},
296 },
297 { // Or('X || Y', 'Y && Z') => '(X || Y || Y) && (X || Y || Z)'
298 lhs: E{{T("X"), T("Y")}}, rhs: E{{T("Y")}, {T("Z")}},
299 expect: E{{T("X"), T("Y"), T("Y")}, {T("X"), T("Y"), T("Z")}},
300 },
301 { // Or('!X && Y', 'Z || !W') => '(!X || Z || !W) && (Y || Z || !W)'
302 lhs: E{{F("X")}, {T("Y")}}, rhs: E{{T("Z"), F("W")}},
303 expect: E{{F("X"), T("Z"), F("W")}, {T("Y"), T("Z"), F("W")}},
304 },
305 } {
306 got := cnf.Or(test.lhs, test.rhs)
307 if diff := cmp.Diff(test.expect, got); diff != "" {
308 t.Errorf("Or('%v', '%v') returned '%v'. Diff:\n%v", test.lhs, test.rhs, got, diff)
309 }
310 }
311}
312
313func TestNot(t *testing.T) {
314 type E = cnf.Expr
315 for _, test := range []struct {
316 expr cnf.Expr
317 expect cnf.Expr
318 }{
319 { // Not('') => ''
320 expr: E{},
321 expect: E{},
322 },
323 { // Not('X') => '!X'
324 expr: E{{T("X")}},
325 expect: E{{F("X")}},
326 },
327 { // Not('!X') => 'X'
328 expr: E{{F("X")}},
329 expect: E{{T("X")}},
330 },
331 { // Not('X || Y') => '!X && !Y'
332 expr: E{{T("X"), T("Y")}},
333 expect: E{{F("X")}, {F("Y")}},
334 },
335 { // Not('X || !Y') => '!X && Y'
336 expr: E{{T("X"), F("Y")}},
337 expect: E{{F("X")}, {T("Y")}},
338 },
339 { // Not('X && Y') => '!X || !Y'
340 expr: E{{T("X")}, {T("Y")}},
341 expect: E{{F("X"), F("Y")}},
342 },
343 { // Not('!X && Y') => 'X || !Y'
344 expr: E{{F("X")}, {T("Y")}},
345 expect: E{{T("X"), F("Y")}},
346 },
347 { // Not('(X || Y) && Z') => '(!X || !Z) && (!Y || !Z)'
348 expr: E{{T("X"), T("Y")}, {T("Z")}},
349 expect: E{{F("X"), F("Z")}, {F("Y"), F("Z")}},
350 },
351 { // Not('X && (Y || Z)') => '(!X || !Y) && (!X || !Z)'
352 expr: E{{T("X")}, {T("Y"), T("Z")}},
353 expect: E{{F("X"), F("Y")}, {F("X"), F("Z")}},
354 },
355 { // Not('X && (!Y || Z)') => '(!X || Y) && (!X || !Z)'
356 expr: E{{T("X")}, {F("Y"), T("Z")}},
357 expect: E{{F("X"), T("Y")}, {F("X"), F("Z")}},
358 },
359 { // Not('(X || Y) && (Z || W)') => '(!X || !Z) && (!X || !W) && (!Y || !Z) && (!Y || !W)'
360 expr: E{{T("X"), T("Y")}, {T("Z"), T("W")}},
361 expect: E{{F("X"), F("Z")}, {F("X"), F("W")}, {F("Y"), F("Z")}, {F("Y"), F("W")}},
362 },
363 { // Not('(X || !Y) && (!Z || W)') => '(!X || Z) && (!X || !W) && (Y || Z) && (Y || !W)'
364 expr: E{{T("X"), F("Y")}, {F("Z"), T("W")}},
365 expect: E{{F("X"), T("Z")}, {F("X"), F("W")}, {T("Y"), T("Z")}, {T("Y"), F("W")}},
366 },
367 } {
368 got := cnf.Not(test.expr)
369 if diff := cmp.Diff(test.expect, got); diff != "" {
370 t.Errorf("Not('%v') returned '%v'. Diff:\n%v", test.expr, got, diff)
371 }
372 }
373}