python - z3python 多个 pow 条件加法

问题描述

我正在使用 z3 并且遇到以下问题，我想根据当前测试值输出结果。

例如：

from z3 import *
# This returns a statement
def arrayF(y):
    return If(y % 8 == 7, 255, If(y % 8 == 6, 127, If(y % 8 == 5, 63, If(y % 8 == 4, 31, If(y % 8 == 3, 15, If(y % 8 == 2, 7, If(y % 8 == 1, 3, If(y % 8 == 0, 1, 0))))))))

KEY_LEN = 16
solver = Solver()
pbInput = [BitVec("{}".format(i), 8) for i in range(KEY_LEN)]
for i in range(KEY_LEN):
    solver.add(ascii_printable(pbInput[i]))
# 255 value is taken randomly, not sure there is a solution, this is not the poblem
solver.add(((0x11 &  arrayF(pbInput[1])) << (8 - (pbInput[1] % 8))) + (0x11 + pbInput[1]) == 255)

这给出了以下回溯：

Traceback (most recent call last):
  File "solve.py", line 12, in <module>
    solver.add(((0x11 &  arrayF(pbInput[1])) << (8 - (pbInput[1] % 8))) + (0x11 + pbInput[1]))  == 255
TypeError: unsupported operand type(s) for &: 'int' and 'instance'

这当然是因为我没有从我的函数中返回一个值。我的问题是：我怎么能设法从我的函数返回一个值，这取决于输入实例值？

这就是大回报的假设

def arrayF(y):
   z = 0
   for i in range(y):  # not possible as y in an instance, not an int
        z += pow(2, y)
   return z

标签： pythonz3z3py

你真的需要发布代码段，人们可以自己尝试看看发生了什么！无法破译你真正追求的东西。

话虽如此，问题在于您的range(y). 由于显而易见的原因，您无法计算符号值的范围。是y8位值吗？如果是这种情况，那么您只有 256 个输入；所以我建议建立一个查找表并简单地查找它。即使它达到 16 位左右，我也会这样做；任何更大的东西可能都不实用。但是请在提问时发布 MVCE，请参见此处：https ://stackoverflow.com/help/minimal-reproducible-example

python - z3python 多个 pow 条件加法

问题描述

解决方案

推荐阅读