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:
You would avoid needing A1 and B1 *and* you could avoid hoisting Op0I.