I’m working on a Boolean Algebra Rewriter with SymbolicUtils.jl, and I’ve noticed that for some reason, associativity and commutativity are not being properly applied for Boolean operations, which makes defining rules painful. I’m wondering if I’m missing something or if there is some way to manually tell SymbolicUtils to apply associativity/commutativity to boolean operations.
To clarify: I need to write these rules
@acrule((~a & ~b) & ~a => ~a & ~b)
@acrule((~a & ~b) & ~b => ~a & ~b)
If I only write the first one, then (A & B) & B has no change.
Furthermore, I have to define:
@acrule((~a & ~b & ~c) & ~a => ~a & ~b & ~c)
@acrule((~a & (~b & ~c)) & ~a => ~a & ~b & ~c)
If I only define the first one, then (A & (B & C)) & A doesn’t simplify.