;; Rewrites for `band`, `bnot`, `bor`, `bxor`
;; x | 0 == x | x == x.
(rule (simplify (bor ty
x
(iconst_u ty 0)))
(subsume x))
(rule (simplify (bor ty x x))
(subsume x))
;; x ^ 0 == x.
(rule (simplify (bxor ty
x
(iconst_u ty 0)))
(subsume x))
;; x ^ x == 0.
(rule (simplify (bxor (ty_int ty) x x))
(subsume (iconst_u ty 0)))
;; x ^ not(x) == not(x) ^ x == x | not(x) == not(x) | x == -1.
;; This identity also holds for non-integer types, vectors, and wider types.
(rule (simplify (bxor (ty_int ty) x (bnot ty x))) (subsume (iconst_s ty -1)))
(rule (simplify (bxor (ty_int ty) (bnot ty x) x)) (subsume (iconst_s ty -1)))
(rule (simplify (bor (ty_int ty) x (bnot ty x))) (subsume (iconst_s ty -1)))
(rule (simplify (bor (ty_int ty) (bnot ty x) x)) (subsume (iconst_s ty -1)))
;; x & x == x & -1 == x.
(rule (simplify (band ty x x)) (subsume x))
(rule (simplify (band ty x (iconst_s ty -1)))
(subsume x))
;; x & 0 == x & not(x) == not(x) & x == 0.
(rule (simplify (band ty _ zero @ (iconst_u ty 0))) (subsume zero))
(rule (simplify (band (ty_int ty) x (bnot ty x))) (subsume (iconst_u ty 0)))
(rule (simplify (band (ty_int ty) (bnot ty x) x)) (subsume (iconst_u ty 0)))
;; (x & y) ^ (x ^ y) == x | y
(rule (simplify (bxor ty (band ty X Y) (bxor ty X Y))) (bor ty X Y))
;; not(not(x)) == x.
(rule (simplify (bnot ty (bnot ty x))) (subsume x))
;; `or(and(x, y), not(y)) == or(x, not(y))`
(rule (simplify (bor ty
(band ty x y)
z @ (bnot ty y)))
(bor ty x z))
;; Duplicate the rule but swap the `bor` operands because `bor` is
;; commutative. We could, of course, add a `simplify` rule to do the commutative
;; swap for all `bor`s but this will bloat the e-graph with many e-nodes. It is
;; cheaper to have additional rules, rather than additional e-nodes, because we
;; amortize their cost via ISLE's smart codegen.
(rule (simplify (bor ty
z @ (bnot ty y)
(band ty x y)))
(bor ty x z))
;; `or(and(x, y), not(y)) == or(x, not(y))` specialized for constants, since
;; otherwise we may not know that `z == not(y)` since we don't generally expand
;; constants in the e-graph.
;;
;; (No need to duplicate for commutative `bor` for this constant version because
;; we move constants to the right.)
(rule (simplify (bor ty
(band ty x (iconst_u ty y))
z @ (iconst_u ty zk)))
(if-let true (u64_eq (u64_and (ty_mask ty) zk)
(u64_and (ty_mask ty) (u64_not y))))
(bor ty x z))
;; (x ^ -1) can be replaced with the `bnot` instruction
(rule (simplify (bxor ty x (iconst_s ty -1)))
(bnot ty x))
;; sshr((x | -x), N) == bmask(x) where N = ty_bits(ty) - 1.
;;
;; (x | -x) sets the sign bit to 1 if x is nonzero, and 0 if x is zero. sshr propagates
;; the sign bit to the rest of the value.
(rule (simplify (sshr ty (bor ty x (ineg ty x)) (iconst_u ty shift_amt)))
(if-let true (u64_eq shift_amt (ty_shift_mask ty)))
(bmask ty x))
(rule (simplify (sshr ty (bor ty (ineg ty x) x) (iconst_u ty shift_amt)))
(if-let true (u64_eq shift_amt (ty_shift_mask ty)))
(bmask ty x))
;; Since icmp is always 0 or 1, bmask is just a negation.
;; TODO: Explore whether this makes sense for things needing extension too.
(rule (simplify (bmask $I8 cmp@(icmp $I8 _ _ _)))
(ineg $I8 cmp))
;; Matches any expressions that preserve "truthiness".
;; i.e. If the input is zero it remains zero, and if it is nonzero it can have
;; a different value as long as it is still nonzero.
(decl pure multi truthy (Value) Value)
(rule (truthy (sextend _ x)) x)
(rule (truthy (uextend _ x)) x)
(rule (truthy (bmask _ x)) x)
(rule (truthy (ineg _ x)) x)
(rule (truthy (bswap _ x)) x)
(rule (truthy (bitrev _ x)) x)
(rule (truthy (popcnt _ x)) x)
(rule (truthy (rotl _ x _)) x)
(rule (truthy (rotr _ x _)) x)
(rule (truthy (select _ x (iconst_u _ (u64_when_non_zero)) (iconst_u _ 0))) x)
;; (ne ty (iconst 0) v) is also canonicalized into this form via another rule
(rule (truthy (ne _ x (iconst_u _ 0))) x)
;; All of these expressions don't care about their input as long as it is truthy.
;; so we can remove expressions that preserve that property from the input.
(rule (simplify (bmask ty v)) (if-let x (truthy v)) (bmask ty x))
(rule (simplify (select ty v t f)) (if-let c (truthy v)) (select ty c t f))
;; (ne ty (iconst 0) v) is also canonicalized into this form via another rule
(rule (simplify (ne cty v (iconst_u _ 0)))
(if-let c (truthy v))
(if-let (value_type (ty_int_ref_scalar_64 ty)) c)
(ne cty c (iconst_u ty 0)))
;; (sextend (bmask x)) can be replaced with (bmask x) since bmask
;; supports any size of output type, regardless of input.
;; Same with `ireduce`
(rule (simplify (sextend ty (bmask _ x))) (bmask ty x))
(rule (simplify (ireduce ty (bmask _ x))) (bmask ty x))
;; (bswap (bswap x)) == x
(rule (simplify (bswap ty (bswap ty x))) (subsume x))
;; (bitrev (bitrev x)) == x
(rule (simplify (bitrev ty (bitrev ty x))) (subsume x))
;; WebAssembly doesn't have a native byte-swapping instruction at this time so
;; languages which have a byte-swapping operation will compile it down to bit
;; shifting and twiddling. This attempts to pattern match what LLVM currently
;; generates today for the Rust code `a.swap_bytes()`. This might be a bit
;; brittle over time and/or with other possible LLVM backend optimizations, but
;; it's at least one way to generate a byte swap.
;;
;; Technically this could be permuted quite a few ways and currently there's no
;; easy way to match all of them, so only one is matched here.
(rule (simplify (bor ty @ $I32
(bor ty
(ishl ty x (iconst_u ty 24))
(ishl ty
(band ty x (iconst_u ty 0xff00))
(iconst_u ty 8)))
(bor ty
(band ty
(ushr ty x (iconst_u ty 8))
(iconst_u ty 0xff00))
(ushr ty x (iconst_u ty 24)))))
(bswap ty x))
(rule (simplify (bor ty @ $I64
(bor ty
(bor ty
(ishl ty x (iconst_u ty 56))
(ishl ty
(band ty x (iconst_u ty 0xff00))
(iconst_u ty 40)))
(bor ty
(ishl ty
(band ty x (iconst_u ty 0xff_0000))
(iconst_u ty 24))
(ishl ty
(band ty x (iconst_u ty 0xff00_0000))
(iconst_u ty 8))))
(bor ty
(bor ty
(band ty
(ushr ty x (iconst_u ty 8))
(iconst_u ty 0xff00_0000))
(band ty
(ushr ty x (iconst_u ty 24))
(iconst_u ty 0xff_0000)))
(bor ty
(band ty
(ushr ty x (iconst_u ty 40))
(iconst_u ty 0xff00))
(ushr ty x (iconst_u ty 56))))))
(bswap ty x))
(rule (simplify (bxor ty (bor ty x y) (band ty x y))) (bxor ty x y))
(rule (simplify (bor ty (bor ty x y) x)) (bor ty x y))
(rule (simplify (bor ty (bor ty x y) y)) (bor ty x y))
(rule (simplify (bor ty x (bor ty x y))) (bor ty x y))
(rule (simplify (bor ty y (bor ty x y))) (bor ty x y))
(rule (simplify (band ty (band ty x y) x)) (band ty x y))
(rule (simplify (band ty (band ty x y) y)) (band ty x y))
(rule (simplify (band ty x (band ty x y))) (band ty x y))
(rule (simplify (band ty y (band ty x y))) (band ty x y))
;; (x ^ ~y) & x --> x & y
(rule (simplify (band ty (bxor ty x (bnot ty y)) x)) (band ty x y))
(rule (simplify (band ty (bxor ty (bnot ty y) x) x)) (band ty x y))
(rule (simplify (band ty x (bxor ty x (bnot ty y)))) (band ty x y))
(rule (simplify (band ty x (bxor ty (bnot ty y) x))) (band ty x y))
; (x & y) + (x ^ y) --> x | y
(rule (simplify (iadd ty (band ty x y) (bxor ty x y))) (bor ty x y))
(rule (simplify (iadd ty (bxor ty x y) (band ty x y))) (bor ty x y))
; (x | y) + (x & y) --> x + y
(rule (simplify (iadd ty (bor ty x y) (band ty x y))) (iadd ty x y))
(rule (simplify (iadd ty (band ty x y) (bor ty x y))) (iadd ty x y))
; (x & y) | x --> x
(rule (simplify (bor ty (band ty x y) x)) x)
(rule (simplify (bor ty x (band ty x y))) x)
; (x ^ y) ^ y --> x
(rule (simplify (bxor ty (bxor ty x y) y)) x)
(rule (simplify (bxor ty y (bxor ty x y))) x)
; (x & y) | ~x -> y | ~x
(rule (simplify (bor ty (band ty x y) (bnot ty x))) (bor ty y (bnot ty x)))
(rule (simplify (bor ty (bnot ty x) (band ty x y))) (bor ty y (bnot ty x)))
; (z & x) ^ (z & y) => z & (x ^ y)
(rule (simplify
(bxor ty (band ty z x) (band ty z y)))
(band ty z (bxor ty x y)))
; (x & y) | ~(x ^ y) => ~(x ^ y)
(rule (simplify (bor ty (band ty x y) (bnot ty (bxor ty x y)))) (bnot ty (bxor ty x y)))
(rule (simplify (bor ty (bnot ty (bxor ty x y)) (band ty x y))) (bnot ty (bxor ty x y)))
(rule (simplify (bor ty (band ty x y) (bnot ty (bxor ty y x)))) (bnot ty (bxor ty x y)))
(rule (simplify (bor ty (bnot ty (bxor ty y x)) (band ty x y))) (bnot ty (bxor ty x y)))
(rule (simplify (bor ty (band ty y x) (bnot ty (bxor ty x y)))) (bnot ty (bxor ty x y)))
(rule (simplify (bor ty (bnot ty (bxor ty x y)) (band ty y x))) (bnot ty (bxor ty x y)))
(rule (simplify (bor ty (band ty y x) (bnot ty (bxor ty y x)))) (bnot ty (bxor ty x y)))
(rule (simplify (bor ty (bnot ty (bxor ty y x)) (band ty y x))) (bnot ty (bxor ty x y)))
; (x | y) + (-y) --> x & ~y
(rule (simplify (iadd ty (bor ty x y) (ineg ty y)))
(band ty x (bnot ty y)))
(rule (simplify (iadd ty (ineg ty y) (bor ty x y)))
(band ty x (bnot ty y)))
(rule (simplify (iadd ty (bor ty y x) (ineg ty y)))
(band ty x (bnot ty y)))
(rule (simplify (iadd ty (ineg ty y) (bor ty y x)))
(band ty x (bnot ty y)))
; x & (x | y) --> x
(rule (simplify (band ty (bor ty x y) x)) x)
(rule (simplify (band ty x (bor ty x y))) x)
(rule (simplify (band ty (bor ty y x) x)) x)
(rule (simplify (band ty x (bor ty y x))) x)
; (x | z) & (y | z) --> (x & y) | z
(rule (simplify (band ty (bor ty x z) (bor ty y z))) (bor ty (band ty x y) z))
(rule (simplify (band ty (bor ty y z) (bor ty x z))) (bor ty (band ty x y) z))
(rule (simplify (band ty (bor ty x z) (bor ty z y))) (bor ty (band ty x y) z))
(rule (simplify (band ty (bor ty z y) (bor ty x z))) (bor ty (band ty x y) z))
(rule (simplify (band ty (bor ty z x) (bor ty y z))) (bor ty (band ty x y) z))
(rule (simplify (band ty (bor ty y z) (bor ty z x))) (bor ty (band ty x y) z))
(rule (simplify (band ty (bor ty z x) (bor ty z y))) (bor ty (band ty x y) z))
(rule (simplify (band ty (bor ty z y) (bor ty z x))) (bor ty (band ty x y) z))
; (x & z) | (y & z) --> (x | y) & z
(rule (simplify (bor ty (band ty x z) (band ty y z))) (band ty (bor ty x y) z))
(rule (simplify (bor ty (band ty y z) (band ty x z))) (band ty (bor ty x y) z))
(rule (simplify (bor ty (band ty x z) (band ty z y))) (band ty (bor ty x y) z))
(rule (simplify (bor ty (band ty z y) (band ty x z))) (band ty (bor ty x y) z))
(rule (simplify (bor ty (band ty z x) (band ty y z))) (band ty (bor ty x y) z))
(rule (simplify (bor ty (band ty y z) (band ty z x))) (band ty (bor ty x y) z))
(rule (simplify (bor ty (band ty z x) (band ty z y))) (band ty (bor ty x y) z))
(rule (simplify (bor ty (band ty z y) (band ty z x))) (band ty (bor ty x y) z))
; (x | y) ^ (x | ~y) --> ~x
(rule (simplify (bxor ty (bor ty x y) (bor ty x (bnot ty y)))) (bnot ty x))
(rule (simplify (bxor ty (bor ty x (bnot ty y)) (bor ty x y))) (bnot ty x))
(rule (simplify (bxor ty (bor ty x y) (bor ty (bnot ty y) x))) (bnot ty x))
(rule (simplify (bxor ty (bor ty (bnot ty y) x) (bor ty x y))) (bnot ty x))
(rule (simplify (bxor ty (bor ty y x) (bor ty x (bnot ty y)))) (bnot ty x))
(rule (simplify (bxor ty (bor ty x (bnot ty y)) (bor ty y x))) (bnot ty x))
(rule (simplify (bxor ty (bor ty y x) (bor ty (bnot ty y) x))) (bnot ty x))
(rule (simplify (bxor ty (bor ty (bnot ty y) x) (bor ty y x))) (bnot ty x))
; (~x) & (~y) --> ~(x | y)
(rule (simplify (band ty (bnot ty x) (bnot ty y))) (bnot ty (bor ty x y)))
(rule (simplify (band ty (bnot ty y) (bnot ty x))) (bnot ty (bor ty x y)))
; (~x) | (~y) --> ~(x & y)
(rule (simplify (bor ty (bnot ty x) (bnot ty y))) (bnot ty (band ty x y)))
(rule (simplify (bor ty (bnot ty y) (bnot ty x))) (bnot ty (band ty x y)))
; x | ((x ^ y) ^ z) --> x | (y ^ z)
(rule (simplify (bor ty (bxor ty (bxor ty x y) z) x)) (bor ty (bxor ty y z) x))
(rule (simplify (bor ty x (bxor ty (bxor ty x y) z))) (bor ty (bxor ty y z) x))
(rule (simplify (bor ty (bxor ty z (bxor ty x y)) x)) (bor ty (bxor ty y z) x))
(rule (simplify (bor ty x (bxor ty z (bxor ty x y)))) (bor ty (bxor ty y z) x))
(rule (simplify (bor ty (bxor ty (bxor ty y x) z) x)) (bor ty (bxor ty y z) x))
(rule (simplify (bor ty x (bxor ty (bxor ty y x) z))) (bor ty (bxor ty y z) x))
(rule (simplify (bor ty (bxor ty z (bxor ty y x)) x)) (bor ty (bxor ty y z) x))
(rule (simplify (bor ty x (bxor ty z (bxor ty y x)))) (bor ty (bxor ty y z) x))
; (x ^ z) == (y ^ z) --> x == y
(rule (simplify (eq ty (bxor cty x z) (bxor cty y z))) (eq ty x y))
(rule (simplify (eq ty (bxor cty y z) (bxor cty x z))) (eq ty x y))
(rule (simplify (eq ty (bxor cty x z) (bxor cty z y))) (eq ty x y))
(rule (simplify (eq ty (bxor cty z y) (bxor cty x z))) (eq ty x y))
(rule (simplify (eq ty (bxor cty z x) (bxor cty y z))) (eq ty x y))
(rule (simplify (eq ty (bxor cty y z) (bxor cty z x))) (eq ty x y))
(rule (simplify (eq ty (bxor cty z x) (bxor cty z y))) (eq ty x y))
(rule (simplify (eq ty (bxor cty z y) (bxor cty z x))) (eq ty x y))
; y | ~(x | y) --> y | ~x
(rule (simplify (bor ty y (bnot ty (bor ty x y)))) (bor ty y (bnot ty x)))
(rule (simplify (bor ty (bnot ty (bor ty x y)) y)) (bor ty y (bnot ty x)))
(rule (simplify (bor ty y (bnot ty (bor ty y x)))) (bor ty y (bnot ty x)))
(rule (simplify (bor ty (bnot ty (bor ty y x)) y)) (bor ty y (bnot ty x)))
; y & ~(x & y) --> y & ~x
(rule (simplify (band ty y (bnot ty (band ty x y)))) (band ty y (bnot ty x)))
(rule (simplify (band ty (bnot ty (band ty x y)) y)) (band ty y (bnot ty x)))
(rule (simplify (band ty y (bnot ty (band ty y x)))) (band ty y (bnot ty x)))
(rule (simplify (band ty (bnot ty (band ty y x)) y)) (band ty y (bnot ty x)))
; (~x) ^ (x | y) --> x | ~y
(rule (simplify (bxor ty (bnot ty x) (bor ty x y))) (bor ty x (bnot ty y)))
(rule (simplify (bxor ty (bor ty x y) (bnot ty x))) (bor ty x (bnot ty y)))
(rule (simplify (bxor ty (bnot ty x) (bor ty y x))) (bor ty x (bnot ty y)))
(rule (simplify (bxor ty (bor ty y x) (bnot ty x))) (bor ty x (bnot ty y)))
; (x < y) | (x > y) --> x != y
(rule (simplify (bor ty (slt ty x y) (sgt ty x y))) (ne ty x y))
(rule (simplify (bor ty (sgt ty x y) (slt ty x y))) (ne ty x y))
(rule (simplify (bor ty (slt ty x y) (slt ty y x))) (ne ty x y))
(rule (simplify (bor ty (slt ty y x) (slt ty x y))) (ne ty x y))
(rule (simplify (bor ty (sgt ty y x) (sgt ty x y))) (ne ty x y))
(rule (simplify (bor ty (sgt ty x y) (sgt ty y x))) (ne ty x y))
(rule (simplify (bor ty (sgt ty y x) (slt ty y x))) (ne ty x y))
(rule (simplify (bor ty (slt ty y x) (sgt ty y x))) (ne ty x y))
; (x <_u y) | (x >_u y) --> x != y
(rule (simplify (bor ty (ult ty x y) (ugt ty x y))) (ne ty x y))
(rule (simplify (bor ty (ugt ty x y) (ult ty x y))) (ne ty x y))
(rule (simplify (bor ty (ult ty x y) (ult ty y x))) (ne ty x y))
(rule (simplify (bor ty (ult ty y x) (ult ty x y))) (ne ty x y))
(rule (simplify (bor ty (ugt ty y x) (ugt ty x y))) (ne ty x y))
(rule (simplify (bor ty (ugt ty x y) (ugt ty y x))) (ne ty x y))
(rule (simplify (bor ty (ugt ty y x) (ult ty y x))) (ne ty x y))
(rule (simplify (bor ty (ult ty y x) (ugt ty y x))) (ne ty x y))
; ~((~x) & y) --> x | ~y
(rule (simplify (bnot ty (band ty (bnot ty x) y))) (bor ty x (bnot ty y)))
(rule (simplify (bnot ty (band ty y (bnot ty x)))) (bor ty x (bnot ty y)))
; ~((~x) | y) --> x & ~y
(rule (simplify (bnot ty (bor ty (bnot ty x) y))) (band ty x (bnot ty y)))
(rule (simplify (bnot ty (bor ty y (bnot ty x)))) (band ty x (bnot ty y)))
; (x <_u y) | (x == y) --> (x <=_u y)
(rule (simplify (bor ty (ult ty x y) (eq ty x y))) (ule ty x y))
(rule (simplify (bor ty (eq ty x y) (ult ty x y))) (ule ty x y))
(rule (simplify (bor ty (ult ty x y) (eq ty y x))) (ule ty x y))
(rule (simplify (bor ty (eq ty y x) (ult ty x y))) (ule ty x y))
; (y >_u x) | (x == y) --> (x <=_u y)
(rule (simplify (bor ty (ugt ty y x) (eq ty x y))) (ule ty x y))
(rule (simplify (bor ty (eq ty x y) (ugt ty y x))) (ule ty x y))
(rule (simplify (bor ty (ugt ty y x) (eq ty y x))) (ule ty x y))
(rule (simplify (bor ty (eq ty y x) (ugt ty y x))) (ule ty x y))
; (x < y) | (x == y) --> (x <= y)
(rule (simplify (bor ty (slt ty x y) (eq ty x y))) (sle ty x y))
(rule (simplify (bor ty (eq ty x y) (slt ty x y))) (sle ty x y))
(rule (simplify (bor ty (slt ty x y) (eq ty y x))) (sle ty x y))
(rule (simplify (bor ty (eq ty y x) (slt ty x y))) (sle ty x y))
; (y > x) | (x == y) --> (x <= y)
(rule (simplify (bor ty (sgt ty y x) (eq ty x y))) (sle ty x y))
(rule (simplify (bor ty (eq ty x y) (sgt ty y x))) (sle ty x y))
(rule (simplify (bor ty (sgt ty y x) (eq ty y x))) (sle ty x y))
(rule (simplify (bor ty (eq ty y x) (sgt ty y x))) (sle ty x y))
; (x ^ z) | (((x ^ z) ^ y)) --> (x ^ z) | y
(rule (simplify (bor ty (bxor ty x z) (bxor ty (bxor ty x z) y))) (bor ty (bxor ty x z) y))
(rule (simplify (bor ty (bxor ty (bxor ty x z) y) (bxor ty x z))) (bor ty (bxor ty x z) y))
(rule (simplify (bor ty (bxor ty x z) (bxor ty y (bxor ty x z)))) (bor ty (bxor ty x z) y))
(rule (simplify (bor ty (bxor ty y (bxor ty x z)) (bxor ty x z))) (bor ty (bxor ty x z) y))
(rule (simplify (bor ty (bxor ty x z) (bxor ty (bxor ty z x) y))) (bor ty (bxor ty x z) y))
(rule (simplify (bor ty (bxor ty (bxor ty z x) y) (bxor ty x z))) (bor ty (bxor ty x z) y))
(rule (simplify (bor ty (bxor ty x z) (bxor ty y (bxor ty z x)))) (bor ty (bxor ty x z) y))
(rule (simplify (bor ty (bxor ty y (bxor ty z x)) (bxor ty x z))) (bor ty (bxor ty x z) y))
(rule (simplify (bor ty (bxor ty z x) (bxor ty (bxor ty x z) y))) (bor ty (bxor ty x z) y))
(rule (simplify (bor ty (bxor ty (bxor ty x z) y) (bxor ty z x))) (bor ty (bxor ty x z) y))
(rule (simplify (bor ty (bxor ty z x) (bxor ty y (bxor ty x z)))) (bor ty (bxor ty x z) y))
(rule (simplify (bor ty (bxor ty y (bxor ty x z)) (bxor ty z x))) (bor ty (bxor ty x z) y))
(rule (simplify (bor ty (bxor ty z x) (bxor ty (bxor ty z x) y))) (bor ty (bxor ty x z) y))
(rule (simplify (bor ty (bxor ty (bxor ty z x) y) (bxor ty z x))) (bor ty (bxor ty x z) y))
(rule (simplify (bor ty (bxor ty z x) (bxor ty y (bxor ty z x)))) (bor ty (bxor ty x z) y))
(rule (simplify (bor ty (bxor ty y (bxor ty z x)) (bxor ty z x))) (bor ty (bxor ty x z) y))
; x | (x ^ y) --> x | y
(rule (simplify (bor ty x (bxor ty x y))) (bor ty x y))
(rule (simplify (bor ty (bxor ty x y) x)) (bor ty x y))
(rule (simplify (bor ty x (bxor ty y x))) (bor ty x y))
(rule (simplify (bor ty (bxor ty y x) x)) (bor ty x y))
; ~((~x) + y) --> x - y
(rule (simplify (bnot ty (iadd ty (bnot ty x) y))) (isub ty x y))
(rule (simplify (bnot ty (iadd ty y (bnot ty x)))) (isub ty x y))
; (x ^ z) | (y | x) --> (y | x) | z
(rule (simplify (bor ty (bxor ty x z) (bor ty y x))) (bor ty (bor ty y x) z))
(rule (simplify (bor ty (bor ty y x) (bxor ty x z))) (bor ty (bor ty y x) z))
(rule (simplify (bor ty (bxor ty x z) (bor ty x y))) (bor ty (bor ty y x) z))
(rule (simplify (bor ty (bor ty x y) (bxor ty x z))) (bor ty (bor ty y x) z))
(rule (simplify (bor ty (bxor ty z x) (bor ty y x))) (bor ty (bor ty y x) z))
(rule (simplify (bor ty (bor ty y x) (bxor ty z x))) (bor ty (bor ty y x) z))
(rule (simplify (bor ty (bxor ty z x) (bor ty x y))) (bor ty (bor ty y x) z))
(rule (simplify (bor ty (bor ty x y) (bxor ty z x))) (bor ty (bor ty y x) z))
; (x | y) ^ (x ^ y) --> x & y
(rule (simplify (bxor ty (bor ty y x) (bxor ty y x))) (band ty x y))
(rule (simplify (bxor ty (bxor ty y x) (bor ty y x))) (band ty x y))
(rule (simplify (bxor ty (bor ty y x) (bxor ty x y))) (band ty x y))
(rule (simplify (bxor ty (bxor ty x y) (bor ty y x))) (band ty x y))
(rule (simplify (bxor ty (bor ty x y) (bxor ty y x))) (band ty x y))
(rule (simplify (bxor ty (bxor ty y x) (bor ty x y))) (band ty x y))
(rule (simplify (bxor ty (bor ty x y) (bxor ty x y))) (band ty x y))
(rule (simplify (bxor ty (bxor ty x y) (bor ty x y))) (band ty x y))
; x | (z & (x ^ y)) --> x | (z & y)
(rule (simplify (bor ty (band ty (bxor ty y x) z) x)) (bor ty (band ty y z) x))
(rule (simplify (bor ty x (band ty (bxor ty y x) z))) (bor ty (band ty y z) x))
(rule (simplify (bor ty (band ty z (bxor ty y x)) x)) (bor ty (band ty y z) x))
(rule (simplify (bor ty x (band ty z (bxor ty y x)))) (bor ty (band ty y z) x))
(rule (simplify (bor ty (band ty (bxor ty x y) z) x)) (bor ty (band ty y z) x))
(rule (simplify (bor ty x (band ty (bxor ty x y) z))) (bor ty (band ty y z) x))
(rule (simplify (bor ty (band ty z (bxor ty x y)) x)) (bor ty (band ty y z) x))
(rule (simplify (bor ty x (band ty z (bxor ty x y)))) (bor ty (band ty y z) x))
; (x | y) | (x ^ z) --> (x | y) | z
(rule (simplify (bor ty (bor ty x y) (bxor ty x z))) (bor ty (bor ty x y) z))
(rule (simplify (bor ty (bxor ty x z) (bor ty x y))) (bor ty (bor ty x y) z))
(rule (simplify (bor ty (bor ty x y) (bxor ty z x))) (bor ty (bor ty x y) z))
(rule (simplify (bor ty (bxor ty z x) (bor ty x y))) (bor ty (bor ty x y) z))
(rule (simplify (bor ty (bor ty y x) (bxor ty x z))) (bor ty (bor ty x y) z))
(rule (simplify (bor ty (bxor ty x z) (bor ty y x))) (bor ty (bor ty x y) z))
(rule (simplify (bor ty (bor ty y x) (bxor ty z x))) (bor ty (bor ty x y) z))
(rule (simplify (bor ty (bxor ty z x) (bor ty y x))) (bor ty (bor ty x y) z))
; (x ^ z) != (y ^ z) --> x != y
(rule (simplify (ne ty (bxor cty x z) (bxor cty y z))) (ne ty x y))
(rule (simplify (ne ty (bxor cty y z) (bxor cty x z))) (ne ty x y))
(rule (simplify (ne ty (bxor cty x z) (bxor cty z y))) (ne ty x y))
(rule (simplify (ne ty (bxor cty z y) (bxor cty x z))) (ne ty x y))
(rule (simplify (ne ty (bxor cty z x) (bxor cty y z))) (ne ty x y))
(rule (simplify (ne ty (bxor cty y z) (bxor cty z x))) (ne ty x y))
(rule (simplify (ne ty (bxor cty z x) (bxor cty z y))) (ne ty x y))
(rule (simplify (ne ty (bxor cty z y) (bxor cty z x))) (ne ty x y))
; (x & y) | (x & ~y) --> x
(rule (simplify (bor ty (band ty x y) (band ty x (bnot ty y)))) x)
(rule (simplify (bor ty (band ty x (bnot ty y)) (band ty x y))) x)
(rule (simplify (bor ty (band ty x y) (band ty (bnot ty y) x))) x)
(rule (simplify (bor ty (band ty (bnot ty y) x) (band ty x y))) x)
(rule (simplify (bor ty (band ty y x) (band ty x (bnot ty y)))) x)
(rule (simplify (bor ty (band ty x (bnot ty y)) (band ty y x))) x)
(rule (simplify (bor ty (band ty y x) (band ty (bnot ty y) x))) x)
(rule (simplify (bor ty (band ty (bnot ty y) x) (band ty y x))) x)
; (x | y) & (x | ~y) --> x
(rule (simplify (band ty (bor ty x y) (bor ty x (bnot ty y)))) x)
(rule (simplify (band ty (bor ty x (bnot ty y)) (bor ty x y))) x)
(rule (simplify (band ty (bor ty x y) (bor ty (bnot ty y) x))) x)
(rule (simplify (band ty (bor ty (bnot ty y) x) (bor ty x y))) x)
(rule (simplify (band ty (bor ty y x) (bor ty x (bnot ty y)))) x)
(rule (simplify (band ty (bor ty x (bnot ty y)) (bor ty y x))) x)
(rule (simplify (band ty (bor ty y x) (bor ty (bnot ty y) x))) x)
(rule (simplify (band ty (bor ty (bnot ty y) x) (bor ty y x))) x)
; (x ^ y) | ~x --> ~(x & y)
(rule (simplify (bor ty (bxor ty y x) (bnot ty x))) (bnot ty (band ty y x)))
(rule (simplify (bor ty (bnot ty x) (bxor ty y x))) (bnot ty (band ty y x)))
(rule (simplify (bor ty (bxor ty x y) (bnot ty x))) (bnot ty (band ty y x)))
(rule (simplify (bor ty (bnot ty x) (bxor ty x y))) (bnot ty (band ty y x)))
; (x ^ y) ^ x --> y
(rule (simplify (bxor ty (bxor ty x y) x)) y)
(rule (simplify (bxor ty x (bxor ty x y))) y)
(rule (simplify (bxor ty (bxor ty y x) x)) y)
(rule (simplify (bxor ty x (bxor ty y x))) y)
; y | (x & (y | z)) --> y | (x & z)
(rule (simplify (bor ty (band ty x (bor ty y z)) y)) (bor ty (band ty x z) y))
(rule (simplify (bor ty y (band ty x (bor ty y z)))) (bor ty (band ty x z) y))
(rule (simplify (bor ty (band ty (bor ty y z) x) y)) (bor ty (band ty x z) y))
(rule (simplify (bor ty y (band ty (bor ty y z) x))) (bor ty (band ty x z) y))
(rule (simplify (bor ty (band ty x (bor ty z y)) y)) (bor ty (band ty x z) y))
(rule (simplify (bor ty y (band ty x (bor ty z y)))) (bor ty (band ty x z) y))
(rule (simplify (bor ty (band ty (bor ty z y) x) y)) (bor ty (band ty x z) y))
(rule (simplify (bor ty y (band ty (bor ty z y) x))) (bor ty (band ty x z) y))
; y & (x | (y & z)) --> y & (x | z)
(rule (simplify (band ty (bor ty x (band ty y z)) y)) (band ty (bor ty x z) y))
(rule (simplify (band ty y (bor ty x (band ty y z)))) (band ty (bor ty x z) y))
(rule (simplify (band ty (bor ty (band ty y z) x) y)) (band ty (bor ty x z) y))
(rule (simplify (band ty y (bor ty (band ty y z) x))) (band ty (bor ty x z) y))
(rule (simplify (band ty (bor ty x (band ty z y)) y)) (band ty (bor ty x z) y))
(rule (simplify (band ty y (bor ty x (band ty z y)))) (band ty (bor ty x z) y))
(rule (simplify (band ty (bor ty (band ty z y) x) y)) (band ty (bor ty x z) y))
(rule (simplify (band ty y (bor ty (band ty z y) x))) (band ty (bor ty x z) y))
; y | (x ^ (y & z)) --> x | y
(rule (simplify (bor ty (bxor ty x (band ty y z)) y)) (bor ty x y))
(rule (simplify (bor ty y (bxor ty x (band ty y z)))) (bor ty x y))
(rule (simplify (bor ty (bxor ty (band ty y z) x) y)) (bor ty x y))
(rule (simplify (bor ty y (bxor ty (band ty y z) x))) (bor ty x y))
(rule (simplify (bor ty (bxor ty x (band ty z y)) y)) (bor ty x y))
(rule (simplify (bor ty y (bxor ty x (band ty z y)))) (bor ty x y))
(rule (simplify (bor ty (bxor ty (band ty z y) x) y)) (bor ty x y))
(rule (simplify (bor ty y (bxor ty (band ty z y) x))) (bor ty x y))
; ((x & y) ^ y) + z --> (y + z) - (x & y)
(rule (simplify (iadd ty (bxor ty (band ty x y) y) z)) (isub ty (iadd ty y z) (band ty x y)))
(rule (simplify (iadd ty z (bxor ty (band ty x y) y))) (isub ty (iadd ty y z) (band ty x y)))
(rule (simplify (iadd ty (bxor ty y (band ty x y)) z)) (isub ty (iadd ty y z) (band ty x y)))
(rule (simplify (iadd ty z (bxor ty y (band ty x y)))) (isub ty (iadd ty y z) (band ty x y)))
(rule (simplify (iadd ty (bxor ty (band ty y x) y) z)) (isub ty (iadd ty y z) (band ty x y)))
(rule (simplify (iadd ty z (bxor ty (band ty y x) y))) (isub ty (iadd ty y z) (band ty x y)))
(rule (simplify (iadd ty (bxor ty y (band ty y x)) z)) (isub ty (iadd ty y z) (band ty x y)))
(rule (simplify (iadd ty z (bxor ty y (band ty y x)))) (isub ty (iadd ty y z) (band ty x y)))
; y & (~y | x) --> y & x
(rule (simplify (band ty y (bor ty (bnot ty y) x))) (band ty y x))
(rule (simplify (band ty (bor ty (bnot ty y) x) y)) (band ty y x))
(rule (simplify (band ty y (bor ty x (bnot ty y)))) (band ty y x))
(rule (simplify (band ty (bor ty x (bnot ty y)) y)) (band ty y x))
; y | (~y & x) --> y | x
(rule (simplify (bor ty y (band ty (bnot ty y) x))) (bor ty y x))
(rule (simplify (bor ty (band ty (bnot ty y) x) y)) (bor ty y x))
(rule (simplify (bor ty y (band ty x (bnot ty y)))) (bor ty y x))
(rule (simplify (bor ty (band ty x (bnot ty y)) y)) (bor ty y x))
;; ((x & ~y) - (x & y)) --> ((x ^ y) - y)
(rule (simplify (isub ty (band ty x (bnot ty y)) (band ty x y))) (isub ty (bxor ty x y) y))
(rule (simplify (isub ty (band ty x (bnot ty y)) (band ty y x))) (isub ty (bxor ty x y) y))
(rule (simplify (isub ty (band ty (bnot ty y) x) (band ty x y))) (isub ty (bxor ty x y) y))
(rule (simplify (isub ty (band ty (bnot ty y) x) (band ty y x))) (isub ty (bxor ty x y) y))
(rule (simplify (isub ty (band ty x y) (band ty x (bnot ty y)))) (isub ty y (bxor ty x y)))
(rule (simplify (isub ty (band ty x y) (band ty (bnot ty y) x))) (isub ty y (bxor ty x y)))
(rule (simplify (isub ty (band ty y x) (band ty x (bnot ty y)))) (isub ty y (bxor ty x y)))
(rule (simplify (isub ty (band ty y x) (band ty (bnot ty y) x))) (isub ty y (bxor ty x y)))
;; (x & ~y) | (~x & y) --> (x ^ y)
(rule (simplify (bor ty (band ty x (bnot ty y)) (band ty (bnot ty x) y))) (bxor ty x y))
(rule (simplify (bor ty (band ty (bnot ty x) y) (band ty x (bnot ty y)))) (bxor ty x y))
(rule (simplify (bor ty (band ty x (bnot ty y)) (band ty y (bnot ty x)))) (bxor ty x y))
(rule (simplify (bor ty (band ty y (bnot ty x)) (band ty x (bnot ty y)))) (bxor ty x y))
(rule (simplify (bor ty (band ty (bnot ty y) x) (band ty (bnot ty x) y))) (bxor ty x y))
(rule (simplify (bor ty (band ty (bnot ty x) y) (band ty (bnot ty y) x))) (bxor ty x y))
(rule (simplify (bor ty (band ty (bnot ty y) x) (band ty y (bnot ty x)))) (bxor ty x y))
(rule (simplify (bor ty (band ty y (bnot ty x)) (band ty (bnot ty y) x))) (bxor ty x y))
;; (x & ~y) | (x ^ y) --> (x ^ y)
(rule (simplify (bor ty (band ty x (bnot ty y)) (bxor ty x y))) (bxor ty x y))
(rule (simplify (bor ty (bxor ty x y) (band ty x (bnot ty y)))) (bxor ty x y))
(rule (simplify (bor ty (band ty x (bnot ty y)) (bxor ty y x))) (bxor ty x y))
(rule (simplify (bor ty (bxor ty y x) (band ty x (bnot ty y)))) (bxor ty x y))
(rule (simplify (bor ty (band ty (bnot ty y) x) (bxor ty x y))) (bxor ty x y))
(rule (simplify (bor ty (bxor ty x y) (band ty (bnot ty y) x))) (bxor ty x y))
(rule (simplify (bor ty (band ty (bnot ty y) x) (bxor ty y x))) (bxor ty x y))
(rule (simplify (bor ty (bxor ty y x) (band ty (bnot ty y) x))) (bxor ty x y))
;; (x & ~y) ^ ~x --> ~(x & y)
(rule (simplify (bxor ty (band ty x (bnot ty y)) (bnot ty x))) (bnot ty (band ty x y)))
(rule (simplify (bxor ty (bnot ty x) (band ty x (bnot ty y)))) (bnot ty (band ty x y)))
(rule (simplify (bxor ty (band ty (bnot ty y) x) (bnot ty x))) (bnot ty (band ty x y)))
(rule (simplify (bxor ty (bnot ty x) (band ty (bnot ty y) x))) (bnot ty (band ty x y)))
;; (~x & y) ^ x --> x | y
(rule (simplify (bxor ty (band ty (bnot ty x) y) x)) (bor ty x y))
(rule (simplify (bxor ty x (band ty (bnot ty x) y))) (bor ty x y))
(rule (simplify (bxor ty (band ty y (bnot ty x)) x)) (bor ty x y))
(rule (simplify (bxor ty x (band ty y (bnot ty x)))) (bor ty x y))
;; (x | y) & ~(x ^ y) --> x & y
(rule (simplify (band ty (bor ty x y) (bnot ty (bxor ty x y)))) (band ty x y))
(rule (simplify (band ty (bnot ty (bxor ty x y)) (bor ty x y))) (band ty x y))
(rule (simplify (band ty (bor ty x y) (bnot ty (bxor ty y x)))) (band ty x y))
(rule (simplify (band ty (bnot ty (bxor ty y x)) (bor ty x y))) (band ty x y))
(rule (simplify (band ty (bor ty y x) (bnot ty (bxor ty x y)))) (band ty x y))
(rule (simplify (band ty (bnot ty (bxor ty x y)) (bor ty y x))) (band ty x y))
(rule (simplify (band ty (bor ty y x) (bnot ty (bxor ty y x)))) (band ty x y))
(rule (simplify (band ty (bnot ty (bxor ty y x)) (bor ty y x))) (band ty x y))
;; x | ~(x ^ y) --> x | ~y
(rule (simplify (bor ty x (bnot ty (bxor ty x y)))) (bor ty x (bnot ty y)))
(rule (simplify (bor ty (bnot ty (bxor ty x y)) x)) (bor ty x (bnot ty y)))
(rule (simplify (bor ty x (bnot ty (bxor ty y x)))) (bor ty x (bnot ty y)))
(rule (simplify (bor ty (bnot ty (bxor ty y x)) x)) (bor ty x (bnot ty y)))
;; x | ((~x) ^ y) --> x | ~y
(rule (simplify (bor ty x (bxor ty (bnot ty x) y))) (bor ty x (bnot ty y)))
(rule (simplify (bor ty (bxor ty (bnot ty x) y) x)) (bor ty x (bnot ty y)))
(rule (simplify (bor ty x (bxor ty y (bnot ty x)))) (bor ty x (bnot ty y)))
(rule (simplify (bor ty (bxor ty y (bnot ty x)) x)) (bor ty x (bnot ty y)))
;; x & ~(x ^ y) --> x & y
(rule (simplify (band ty x (bnot ty (bxor ty x y)))) (band ty x y))
(rule (simplify (band ty (bnot ty (bxor ty x y)) x)) (band ty x y))
(rule (simplify (band ty x (bnot ty (bxor ty y x)))) (band ty x y))
(rule (simplify (band ty (bnot ty (bxor ty y x)) x)) (band ty x y))
;; x & ((~x) ^ y) --> x & y
(rule (simplify (band ty x (bxor ty (bnot ty x) y))) (band ty x y))
(rule (simplify (band ty (bxor ty (bnot ty x) y) x)) (band ty x y))
(rule (simplify (band ty x (bxor ty y (bnot ty x)))) (band ty x y))
(rule (simplify (band ty (bxor ty y (bnot ty x)) x)) (band ty x y))
;; (x | y) | (x ^ y) --> (x | y)
(rule (simplify (bor ty (bor ty x y) (bxor ty x y))) (bor ty x y))
(rule (simplify (bor ty (bxor ty x y) (bor ty x y))) (bor ty x y))
(rule (simplify (bor ty (bor ty x y) (bxor ty y x))) (bor ty x y))
(rule (simplify (bor ty (bxor ty y x) (bor ty x y))) (bor ty x y))
(rule (simplify (bor ty (bor ty y x) (bxor ty x y))) (bor ty x y))
(rule (simplify (bor ty (bxor ty x y) (bor ty y x))) (bor ty x y))
(rule (simplify (bor ty (bor ty y x) (bxor ty y x))) (bor ty x y))
(rule (simplify (bor ty (bxor ty y x) (bor ty y x))) (bor ty x y))
;; (x ^ y) & (x ^ (y ^ z)) --> (x ^ y) & ~z
(rule (simplify (band ty (bxor ty x y) (bxor ty (bxor ty y z) x))) (band ty (bxor ty x y) (bnot ty z)))
(rule (simplify (band ty (bxor ty (bxor ty y z) x) (bxor ty x y))) (band ty (bxor ty x y) (bnot ty z)))
(rule (simplify (band ty (bxor ty x y) (bxor ty x (bxor ty y z)))) (band ty (bxor ty x y) (bnot ty z)))
(rule (simplify (band ty (bxor ty x (bxor ty y z)) (bxor ty x y))) (band ty (bxor ty x y) (bnot ty z)))
(rule (simplify (band ty (bxor ty x y) (bxor ty (bxor ty z y) x))) (band ty (bxor ty x y) (bnot ty z)))
(rule (simplify (band ty (bxor ty (bxor ty z y) x) (bxor ty x y))) (band ty (bxor ty x y) (bnot ty z)))
(rule (simplify (band ty (bxor ty x y) (bxor ty x (bxor ty z y)))) (band ty (bxor ty x y) (bnot ty z)))
(rule (simplify (band ty (bxor ty x (bxor ty z y)) (bxor ty x y))) (band ty (bxor ty x y) (bnot ty z)))
(rule (simplify (band ty (bxor ty y x) (bxor ty (bxor ty y z) x))) (band ty (bxor ty x y) (bnot ty z)))
(rule (simplify (band ty (bxor ty (bxor ty y z) x) (bxor ty y x))) (band ty (bxor ty x y) (bnot ty z)))
(rule (simplify (band ty (bxor ty y x) (bxor ty x (bxor ty y z)))) (band ty (bxor ty x y) (bnot ty z)))
(rule (simplify (band ty (bxor ty x (bxor ty y z)) (bxor ty y x))) (band ty (bxor ty x y) (bnot ty z)))
(rule (simplify (band ty (bxor ty y x) (bxor ty (bxor ty z y) x))) (band ty (bxor ty x y) (bnot ty z)))
(rule (simplify (band ty (bxor ty (bxor ty z y) x) (bxor ty y x))) (band ty (bxor ty x y) (bnot ty z)))
(rule (simplify (band ty (bxor ty y x) (bxor ty x (bxor ty z y)))) (band ty (bxor ty x y) (bnot ty z)))
(rule (simplify (band ty (bxor ty x (bxor ty z y)) (bxor ty y x))) (band ty (bxor ty x y) (bnot ty z)))
;; (~x & y) ^ z --> (x & y) ^ (z ^ y)
(rule (simplify (bxor ty (band ty (bnot ty x) y) z)) (bxor ty (band ty x y) (bxor ty z y)))
(rule (simplify (bxor ty z (band ty (bnot ty x) y))) (bxor ty (band ty x y) (bxor ty z y)))
(rule (simplify (bxor ty (band ty y (bnot ty x)) z)) (bxor ty (band ty x y) (bxor ty z y)))
(rule (simplify (bxor ty z (band ty y (bnot ty x)))) (bxor ty (band ty x y) (bxor ty z y)))
;; ~x - ~y --> y - x
(rule (simplify (isub ty (bnot ty x) (bnot ty y))) (isub ty y x))
;; (~x & y) | ~(x | y) --> ~x
(rule (simplify (bor ty (band ty (bnot ty x) y) (bnot ty (bor ty x y)))) (bnot ty x))
(rule (simplify (bor ty (bnot ty (bor ty x y)) (band ty (bnot ty x) y))) (bnot ty x))
(rule (simplify (bor ty (band ty (bnot ty x) y) (bnot ty (bor ty y x)))) (bnot ty x))
(rule (simplify (bor ty (bnot ty (bor ty y x)) (band ty (bnot ty x) y))) (bnot ty x))
(rule (simplify (bor ty (band ty y (bnot ty x)) (bnot ty (bor ty x y)))) (bnot ty x))
(rule (simplify (bor ty (bnot ty (bor ty x y)) (band ty y (bnot ty x)))) (bnot ty x))
(rule (simplify (bor ty (band ty y (bnot ty x)) (bnot ty (bor ty y x)))) (bnot ty x))
(rule (simplify (bor ty (bnot ty (bor ty y x)) (band ty y (bnot ty x)))) (bnot ty x))
;; (~x | y) & ~(x & y) --> ~x
(rule (simplify (band ty (bor ty (bnot ty x) y) (bnot ty (band ty x y)))) (bnot ty x))
(rule (simplify (band ty (bnot ty (band ty x y)) (bor ty (bnot ty x) y))) (bnot ty x))
(rule (simplify (band ty (bor ty (bnot ty x) y) (bnot ty (band ty y x)))) (bnot ty x))
(rule (simplify (band ty (bnot ty (band ty y x)) (bor ty (bnot ty x) y))) (bnot ty x))
(rule (simplify (band ty (bor ty y (bnot ty x)) (bnot ty (band ty x y)))) (bnot ty x))
(rule (simplify (band ty (bnot ty (band ty x y)) (bor ty y (bnot ty x)))) (bnot ty x))
(rule (simplify (band ty (bor ty y (bnot ty x)) (bnot ty (band ty y x)))) (bnot ty x))
(rule (simplify (band ty (bnot ty (band ty y x)) (bor ty y (bnot ty x)))) (bnot ty x))
;; (x & y) | ~(x | y) --> ~(x ^ y)
(rule (simplify (bor ty (band ty x y) (bnot ty (bor ty x y)))) (bnot ty (bxor ty x y)))
(rule (simplify (bor ty (bnot ty (bor ty x y)) (band ty x y))) (bnot ty (bxor ty x y)))
(rule (simplify (bor ty (band ty x y) (bnot ty (bor ty y x)))) (bnot ty (bxor ty x y)))
(rule (simplify (bor ty (bnot ty (bor ty y x)) (band ty x y))) (bnot ty (bxor ty x y)))
(rule (simplify (bor ty (band ty y x) (bnot ty (bor ty x y)))) (bnot ty (bxor ty x y)))
(rule (simplify (bor ty (bnot ty (bor ty x y)) (band ty y x))) (bnot ty (bxor ty x y)))
(rule (simplify (bor ty (band ty y x) (bnot ty (bor ty y x)))) (bnot ty (bxor ty x y)))
(rule (simplify (bor ty (bnot ty (bor ty y x)) (band ty y x))) (bnot ty (bxor ty x y)))
;; (~x | y) ^ (x ^ y) --> x | ~y
(rule (simplify (bxor ty (bor ty (bnot ty x) y) (bxor ty x y))) (bor ty x (bnot ty y)))
(rule (simplify (bxor ty (bxor ty x y) (bor ty (bnot ty x) y))) (bor ty x (bnot ty y)))
(rule (simplify (bxor ty (bor ty (bnot ty x) y) (bxor ty y x))) (bor ty x (bnot ty y)))
(rule (simplify (bxor ty (bxor ty y x) (bor ty (bnot ty x) y))) (bor ty x (bnot ty y)))
(rule (simplify (bxor ty (bor ty y (bnot ty x)) (bxor ty x y))) (bor ty x (bnot ty y)))
(rule (simplify (bxor ty (bxor ty x y) (bor ty y (bnot ty x)))) (bor ty x (bnot ty y)))
(rule (simplify (bxor ty (bor ty y (bnot ty x)) (bxor ty y x))) (bor ty x (bnot ty y)))
(rule (simplify (bxor ty (bxor ty y x) (bor ty y (bnot ty x)))) (bor ty x (bnot ty y)))