1from opcodes import AND, OR 2from rule import Rule 3from z3 import BitVec 4 5 6""" 7Rule: 8AND(OR(AND(X, A), Y), B) -> OR(AND(X, A & B), AND(Y, B)) 9""" 10 11rule = Rule() 12 13# bit width is irrelevant 14n_bits = 128 15 16# Input vars 17X = BitVec('X', n_bits) 18Y = BitVec('Y', n_bits) 19A = BitVec('A', n_bits) 20B = BitVec('B', n_bits) 21 22# Non optimized result, explicit form 23nonopt = AND(OR(AND(X, A), Y), B) 24 25# Optimized result 26opt = OR(AND(X, A & B), AND(Y, B)) 27 28rule.check(nonopt, opt) 29 30# Now the forms as they are constructod in the code. 31for inner in [AND(X, A), AND(A, X)]: 32 for second in [OR(inner, Y), OR(Y, inner)]: 33 rule.check(AND(second, B), opt) 34 rule.check(AND(B, second), opt) 35