1;; Rewrites for `band`, `bnot`, `bor`, `bxor`
2
3;; x | 0 == x | x == x.
4(rule (simplify (bor ty
5                     x
6                     (iconst_u ty 0)))
7      (subsume x))
8(rule (simplify (bor ty x x))
9      (subsume x))
10
11;; x ^ 0 == x.
12(rule (simplify (bxor ty
13                     x
14                     (iconst_u ty 0)))
15      (subsume x))
16
17;; x ^ x == 0.
18(rule (simplify (bxor (ty_int ty) x x))
19      (subsume (iconst_u ty 0)))
20
21;; x ^ not(x) == not(x) ^ x == x | not(x) == not(x) | x == -1.
22;; This identity also holds for non-integer types, vectors, and wider types.
23(rule (simplify (bxor (ty_int ty) x (bnot ty x))) (subsume (iconst_s ty -1)))
24(rule (simplify (bxor (ty_int ty) (bnot ty x) x)) (subsume (iconst_s ty -1)))
25(rule (simplify (bor (ty_int ty) x (bnot ty x))) (subsume (iconst_s ty -1)))
26(rule (simplify (bor (ty_int ty) (bnot ty x) x)) (subsume (iconst_s ty -1)))
27
28;; x & x == x & -1 == x.
29(rule (simplify (band ty x x)) (subsume x))
30(rule (simplify (band ty x (iconst_s ty -1)))
31      (subsume x))
32
33;; x & 0 == x & not(x) == not(x) & x == 0.
34(rule (simplify (band ty _ zero @ (iconst_u ty 0))) (subsume zero))
35(rule (simplify (band (ty_int ty) x (bnot ty x))) (subsume (iconst_u ty 0)))
36(rule (simplify (band (ty_int ty) (bnot ty x) x)) (subsume (iconst_u ty 0)))
37
38;; (x & y) ^ (x ^ y) == x | y
39(rule (simplify (bxor ty (band ty X Y) (bxor ty X Y))) (bor ty X Y))
40
41;; not(not(x)) == x.
42(rule (simplify (bnot ty (bnot ty x))) (subsume x))
43
44;; `or(and(x, y), not(y)) == or(x, not(y))`
45(rule (simplify (bor ty
46                     (band ty x y)
47                     z @ (bnot ty y)))
48      (bor ty x z))
49;; Duplicate the rule but swap the `bor` operands because `bor` is
50;; commutative. We could, of course, add a `simplify` rule to do the commutative
51;; swap for all `bor`s but this will bloat the e-graph with many e-nodes. It is
52;; cheaper to have additional rules, rather than additional e-nodes, because we
53;; amortize their cost via ISLE's smart codegen.
54(rule (simplify (bor ty
55                     z @ (bnot ty y)
56                     (band ty x y)))
57      (bor ty x z))
58
59;; `or(and(x, y), not(y)) == or(x, not(y))` specialized for constants, since
60;; otherwise we may not know that `z == not(y)` since we don't generally expand
61;; constants in the e-graph.
62;;
63;; (No need to duplicate for commutative `bor` for this constant version because
64;; we move constants to the right.)
65(rule (simplify (bor ty
66                     (band ty x (iconst_u ty y))
67                     z @ (iconst_u ty zk)))
68      (if-let true (u64_eq (u64_and (ty_mask ty) zk)
69                            (u64_and (ty_mask ty) (u64_not y))))
70      (bor ty x z))
71
72;; (x ^ -1) can be replaced with the `bnot` instruction
73(rule (simplify (bxor ty x (iconst_s ty -1)))
74  (bnot ty x))
75
76;; sshr((x | -x), N) == bmask(x) where N = ty_bits(ty) - 1.
77;;
78;; (x | -x) sets the sign bit to 1 if x is nonzero, and 0 if x is zero. sshr propagates
79;; the sign bit to the rest of the value.
80(rule (simplify (sshr ty (bor ty x (ineg ty x)) (iconst_u ty shift_amt)))
81      (if-let true (u64_eq shift_amt (ty_shift_mask ty)))
82      (bmask ty x))
83
84(rule (simplify (sshr ty (bor ty (ineg ty x) x) (iconst_u ty shift_amt)))
85      (if-let true (u64_eq shift_amt (ty_shift_mask ty)))
86      (bmask ty x))
87
88;; Since icmp is always 0 or 1, bmask is just a negation.
89;; TODO: Explore whether this makes sense for things needing extension too.
90(rule (simplify (bmask $I8 cmp@(icmp $I8 _ _ _)))
91      (ineg $I8 cmp))
92
93;; Matches any expressions that preserve "truthiness".
94;; i.e. If the input is zero it remains zero, and if it is nonzero it can have
95;; a different value as long as it is still nonzero.
96(decl pure multi truthy (Value) Value)
97(rule (truthy (sextend _ x)) x)
98(rule (truthy (uextend _ x)) x)
99(rule (truthy (bmask _ x)) x)
100(rule (truthy (ineg _ x)) x)
101(rule (truthy (bswap _ x)) x)
102(rule (truthy (bitrev _ x)) x)
103(rule (truthy (popcnt _ x)) x)
104(rule (truthy (rotl _ x _)) x)
105(rule (truthy (rotr _ x _)) x)
106(rule (truthy (select _ x (iconst_u _ (u64_when_non_zero)) (iconst_u _ 0))) x)
107;; (ne ty (iconst 0) v) is also canonicalized into this form via another rule
108(rule (truthy (ne _ x (iconst_u _ 0))) x)
109
110;; All of these expressions don't care about their input as long as it is truthy.
111;; so we can remove expressions that preserve that property from the input.
112(rule (simplify (bmask ty v)) (if-let x (truthy v)) (bmask ty x))
113(rule (simplify (select ty v t f)) (if-let c (truthy v)) (select ty c t f))
114;; (ne ty (iconst 0) v) is also canonicalized into this form via another rule
115(rule (simplify (ne cty v (iconst_u _ 0)))
116      (if-let c (truthy v))
117      (if-let (value_type (ty_int_ref_scalar_64 ty)) c)
118      (ne cty c (iconst_u ty 0)))
119
120
121
122;; (sextend (bmask x)) can be replaced with (bmask x) since bmask
123;; supports any size of output type, regardless of input.
124;; Same with `ireduce`
125(rule (simplify (sextend ty (bmask _ x))) (bmask ty x))
126(rule (simplify (ireduce ty (bmask _ x))) (bmask ty x))
127
128;; (bswap (bswap x)) == x
129(rule (simplify (bswap ty (bswap ty x))) (subsume x))
130
131;; (bitrev (bitrev x)) == x
132(rule (simplify (bitrev ty (bitrev ty x))) (subsume x))
133
134;; WebAssembly doesn't have a native byte-swapping instruction at this time so
135;; languages which have a byte-swapping operation will compile it down to bit
136;; shifting and twiddling. This attempts to pattern match what LLVM currently
137;; generates today for the Rust code `a.swap_bytes()`. This might be a bit
138;; brittle over time and/or with other possible LLVM backend optimizations, but
139;; it's at least one way to generate a byte swap.
140;;
141;; Technically this could be permuted quite a few ways and currently there's no
142;; easy way to match all of them, so only one is matched here.
143(rule (simplify (bor ty @ $I32
144    (bor ty
145      (ishl ty x (iconst_u ty 24))
146      (ishl ty
147        (band ty x (iconst_u ty 0xff00))
148        (iconst_u ty 8)))
149    (bor ty
150      (band ty
151        (ushr ty x (iconst_u ty 8))
152        (iconst_u ty 0xff00))
153      (ushr ty x (iconst_u ty 24)))))
154  (bswap ty x))
155
156(rule (simplify (bor ty @ $I64
157    (bor ty
158      (bor ty
159        (ishl ty x (iconst_u ty 56))
160        (ishl ty
161          (band ty x (iconst_u ty 0xff00))
162          (iconst_u ty 40)))
163      (bor ty
164        (ishl ty
165          (band ty x (iconst_u ty 0xff_0000))
166          (iconst_u ty 24))
167        (ishl ty
168          (band ty x (iconst_u ty 0xff00_0000))
169          (iconst_u ty 8))))
170    (bor ty
171      (bor ty
172        (band ty
173          (ushr ty x (iconst_u ty 8))
174          (iconst_u ty 0xff00_0000))
175        (band ty
176          (ushr ty x (iconst_u ty 24))
177          (iconst_u ty 0xff_0000)))
178      (bor ty
179        (band ty
180          (ushr ty x (iconst_u ty 40))
181          (iconst_u ty 0xff00))
182        (ushr ty x (iconst_u ty 56))))))
183  (bswap ty x))
184
185(rule (simplify (bxor ty (bor ty x y) (band ty x y))) (bxor ty x y))
186
187
188(rule (simplify (bor ty (bor ty x y) x)) (bor ty x y))
189(rule (simplify (bor ty (bor ty x y) y)) (bor ty x y))
190(rule (simplify (bor ty x (bor ty x y))) (bor ty x y))
191(rule (simplify (bor ty y (bor ty x y))) (bor ty x y))
192
193(rule (simplify (band ty (band ty x y) x)) (band ty x y))
194(rule (simplify (band ty (band ty x y) y)) (band ty x y))
195(rule (simplify (band ty x (band ty x y))) (band ty x y))
196(rule (simplify (band ty y (band ty x y))) (band ty x y))
197
198;; (x ^ ~y) & x --> x & y
199(rule (simplify (band ty (bxor ty x (bnot ty y)) x)) (band ty x y))
200(rule (simplify (band ty (bxor ty (bnot ty y) x) x)) (band ty x y))
201(rule (simplify (band ty x (bxor ty x (bnot ty y)))) (band ty x y))
202(rule (simplify (band ty x (bxor ty (bnot ty y) x))) (band ty x y))
203
204; (x & y) + (x ^ y) --> x | y
205(rule (simplify (iadd ty (band ty x y) (bxor ty x y))) (bor ty x y))
206(rule (simplify (iadd ty (bxor ty x y) (band ty x y))) (bor ty x y))
207
208; (x | y) + (x & y) --> x + y
209(rule (simplify (iadd ty (bor ty x y) (band ty x y))) (iadd ty x y))
210(rule (simplify (iadd ty (band ty x y) (bor ty x y))) (iadd ty x y))
211
212; (x & y) | x --> x
213(rule (simplify (bor ty (band ty x y) x)) x)
214(rule (simplify (bor ty x (band ty x y))) x)
215
216; (x ^ y) ^ y --> x
217(rule (simplify (bxor ty (bxor ty x y) y)) x)
218(rule (simplify (bxor ty y (bxor ty x y))) x)
219
220; (x & y) | ~x -> y | ~x
221(rule (simplify (bor ty (band ty x y) (bnot ty x))) (bor ty y (bnot ty x)))
222(rule (simplify (bor ty (bnot ty x) (band ty x y))) (bor ty y (bnot ty x)))
223
224; (z & x) ^ (z & y) => z & (x ^ y)
225(rule (simplify
226  (bxor ty (band ty z x) (band ty z y)))
227	(band ty z (bxor ty x y)))
228
229; (x & y) | ~(x ^ y) => ~(x ^ y)
230(rule (simplify (bor ty (band ty x y) (bnot ty (bxor ty x y)))) (bnot ty (bxor ty x y)))
231(rule (simplify (bor ty (bnot ty (bxor ty x y)) (band ty x y))) (bnot ty (bxor ty x y)))
232(rule (simplify (bor ty (band ty x y) (bnot ty (bxor ty y x)))) (bnot ty (bxor ty x y)))
233(rule (simplify (bor ty (bnot ty (bxor ty y x)) (band ty x y))) (bnot ty (bxor ty x y)))
234(rule (simplify (bor ty (band ty y x) (bnot ty (bxor ty x y)))) (bnot ty (bxor ty x y)))
235(rule (simplify (bor ty (bnot ty (bxor ty x y)) (band ty y x))) (bnot ty (bxor ty x y)))
236(rule (simplify (bor ty (band ty y x) (bnot ty (bxor ty y x)))) (bnot ty (bxor ty x y)))
237(rule (simplify (bor ty (bnot ty (bxor ty y x)) (band ty y x))) (bnot ty (bxor ty x y)))
238
239; (x | y) + (-y) --> x & ~y
240(rule (simplify (iadd ty (bor ty x y) (ineg ty y)))
241      (band ty x (bnot ty y)))
242(rule (simplify (iadd ty (ineg ty y) (bor ty x y)))
243      (band ty x (bnot ty y)))
244(rule (simplify (iadd ty (bor ty y x) (ineg ty y)))
245      (band ty x (bnot ty y)))
246(rule (simplify (iadd ty (ineg ty y) (bor ty y x)))
247      (band ty x (bnot ty y)))
248
249; x & (x | y) --> x
250(rule (simplify (band ty (bor ty x y) x)) x)
251(rule (simplify (band ty x (bor ty x y))) x)
252(rule (simplify (band ty (bor ty y x) x)) x)
253(rule (simplify (band ty x (bor ty y x))) x)
254
255; (x | z) & (y | z) --> (x & y) | z
256(rule (simplify (band ty (bor ty x z) (bor ty y z))) (bor ty (band ty x y) z))
257(rule (simplify (band ty (bor ty y z) (bor ty x z))) (bor ty (band ty x y) z))
258(rule (simplify (band ty (bor ty x z) (bor ty z y))) (bor ty (band ty x y) z))
259(rule (simplify (band ty (bor ty z y) (bor ty x z))) (bor ty (band ty x y) z))
260(rule (simplify (band ty (bor ty z x) (bor ty y z))) (bor ty (band ty x y) z))
261(rule (simplify (band ty (bor ty y z) (bor ty z x))) (bor ty (band ty x y) z))
262(rule (simplify (band ty (bor ty z x) (bor ty z y))) (bor ty (band ty x y) z))
263(rule (simplify (band ty (bor ty z y) (bor ty z x))) (bor ty (band ty x y) z))
264
265; (x & z) | (y & z) --> (x | y) & z
266(rule (simplify (bor ty (band ty x z) (band ty y z))) (band ty (bor ty x y) z))
267(rule (simplify (bor ty (band ty y z) (band ty x z))) (band ty (bor ty x y) z))
268(rule (simplify (bor ty (band ty x z) (band ty z y))) (band ty (bor ty x y) z))
269(rule (simplify (bor ty (band ty z y) (band ty x z))) (band ty (bor ty x y) z))
270(rule (simplify (bor ty (band ty z x) (band ty y z))) (band ty (bor ty x y) z))
271(rule (simplify (bor ty (band ty y z) (band ty z x))) (band ty (bor ty x y) z))
272(rule (simplify (bor ty (band ty z x) (band ty z y))) (band ty (bor ty x y) z))
273(rule (simplify (bor ty (band ty z y) (band ty z x))) (band ty (bor ty x y) z))
274
275; (x | y) ^ (x | ~y) --> ~x
276(rule (simplify (bxor ty (bor ty x y) (bor ty x (bnot ty y)))) (bnot ty x))
277(rule (simplify (bxor ty (bor ty x (bnot ty y)) (bor ty x y))) (bnot ty x))
278(rule (simplify (bxor ty (bor ty x y) (bor ty (bnot ty y) x))) (bnot ty x))
279(rule (simplify (bxor ty (bor ty (bnot ty y) x) (bor ty x y))) (bnot ty x))
280(rule (simplify (bxor ty (bor ty y x) (bor ty x (bnot ty y)))) (bnot ty x))
281(rule (simplify (bxor ty (bor ty x (bnot ty y)) (bor ty y x))) (bnot ty x))
282(rule (simplify (bxor ty (bor ty y x) (bor ty (bnot ty y) x))) (bnot ty x))
283(rule (simplify (bxor ty (bor ty (bnot ty y) x) (bor ty y x))) (bnot ty x))
284
285; (~x) & (~y) --> ~(x | y)
286(rule (simplify (band ty (bnot ty x) (bnot ty y))) (bnot ty (bor ty x y)))
287(rule (simplify (band ty (bnot ty y) (bnot ty x))) (bnot ty (bor ty x y)))
288
289; (~x) | (~y) --> ~(x & y)
290(rule (simplify (bor ty (bnot ty x) (bnot ty y))) (bnot ty (band ty x y)))
291(rule (simplify (bor ty (bnot ty y) (bnot ty x))) (bnot ty (band ty x y)))
292
293; x | ((x ^ y) ^ z) --> x | (y ^ z)
294(rule (simplify (bor ty (bxor ty (bxor ty x y) z) x)) (bor ty (bxor ty y z) x))
295(rule (simplify (bor ty x (bxor ty (bxor ty x y) z))) (bor ty (bxor ty y z) x))
296(rule (simplify (bor ty (bxor ty z (bxor ty x y)) x)) (bor ty (bxor ty y z) x))
297(rule (simplify (bor ty x (bxor ty z (bxor ty x y)))) (bor ty (bxor ty y z) x))
298(rule (simplify (bor ty (bxor ty (bxor ty y x) z) x)) (bor ty (bxor ty y z) x))
299(rule (simplify (bor ty x (bxor ty (bxor ty y x) z))) (bor ty (bxor ty y z) x))
300(rule (simplify (bor ty (bxor ty z (bxor ty y x)) x)) (bor ty (bxor ty y z) x))
301(rule (simplify (bor ty x (bxor ty z (bxor ty y x)))) (bor ty (bxor ty y z) x))
302
303; (x ^ z) == (y ^ z) --> x == y
304(rule (simplify (eq ty (bxor cty x z) (bxor cty y z))) (eq ty x y))
305(rule (simplify (eq ty (bxor cty y z) (bxor cty x z))) (eq ty x y))
306(rule (simplify (eq ty (bxor cty x z) (bxor cty z y))) (eq ty x y))
307(rule (simplify (eq ty (bxor cty z y) (bxor cty x z))) (eq ty x y))
308(rule (simplify (eq ty (bxor cty z x) (bxor cty y z))) (eq ty x y))
309(rule (simplify (eq ty (bxor cty y z) (bxor cty z x))) (eq ty x y))
310(rule (simplify (eq ty (bxor cty z x) (bxor cty z y))) (eq ty x y))
311(rule (simplify (eq ty (bxor cty z y) (bxor cty z x))) (eq ty x y))
312
313; y | ~(x | y) --> y | ~x
314(rule (simplify (bor ty y (bnot ty (bor ty x y)))) (bor ty y (bnot ty x)))
315(rule (simplify (bor ty (bnot ty (bor ty x y)) y)) (bor ty y (bnot ty x)))
316(rule (simplify (bor ty y (bnot ty (bor ty y x)))) (bor ty y (bnot ty x)))
317(rule (simplify (bor ty (bnot ty (bor ty y x)) y)) (bor ty y (bnot ty x)))
318
319; y & ~(x & y) --> y & ~x
320(rule (simplify (band ty y (bnot ty (band ty x y)))) (band ty y (bnot ty x)))
321(rule (simplify (band ty (bnot ty (band ty x y)) y)) (band ty y (bnot ty x)))
322(rule (simplify (band ty y (bnot ty (band ty y x)))) (band ty y (bnot ty x)))
323(rule (simplify (band ty (bnot ty (band ty y x)) y)) (band ty y (bnot ty x)))
324
325; (~x) ^ (x | y) --> x | ~y
326(rule (simplify (bxor ty (bnot ty x) (bor ty x y))) (bor ty x (bnot ty y)))
327(rule (simplify (bxor ty (bor ty x y) (bnot ty x))) (bor ty x (bnot ty y)))
328(rule (simplify (bxor ty (bnot ty x) (bor ty y x))) (bor ty x (bnot ty y)))
329(rule (simplify (bxor ty (bor ty y x) (bnot ty x))) (bor ty x (bnot ty y)))
330
331; (x < y) | (x > y) --> x != y
332(rule (simplify (bor ty (slt ty x y) (sgt ty x y))) (ne ty x y))
333(rule (simplify (bor ty (sgt ty x y) (slt ty x y))) (ne ty x y))
334(rule (simplify (bor ty (slt ty x y) (slt ty y x))) (ne ty x y))
335(rule (simplify (bor ty (slt ty y x) (slt ty x y))) (ne ty x y))
336(rule (simplify (bor ty (sgt ty y x) (sgt ty x y))) (ne ty x y))
337(rule (simplify (bor ty (sgt ty x y) (sgt ty y x))) (ne ty x y))
338(rule (simplify (bor ty (sgt ty y x) (slt ty y x))) (ne ty x y))
339(rule (simplify (bor ty (slt ty y x) (sgt ty y x))) (ne ty x y))
340
341; (x <_u y) | (x >_u y) --> x != y
342(rule (simplify (bor ty (ult ty x y) (ugt ty x y))) (ne ty x y))
343(rule (simplify (bor ty (ugt ty x y) (ult ty x y))) (ne ty x y))
344(rule (simplify (bor ty (ult ty x y) (ult ty y x))) (ne ty x y))
345(rule (simplify (bor ty (ult ty y x) (ult ty x y))) (ne ty x y))
346(rule (simplify (bor ty (ugt ty y x) (ugt ty x y))) (ne ty x y))
347(rule (simplify (bor ty (ugt ty x y) (ugt ty y x))) (ne ty x y))
348(rule (simplify (bor ty (ugt ty y x) (ult ty y x))) (ne ty x y))
349(rule (simplify (bor ty (ult ty y x) (ugt ty y x))) (ne ty x y))
350
351; ~((~x) & y) --> x | ~y
352(rule (simplify (bnot ty (band ty (bnot ty x) y))) (bor ty x (bnot ty y)))
353(rule (simplify (bnot ty (band ty y (bnot ty x)))) (bor ty x (bnot ty y)))
354
355; ~((~x) | y) --> x & ~y
356(rule (simplify (bnot ty (bor ty (bnot ty x) y))) (band ty x (bnot ty y)))
357(rule (simplify (bnot ty (bor ty y (bnot ty x)))) (band ty x (bnot ty y)))
358
359; (x <_u y) | (x == y) --> (x <=_u y)
360(rule (simplify (bor ty (ult ty x y) (eq ty x y))) (ule ty x y))
361(rule (simplify (bor ty (eq ty x y) (ult ty x y))) (ule ty x y))
362(rule (simplify (bor ty (ult ty x y) (eq ty y x))) (ule ty x y))
363(rule (simplify (bor ty (eq ty y x) (ult ty x y))) (ule ty x y))
364
365; (y >_u x) | (x == y) --> (x <=_u y)
366(rule (simplify (bor ty (ugt ty y x) (eq ty x y))) (ule ty x y))
367(rule (simplify (bor ty (eq ty x y) (ugt ty y x))) (ule ty x y))
368(rule (simplify (bor ty (ugt ty y x) (eq ty y x))) (ule ty x y))
369(rule (simplify (bor ty (eq ty y x) (ugt ty y x))) (ule ty x y))
370
371; (x < y) | (x == y) --> (x <= y)
372(rule (simplify (bor ty (slt ty x y) (eq ty x y))) (sle ty x y))
373(rule (simplify (bor ty (eq ty x y) (slt ty x y))) (sle ty x y))
374(rule (simplify (bor ty (slt ty x y) (eq ty y x))) (sle ty x y))
375(rule (simplify (bor ty (eq ty y x) (slt ty x y))) (sle ty x y))
376
377; (y > x) | (x == y) --> (x <= y)
378(rule (simplify (bor ty (sgt ty y x) (eq ty x y))) (sle ty x y))
379(rule (simplify (bor ty (eq ty x y) (sgt ty y x))) (sle ty x y))
380(rule (simplify (bor ty (sgt ty y x) (eq ty y x))) (sle ty x y))
381(rule (simplify (bor ty (eq ty y x) (sgt ty y x))) (sle ty x y))
382
383; (x ^ z) | (((x ^ z) ^ y)) --> (x ^ z) | y
384(rule (simplify (bor ty (bxor ty x z) (bxor ty (bxor ty x z) y))) (bor ty (bxor ty x z) y))
385(rule (simplify (bor ty (bxor ty (bxor ty x z) y) (bxor ty x z))) (bor ty (bxor ty x z) y))
386(rule (simplify (bor ty (bxor ty x z) (bxor ty y (bxor ty x z)))) (bor ty (bxor ty x z) y))
387(rule (simplify (bor ty (bxor ty y (bxor ty x z)) (bxor ty x z))) (bor ty (bxor ty x z) y))
388
389(rule (simplify (bor ty (bxor ty x z) (bxor ty (bxor ty z x) y))) (bor ty (bxor ty x z) y))
390(rule (simplify (bor ty (bxor ty (bxor ty z x) y) (bxor ty x z))) (bor ty (bxor ty x z) y))
391(rule (simplify (bor ty (bxor ty x z) (bxor ty y (bxor ty z x)))) (bor ty (bxor ty x z) y))
392(rule (simplify (bor ty (bxor ty y (bxor ty z x)) (bxor ty x z))) (bor ty (bxor ty x z) y))
393
394(rule (simplify (bor ty (bxor ty z x) (bxor ty (bxor ty x z) y))) (bor ty (bxor ty x z) y))
395(rule (simplify (bor ty (bxor ty (bxor ty x z) y) (bxor ty z x))) (bor ty (bxor ty x z) y))
396(rule (simplify (bor ty (bxor ty z x) (bxor ty y (bxor ty x z)))) (bor ty (bxor ty x z) y))
397(rule (simplify (bor ty (bxor ty y (bxor ty x z)) (bxor ty z x))) (bor ty (bxor ty x z) y))
398
399(rule (simplify (bor ty (bxor ty z x) (bxor ty (bxor ty z x) y))) (bor ty (bxor ty x z) y))
400(rule (simplify (bor ty (bxor ty (bxor ty z x) y) (bxor ty z x))) (bor ty (bxor ty x z) y))
401(rule (simplify (bor ty (bxor ty z x) (bxor ty y (bxor ty z x)))) (bor ty (bxor ty x z) y))
402(rule (simplify (bor ty (bxor ty y (bxor ty z x)) (bxor ty z x))) (bor ty (bxor ty x z) y))
403
404; x | (x ^ y) --> x | y
405(rule (simplify (bor ty x (bxor ty x y))) (bor ty x y))
406(rule (simplify (bor ty (bxor ty x y) x)) (bor ty x y))
407(rule (simplify (bor ty x (bxor ty y x))) (bor ty x y))
408(rule (simplify (bor ty (bxor ty y x) x)) (bor ty x y))
409
410; ~((~x) + y) --> x - y
411(rule (simplify (bnot ty (iadd ty (bnot ty x) y))) (isub ty x y))
412(rule (simplify (bnot ty (iadd ty y (bnot ty x)))) (isub ty x y))
413
414; (x ^ z) | (y | x) --> (y | x) | z
415(rule (simplify (bor ty (bxor ty x z) (bor ty y x))) (bor ty (bor ty y x) z))
416(rule (simplify (bor ty (bor ty y x) (bxor ty x z))) (bor ty (bor ty y x) z))
417(rule (simplify (bor ty (bxor ty x z) (bor ty x y))) (bor ty (bor ty y x) z))
418(rule (simplify (bor ty (bor ty x y) (bxor ty x z))) (bor ty (bor ty y x) z))
419(rule (simplify (bor ty (bxor ty z x) (bor ty y x))) (bor ty (bor ty y x) z))
420(rule (simplify (bor ty (bor ty y x) (bxor ty z x))) (bor ty (bor ty y x) z))
421(rule (simplify (bor ty (bxor ty z x) (bor ty x y))) (bor ty (bor ty y x) z))
422(rule (simplify (bor ty (bor ty x y) (bxor ty z x))) (bor ty (bor ty y x) z))
423
424; (x | y) ^ (x ^ y) --> x & y
425(rule (simplify (bxor ty (bor ty y x) (bxor ty y x))) (band ty x y))
426(rule (simplify (bxor ty (bxor ty y x) (bor ty y x))) (band ty x y))
427(rule (simplify (bxor ty (bor ty y x) (bxor ty x y))) (band ty x y))
428(rule (simplify (bxor ty (bxor ty x y) (bor ty y x))) (band ty x y))
429(rule (simplify (bxor ty (bor ty x y) (bxor ty y x))) (band ty x y))
430(rule (simplify (bxor ty (bxor ty y x) (bor ty x y))) (band ty x y))
431(rule (simplify (bxor ty (bor ty x y) (bxor ty x y))) (band ty x y))
432(rule (simplify (bxor ty (bxor ty x y) (bor ty x y))) (band ty x y))
433
434; x | (z & (x ^ y)) --> x | (z & y)
435(rule (simplify (bor ty (band ty (bxor ty y x) z) x)) (bor ty (band ty y z) x))
436(rule (simplify (bor ty x (band ty (bxor ty y x) z))) (bor ty (band ty y z) x))
437(rule (simplify (bor ty (band ty z (bxor ty y x)) x)) (bor ty (band ty y z) x))
438(rule (simplify (bor ty x (band ty z (bxor ty y x)))) (bor ty (band ty y z) x))
439(rule (simplify (bor ty (band ty (bxor ty x y) z) x)) (bor ty (band ty y z) x))
440(rule (simplify (bor ty x (band ty (bxor ty x y) z))) (bor ty (band ty y z) x))
441(rule (simplify (bor ty (band ty z (bxor ty x y)) x)) (bor ty (band ty y z) x))
442(rule (simplify (bor ty x (band ty z (bxor ty x y)))) (bor ty (band ty y z) x))
443
444; (x | y) | (x ^ z) --> (x | y) | z
445(rule (simplify (bor ty (bor ty x y) (bxor ty x z))) (bor ty (bor ty x y) z))
446(rule (simplify (bor ty (bxor ty x z) (bor ty x y))) (bor ty (bor ty x y) z))
447(rule (simplify (bor ty (bor ty x y) (bxor ty z x))) (bor ty (bor ty x y) z))
448(rule (simplify (bor ty (bxor ty z x) (bor ty x y))) (bor ty (bor ty x y) z))
449(rule (simplify (bor ty (bor ty y x) (bxor ty x z))) (bor ty (bor ty x y) z))
450(rule (simplify (bor ty (bxor ty x z) (bor ty y x))) (bor ty (bor ty x y) z))
451(rule (simplify (bor ty (bor ty y x) (bxor ty z x))) (bor ty (bor ty x y) z))
452(rule (simplify (bor ty (bxor ty z x) (bor ty y x))) (bor ty (bor ty x y) z))
453
454; (x ^ z) != (y ^ z) --> x != y
455(rule (simplify (ne ty (bxor cty x z) (bxor cty y z))) (ne ty x y))
456(rule (simplify (ne ty (bxor cty y z) (bxor cty x z))) (ne ty x y))
457(rule (simplify (ne ty (bxor cty x z) (bxor cty z y))) (ne ty x y))
458(rule (simplify (ne ty (bxor cty z y) (bxor cty x z))) (ne ty x y))
459(rule (simplify (ne ty (bxor cty z x) (bxor cty y z))) (ne ty x y))
460(rule (simplify (ne ty (bxor cty y z) (bxor cty z x))) (ne ty x y))
461(rule (simplify (ne ty (bxor cty z x) (bxor cty z y))) (ne ty x y))
462(rule (simplify (ne ty (bxor cty z y) (bxor cty z x))) (ne ty x y))
463
464; (x & y) | (x & ~y) --> x
465(rule (simplify (bor ty (band ty x y) (band ty x (bnot ty y)))) x)
466(rule (simplify (bor ty (band ty x (bnot ty y)) (band ty x y))) x)
467(rule (simplify (bor ty (band ty x y) (band ty (bnot ty y) x))) x)
468(rule (simplify (bor ty (band ty (bnot ty y) x) (band ty x y))) x)
469(rule (simplify (bor ty (band ty y x) (band ty x (bnot ty y)))) x)
470(rule (simplify (bor ty (band ty x (bnot ty y)) (band ty y x))) x)
471(rule (simplify (bor ty (band ty y x) (band ty (bnot ty y) x))) x)
472(rule (simplify (bor ty (band ty (bnot ty y) x) (band ty y x))) x)
473
474; (x | y) & (x | ~y) --> x
475(rule (simplify (band ty (bor ty x y) (bor ty x (bnot ty y)))) x)
476(rule (simplify (band ty (bor ty x (bnot ty y)) (bor ty x y))) x)
477(rule (simplify (band ty (bor ty x y) (bor ty (bnot ty y) x))) x)
478(rule (simplify (band ty (bor ty (bnot ty y) x) (bor ty x y))) x)
479(rule (simplify (band ty (bor ty y x) (bor ty x (bnot ty y)))) x)
480(rule (simplify (band ty (bor ty x (bnot ty y)) (bor ty y x))) x)
481(rule (simplify (band ty (bor ty y x) (bor ty (bnot ty y) x))) x)
482(rule (simplify (band ty (bor ty (bnot ty y) x) (bor ty y x))) x)
483
484; (x ^ y) | ~x --> ~(x & y)
485(rule (simplify (bor ty (bxor ty y x) (bnot ty x))) (bnot ty (band ty y x)))
486(rule (simplify (bor ty (bnot ty x) (bxor ty y x))) (bnot ty (band ty y x)))
487(rule (simplify (bor ty (bxor ty x y) (bnot ty x))) (bnot ty (band ty y x)))
488(rule (simplify (bor ty (bnot ty x) (bxor ty x y))) (bnot ty (band ty y x)))
489
490; (x ^ y) ^ x --> y
491(rule (simplify (bxor ty (bxor ty x y) x)) y)
492(rule (simplify (bxor ty x (bxor ty x y))) y)
493(rule (simplify (bxor ty (bxor ty y x) x)) y)
494(rule (simplify (bxor ty x (bxor ty y x))) y)
495
496; y | (x & (y | z)) --> y | (x & z)
497(rule (simplify (bor ty (band ty x (bor ty y z)) y)) (bor ty (band ty x z) y))
498(rule (simplify (bor ty y (band ty x (bor ty y z)))) (bor ty (band ty x z) y))
499(rule (simplify (bor ty (band ty (bor ty y z) x) y)) (bor ty (band ty x z) y))
500(rule (simplify (bor ty y (band ty (bor ty y z) x))) (bor ty (band ty x z) y))
501(rule (simplify (bor ty (band ty x (bor ty z y)) y)) (bor ty (band ty x z) y))
502(rule (simplify (bor ty y (band ty x (bor ty z y)))) (bor ty (band ty x z) y))
503(rule (simplify (bor ty (band ty (bor ty z y) x) y)) (bor ty (band ty x z) y))
504(rule (simplify (bor ty y (band ty (bor ty z y) x))) (bor ty (band ty x z) y))
505
506; y & (x | (y & z)) --> y & (x | z)
507(rule (simplify (band ty (bor ty x (band ty y z)) y)) (band ty (bor ty x z) y))
508(rule (simplify (band ty y (bor ty x (band ty y z)))) (band ty (bor ty x z) y))
509(rule (simplify (band ty (bor ty (band ty y z) x) y)) (band ty (bor ty x z) y))
510(rule (simplify (band ty y (bor ty (band ty y z) x))) (band ty (bor ty x z) y))
511(rule (simplify (band ty (bor ty x (band ty z y)) y)) (band ty (bor ty x z) y))
512(rule (simplify (band ty y (bor ty x (band ty z y)))) (band ty (bor ty x z) y))
513(rule (simplify (band ty (bor ty (band ty z y) x) y)) (band ty (bor ty x z) y))
514(rule (simplify (band ty y (bor ty (band ty z y) x))) (band ty (bor ty x z) y))
515
516; y | (x ^ (y & z)) --> x | y
517(rule (simplify (bor ty (bxor ty x (band ty y z)) y)) (bor ty x y))
518(rule (simplify (bor ty y (bxor ty x (band ty y z)))) (bor ty x y))
519(rule (simplify (bor ty (bxor ty (band ty y z) x) y)) (bor ty x y))
520(rule (simplify (bor ty y (bxor ty (band ty y z) x))) (bor ty x y))
521(rule (simplify (bor ty (bxor ty x (band ty z y)) y)) (bor ty x y))
522(rule (simplify (bor ty y (bxor ty x (band ty z y)))) (bor ty x y))
523(rule (simplify (bor ty (bxor ty (band ty z y) x) y)) (bor ty x y))
524(rule (simplify (bor ty y (bxor ty (band ty z y) x))) (bor ty x y))
525
526; ((x & y) ^ y) + z --> (y + z) - (x & y)
527(rule (simplify (iadd ty (bxor ty (band ty x y) y) z)) (isub ty (iadd ty y z) (band ty x y)))
528(rule (simplify (iadd ty z (bxor ty (band ty x y) y))) (isub ty (iadd ty y z) (band ty x y)))
529(rule (simplify (iadd ty (bxor ty y (band ty x y)) z)) (isub ty (iadd ty y z) (band ty x y)))
530(rule (simplify (iadd ty z (bxor ty y (band ty x y)))) (isub ty (iadd ty y z) (band ty x y)))
531(rule (simplify (iadd ty (bxor ty (band ty y x) y) z)) (isub ty (iadd ty y z) (band ty x y)))
532(rule (simplify (iadd ty z (bxor ty (band ty y x) y))) (isub ty (iadd ty y z) (band ty x y)))
533(rule (simplify (iadd ty (bxor ty y (band ty y x)) z)) (isub ty (iadd ty y z) (band ty x y)))
534(rule (simplify (iadd ty z (bxor ty y (band ty y x)))) (isub ty (iadd ty y z) (band ty x y)))
535
536; y & (~y | x) --> y & x
537(rule (simplify (band ty y (bor ty (bnot ty y) x))) (band ty y x))
538(rule (simplify (band ty (bor ty (bnot ty y) x) y)) (band ty y x))
539(rule (simplify (band ty y (bor ty x (bnot ty y)))) (band ty y x))
540(rule (simplify (band ty (bor ty x (bnot ty y)) y)) (band ty y x))
541
542; y | (~y & x) --> y | x
543(rule (simplify (bor ty y (band ty (bnot ty y) x))) (bor ty y x))
544(rule (simplify (bor ty (band ty (bnot ty y) x) y)) (bor ty y x))
545(rule (simplify (bor ty y (band ty x (bnot ty y)))) (bor ty y x))
546(rule (simplify (bor ty (band ty x (bnot ty y)) y)) (bor ty y x))
547
548;; ((x & ~y) - (x & y)) --> ((x ^ y) - y)
549(rule (simplify (isub ty (band ty x (bnot ty y)) (band ty x y))) (isub ty (bxor ty x y) y))
550(rule (simplify (isub ty (band ty x (bnot ty y)) (band ty y x))) (isub ty (bxor ty x y) y))
551(rule (simplify (isub ty (band ty (bnot ty y) x) (band ty x y))) (isub ty (bxor ty x y) y))
552(rule (simplify (isub ty (band ty (bnot ty y) x) (band ty y x))) (isub ty (bxor ty x y) y))
553(rule (simplify (isub ty (band ty x y) (band ty x (bnot ty y)))) (isub ty y (bxor ty x y)))
554(rule (simplify (isub ty (band ty x y) (band ty (bnot ty y) x))) (isub ty y (bxor ty x y)))
555(rule (simplify (isub ty (band ty y x) (band ty x (bnot ty y)))) (isub ty y (bxor ty x y)))
556(rule (simplify (isub ty (band ty y x) (band ty (bnot ty y) x))) (isub ty y (bxor ty x y)))
557
558;; (x & ~y) | (~x & y) --> (x ^ y)
559(rule (simplify (bor ty (band ty x (bnot ty y)) (band ty (bnot ty x) y))) (bxor ty x y))
560(rule (simplify (bor ty (band ty (bnot ty x) y) (band ty x (bnot ty y)))) (bxor ty x y))
561(rule (simplify (bor ty (band ty x (bnot ty y)) (band ty y (bnot ty x)))) (bxor ty x y))
562(rule (simplify (bor ty (band ty y (bnot ty x)) (band ty x (bnot ty y)))) (bxor ty x y))
563(rule (simplify (bor ty (band ty (bnot ty y) x) (band ty (bnot ty x) y))) (bxor ty x y))
564(rule (simplify (bor ty (band ty (bnot ty x) y) (band ty (bnot ty y) x))) (bxor ty x y))
565(rule (simplify (bor ty (band ty (bnot ty y) x) (band ty y (bnot ty x)))) (bxor ty x y))
566(rule (simplify (bor ty (band ty y (bnot ty x)) (band ty (bnot ty y) x))) (bxor ty x y))
567
568;; (x & ~y) | (x ^ y) --> (x ^ y)
569(rule (simplify (bor ty (band ty x (bnot ty y)) (bxor ty x y))) (bxor ty x y))
570(rule (simplify (bor ty (bxor ty x y) (band ty x (bnot ty y)))) (bxor ty x y))
571(rule (simplify (bor ty (band ty x (bnot ty y)) (bxor ty y x))) (bxor ty x y))
572(rule (simplify (bor ty (bxor ty y x) (band ty x (bnot ty y)))) (bxor ty x y))
573(rule (simplify (bor ty (band ty (bnot ty y) x) (bxor ty x y))) (bxor ty x y))
574(rule (simplify (bor ty (bxor ty x y) (band ty (bnot ty y) x))) (bxor ty x y))
575(rule (simplify (bor ty (band ty (bnot ty y) x) (bxor ty y x))) (bxor ty x y))
576(rule (simplify (bor ty (bxor ty y x) (band ty (bnot ty y) x))) (bxor ty x y))
577
578;; (x & ~y) ^ ~x --> ~(x & y)
579(rule (simplify (bxor ty (band ty x (bnot ty y)) (bnot ty x))) (bnot ty (band ty x y)))
580(rule (simplify (bxor ty (bnot ty x) (band ty x (bnot ty y)))) (bnot ty (band ty x y)))
581(rule (simplify (bxor ty (band ty (bnot ty y) x) (bnot ty x))) (bnot ty (band ty x y)))
582(rule (simplify (bxor ty (bnot ty x) (band ty (bnot ty y) x))) (bnot ty (band ty x y)))
583
584;; (~x & y) ^ x --> x | y
585(rule (simplify (bxor ty (band ty (bnot ty x) y) x)) (bor ty x y))
586(rule (simplify (bxor ty x (band ty (bnot ty x) y))) (bor ty x y))
587(rule (simplify (bxor ty (band ty y (bnot ty x)) x)) (bor ty x y))
588(rule (simplify (bxor ty x (band ty y (bnot ty x)))) (bor ty x y))
589
590;; (x | y) & ~(x ^ y) --> x & y
591(rule (simplify (band ty (bor ty x y) (bnot ty (bxor ty x y)))) (band ty x y))
592(rule (simplify (band ty (bnot ty (bxor ty x y)) (bor ty x y))) (band ty x y))
593(rule (simplify (band ty (bor ty x y) (bnot ty (bxor ty y x)))) (band ty x y))
594(rule (simplify (band ty (bnot ty (bxor ty y x)) (bor ty x y))) (band ty x y))
595(rule (simplify (band ty (bor ty y x) (bnot ty (bxor ty x y)))) (band ty x y))
596(rule (simplify (band ty (bnot ty (bxor ty x y)) (bor ty y x))) (band ty x y))
597(rule (simplify (band ty (bor ty y x) (bnot ty (bxor ty y x)))) (band ty x y))
598(rule (simplify (band ty (bnot ty (bxor ty y x)) (bor ty y x))) (band ty x y))
599
600;; x | ~(x ^ y) --> x | ~y
601(rule (simplify (bor ty x (bnot ty (bxor ty x y)))) (bor ty x (bnot ty y)))
602(rule (simplify (bor ty (bnot ty (bxor ty x y)) x)) (bor ty x (bnot ty y)))
603(rule (simplify (bor ty x (bnot ty (bxor ty y x)))) (bor ty x (bnot ty y)))
604(rule (simplify (bor ty (bnot ty (bxor ty y x)) x)) (bor ty x (bnot ty y)))
605
606;; x | ((~x) ^ y) --> x | ~y
607(rule (simplify (bor ty x (bxor ty (bnot ty x) y))) (bor ty x (bnot ty y)))
608(rule (simplify (bor ty (bxor ty (bnot ty x) y) x)) (bor ty x (bnot ty y)))
609(rule (simplify (bor ty x (bxor ty y (bnot ty x)))) (bor ty x (bnot ty y)))
610(rule (simplify (bor ty (bxor ty y (bnot ty x)) x)) (bor ty x (bnot ty y)))
611
612;; x & ~(x ^ y) --> x & y
613(rule (simplify (band ty x (bnot ty (bxor ty x y)))) (band ty x y))
614(rule (simplify (band ty (bnot ty (bxor ty x y)) x)) (band ty x y))
615(rule (simplify (band ty x (bnot ty (bxor ty y x)))) (band ty x y))
616(rule (simplify (band ty (bnot ty (bxor ty y x)) x)) (band ty x y))
617
618;; x & ((~x) ^ y) --> x & y
619(rule (simplify (band ty x (bxor ty (bnot ty x) y))) (band ty x y))
620(rule (simplify (band ty (bxor ty (bnot ty x) y) x)) (band ty x y))
621(rule (simplify (band ty x (bxor ty y (bnot ty x)))) (band ty x y))
622(rule (simplify (band ty (bxor ty y (bnot ty x)) x)) (band ty x y))
623
624;; (x | y) | (x ^ y) --> (x | y)
625(rule (simplify (bor ty (bor ty x y) (bxor ty x y))) (bor ty x y))
626(rule (simplify (bor ty (bxor ty x y) (bor ty x y))) (bor ty x y))
627(rule (simplify (bor ty (bor ty x y) (bxor ty y x))) (bor ty x y))
628(rule (simplify (bor ty (bxor ty y x) (bor ty x y))) (bor ty x y))
629(rule (simplify (bor ty (bor ty y x) (bxor ty x y))) (bor ty x y))
630(rule (simplify (bor ty (bxor ty x y) (bor ty y x))) (bor ty x y))
631(rule (simplify (bor ty (bor ty y x) (bxor ty y x))) (bor ty x y))
632(rule (simplify (bor ty (bxor ty y x) (bor ty y x))) (bor ty x y))
633
634;; (x ^ y) & (x ^ (y ^ z)) --> (x ^ y) & ~z
635(rule (simplify (band ty (bxor ty x y) (bxor ty (bxor ty y z) x))) (band ty (bxor ty x y) (bnot ty z)))
636(rule (simplify (band ty (bxor ty (bxor ty y z) x) (bxor ty x y))) (band ty (bxor ty x y) (bnot ty z)))
637(rule (simplify (band ty (bxor ty x y) (bxor ty x (bxor ty y z)))) (band ty (bxor ty x y) (bnot ty z)))
638(rule (simplify (band ty (bxor ty x (bxor ty y z)) (bxor ty x y))) (band ty (bxor ty x y) (bnot ty z)))
639(rule (simplify (band ty (bxor ty x y) (bxor ty (bxor ty z y) x))) (band ty (bxor ty x y) (bnot ty z)))
640(rule (simplify (band ty (bxor ty (bxor ty z y) x) (bxor ty x y))) (band ty (bxor ty x y) (bnot ty z)))
641(rule (simplify (band ty (bxor ty x y) (bxor ty x (bxor ty z y)))) (band ty (bxor ty x y) (bnot ty z)))
642(rule (simplify (band ty (bxor ty x (bxor ty z y)) (bxor ty x y))) (band ty (bxor ty x y) (bnot ty z)))
643(rule (simplify (band ty (bxor ty y x) (bxor ty (bxor ty y z) x))) (band ty (bxor ty x y) (bnot ty z)))
644(rule (simplify (band ty (bxor ty (bxor ty y z) x) (bxor ty y x))) (band ty (bxor ty x y) (bnot ty z)))
645(rule (simplify (band ty (bxor ty y x) (bxor ty x (bxor ty y z)))) (band ty (bxor ty x y) (bnot ty z)))
646(rule (simplify (band ty (bxor ty x (bxor ty y z)) (bxor ty y x))) (band ty (bxor ty x y) (bnot ty z)))
647(rule (simplify (band ty (bxor ty y x) (bxor ty (bxor ty z y) x))) (band ty (bxor ty x y) (bnot ty z)))
648(rule (simplify (band ty (bxor ty (bxor ty z y) x) (bxor ty y x))) (band ty (bxor ty x y) (bnot ty z)))
649(rule (simplify (band ty (bxor ty y x) (bxor ty x (bxor ty z y)))) (band ty (bxor ty x y) (bnot ty z)))
650(rule (simplify (band ty (bxor ty x (bxor ty z y)) (bxor ty y x))) (band ty (bxor ty x y) (bnot ty z)))
651
652;; (~x & y) ^ z --> (x & y) ^ (z ^ y)
653(rule (simplify (bxor ty (band ty (bnot ty x) y) z)) (bxor ty (band ty x y) (bxor ty z y)))
654(rule (simplify (bxor ty z (band ty (bnot ty x) y))) (bxor ty (band ty x y) (bxor ty z y)))
655(rule (simplify (bxor ty (band ty y (bnot ty x)) z)) (bxor ty (band ty x y) (bxor ty z y)))
656(rule (simplify (bxor ty z (band ty y (bnot ty x)))) (bxor ty (band ty x y) (bxor ty z y)))
657
658;; ~x - ~y --> y - x
659(rule (simplify (isub ty (bnot ty x) (bnot ty y))) (isub ty y x))
660
661;; (~x & y) | ~(x | y) --> ~x
662(rule (simplify (bor ty (band ty (bnot ty x) y) (bnot ty (bor ty x y)))) (bnot ty x))
663(rule (simplify (bor ty (bnot ty (bor ty x y)) (band ty (bnot ty x) y))) (bnot ty x))
664(rule (simplify (bor ty (band ty (bnot ty x) y) (bnot ty (bor ty y x)))) (bnot ty x))
665(rule (simplify (bor ty (bnot ty (bor ty y x)) (band ty (bnot ty x) y))) (bnot ty x))
666(rule (simplify (bor ty (band ty y (bnot ty x)) (bnot ty (bor ty x y)))) (bnot ty x))
667(rule (simplify (bor ty (bnot ty (bor ty x y)) (band ty y (bnot ty x)))) (bnot ty x))
668(rule (simplify (bor ty (band ty y (bnot ty x)) (bnot ty (bor ty y x)))) (bnot ty x))
669(rule (simplify (bor ty (bnot ty (bor ty y x)) (band ty y (bnot ty x)))) (bnot ty x))
670
671;; (~x | y) & ~(x & y) --> ~x
672(rule (simplify (band ty (bor ty (bnot ty x) y) (bnot ty (band ty x y)))) (bnot ty x))
673(rule (simplify (band ty (bnot ty (band ty x y)) (bor ty (bnot ty x) y))) (bnot ty x))
674(rule (simplify (band ty (bor ty (bnot ty x) y) (bnot ty (band ty y x)))) (bnot ty x))
675(rule (simplify (band ty (bnot ty (band ty y x)) (bor ty (bnot ty x) y))) (bnot ty x))
676(rule (simplify (band ty (bor ty y (bnot ty x)) (bnot ty (band ty x y)))) (bnot ty x))
677(rule (simplify (band ty (bnot ty (band ty x y)) (bor ty y (bnot ty x)))) (bnot ty x))
678(rule (simplify (band ty (bor ty y (bnot ty x)) (bnot ty (band ty y x)))) (bnot ty x))
679(rule (simplify (band ty (bnot ty (band ty y x)) (bor ty y (bnot ty x)))) (bnot ty x))
680
681;; (x & y) | ~(x | y) --> ~(x ^ y)
682(rule (simplify (bor ty (band ty x y) (bnot ty (bor ty x y)))) (bnot ty (bxor ty x y)))
683(rule (simplify (bor ty (bnot ty (bor ty x y)) (band ty x y))) (bnot ty (bxor ty x y)))
684(rule (simplify (bor ty (band ty x y) (bnot ty (bor ty y x)))) (bnot ty (bxor ty x y)))
685(rule (simplify (bor ty (bnot ty (bor ty y x)) (band ty x y))) (bnot ty (bxor ty x y)))
686(rule (simplify (bor ty (band ty y x) (bnot ty (bor ty x y)))) (bnot ty (bxor ty x y)))
687(rule (simplify (bor ty (bnot ty (bor ty x y)) (band ty y x))) (bnot ty (bxor ty x y)))
688(rule (simplify (bor ty (band ty y x) (bnot ty (bor ty y x)))) (bnot ty (bxor ty x y)))
689(rule (simplify (bor ty (bnot ty (bor ty y x)) (band ty y x))) (bnot ty (bxor ty x y)))
690
691;; (~x | y) ^ (x ^ y) --> x | ~y
692(rule (simplify (bxor ty (bor ty (bnot ty x) y) (bxor ty x y))) (bor ty x (bnot ty y)))
693(rule (simplify (bxor ty (bxor ty x y) (bor ty (bnot ty x) y))) (bor ty x (bnot ty y)))
694(rule (simplify (bxor ty (bor ty (bnot ty x) y) (bxor ty y x))) (bor ty x (bnot ty y)))
695(rule (simplify (bxor ty (bxor ty y x) (bor ty (bnot ty x) y))) (bor ty x (bnot ty y)))
696(rule (simplify (bxor ty (bor ty y (bnot ty x)) (bxor ty x y))) (bor ty x (bnot ty y)))
697(rule (simplify (bxor ty (bxor ty x y) (bor ty y (bnot ty x)))) (bor ty x (bnot ty y)))
698(rule (simplify (bxor ty (bor ty y (bnot ty x)) (bxor ty y x))) (bor ty x (bnot ty y)))
699(rule (simplify (bxor ty (bxor ty y x) (bor ty y (bnot ty x)))) (bor ty x (bnot ty y)))