Hi All,
This patch implements transform for pattern (A|B) ^(A^B)  to  A&B.
Please find the correctness proof of the transform using CVC3 -
$ cat t.cvc
A, B : BITVECTOR(32);
QUERY BVXOR(A | B, BVXOR(A,B) ) = A & B;
$ cvc3  t.cvc
Valid.
Please let me know if this is good to commit.
Thanks
Karthik Bhat
I think this would be simpler as:
} else if (match(Op0, m_Xor(m_Specific(A), m_Specific(B)))) { I.swapOperands(); // (A^B)^(A|B) == (A|B)^(A^B) std::swap(Op0, Op1); // Simplified below. } else if (match(Op0, m_Xor(m_Specific(B), m_Specific(A)))) { Op1I->swapOperands(); // (A^B)^(B|A) == (A|B)^(A^B) I.swapOperands(); // Simplied below. std::swap(Op0, Op1);You would avoid needing A1 and B1 *and* you could avoid hoisting Op0I.