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