;; 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)))