Permalink
Browse files

Examples: Equivalence checking of XOR rewriting

  • Loading branch information...
marcogario committed Jun 5, 2017
1 parent b6257b3 commit 09ef97a0c765a61306b9ba87cbe05b0c92661e53
Showing with 25 additions and 0 deletions.
  1. +1 −0 examples/README.rst
  2. +24 −0 examples/xor.py
View
@@ -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
View
@@ -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))

0 comments on commit 09ef97a

Please sign in to comment.