Merge pull request #413 from pysmt/examples/xor

Examples: Equivalence checking of XOR rewriting

examples/README.rst

@@ -16,3 +16,4 @@ This directory contains examples to get you started using pySMT. Suggested order
 11. `parallel.py </examples/parallel.py>`_ : Shows how to use multi-processing to perform parallel and asynchronous solving
 12. `smtlib.py </examples/smtlib.py>`_ : Demonstrates how to perform SMT-LIB parsing, dumping and extension
 13. `einstein.py </examples/einstein.py>`_ : Shows the use of UNSAT Core as debugging tools
+14. `xor.py </examples/xor.py>`_ : Equivalence checking of XOR rewriting using BitVectors

examples/xor.py

@@ -0,0 +1,24 @@
+# Verify the correctness of a rewriting using Bit-Vectors
+#
+# The following expression computes the xor of y and x:
+#  (((y & x)*-2) + (y + x)
+#
+# We verify that this is indeed the case
+#
+# Source: https://yurichev.com/writings/SAT_SMT_draft-EN.pdf
+#
+from pysmt.shortcuts import SBV, Symbol, is_valid, Equals
+from pysmt.typing import BV16
+
+# X and Y are BV of width 16
+x = Symbol("x", BV16)
+y = Symbol("y", BV16)
+
+r1 = y + x            # add   r1,ry,rx
+r2 = y & x            # and   r2,ry,rx
+r3 = r2 * SBV(-2, 16) # mul   r3,r2,-2
+r4 = r3 + r1          # add   r4,r3,r1
+
+# x xor y == r4
+real_xor = x ^ y
+assert is_valid(real_xor.Equals(r4))