(just some very quick comments, they may be off, and I haven't looked
closely)
On Tue, 11 Sep 2018, MCC CS wrote:
+/* (~x & y) | ~(x | y) -> ~x */
+(simplify
+ (bit_ior:c (bit_and:c (bit_not @0) @1) (bit_not (bit_ior:s @0 @1)))
+ (bit_not @0))
Did you mean :c instead of :s?
You should write (bit_not@2 @0) in the input, then the output can be just
@2.
+/* (x | y) ^ (x | ~y) -> ~x */
+(simplify
+ (bit_xor:c (bit_ior:s @0 @1) (bit_ior:c @0 (bit_not @1)))
+ (bit_not @0))
:s -> :c again?
+/* (x & y) | ~(x | y) -> ~(x ^ y) */
+(simplify
+ (bit_ior:c (bit_and:s @0 @1) (bit_not (bit_ior:s @0 @1)))
+ (bit_not (bit_xor @0 @1)))
Probably add :s to bit_not as well?
+/* (~x | y) ^ (x ^ y) -> x | ~y */
+(simplify
+ (bit_xor:c (bit_ior:c (bit_not @0) @1) (bit_xor:s @0 @1))
+ (bit_ior @0 (bit_not @1)))
:c on the last bit_xor.
If we have some :s, having one just on the last bit_xor seems strange.
+/* (x ^ y) | ~(x | y) -> ~(x & y) */
+(simplify
+ (bit_ior:c (bit_xor:s @0 @1) (bit_not (bit_ior:s @0 @1)))
+ (bit_not (bit_and @0 @1)))
bit_not:s
--
Marc Glisse
