1from opcodes import DIV, SHL, SHR
2from rule import Rule
3from z3 import BitVec
4
5"""
6Rule:
7DIV(X, SHL(Y, 1)) -> SHR(Y, X)
8Requirements:
9"""
10
11rule = Rule()
12
13n_bits = 32
14
15# Input vars
16X = BitVec('X', n_bits)
17Y = BitVec('Y', n_bits)
18
19# Non optimized result
20nonopt = DIV(X, SHL(Y, 1))
21
22# Optimized result
23opt = SHR(Y, X)
24
25rule.check(nonopt, opt)
26