我想解决的公式在 C 中如下所示:
#define foo(w,x,y) ((((w)*(x)*(y)+31) & ~31) / 8)
WORD w,x,y,z;
y = 24;
if( (foo(w,x,y) * z) == -1 )
printf("yeah!");
我通过以下方式将其重写为 z3py:
from z3 import *
w= BitVec('w',16)
x= BitVec('x',16)
z= BitVec('z',16)
y= BitVecVal(24,16)
solve( (UDiv( (w*x*y+31) & ~31, 8 )) * z == 0xffffffff)
有什么建议么 ?
PS:请注意,尝试以这种形式求解公式:
solve( (UDiv( (w*x*y+31), 8 )) * z == 0xffffffff)
是可能的,所以我不能相信按位运算会导致这个公式无法满足。