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