I implemented logical expressions using a binary tree in C++. Now I want to be able to simplify such an expression using rules like e.g.
but have issues with the commutativity. Assuming the expression is
then the tree would look like this:
xor /\ xor b /\ xor true /\ true a
The expression can be simplified:
but I don't know how to apply the above rule to this tree since it is never directly applicable to one of the subtrees. Is there a better way than having to rotate the tree in all possible orders?