函数根据参数返回错误值（Z3，Python）

Question

我正在使用简单函数 (Tab) 模拟一个数组，但它没有按预期工作。如果我在 SMT2 中编写代码，它运行良好，但在 Z3py 中它不起作用。

from z3 import *

A = BitVec('A', 8)
B1 = BitVec('B1', 8)
B2 = BitVec('B2', 8)
B3 = BitVec('B3', 8)
B4 = BitVec('B4', 8)

# Emulate Array
def Tab(N):
  if N == 0x01: return B1
  if N == 0x02: return B2
  if N == 0x03: return B3
  if N == 0x04: return B4

s = Solver()
s.add(A == 0x01)
s.add(Tab(A + 0x02) == 0x09 )
s.check()
m = s.model()

print (m)
print("Pos:", m.eval(A + 0x02))
print("Tab(3a):", m.eval(Tab(A + 0x02)))
print("Tab(3):", m.eval(Tab(0x03)))
print("B1: ", m[B1])
print("B2: ", m[B2])
print("B3: ", m[B3])
print("B4: ", m[B4])
print("B3n:", m.eval(B3))

输出：

[B1 = 9, A = 1] <- Model
Pos: 3          <- this is OK
Tab(3a): 9      <- this is OK (based on our condition)
Tab(3):  B3     <- why does this return name B3? (should return None or 9)
B1:  9          <- this is BAD, here should be None
B2:  None
B3:  None       <- this is BAD, here should be 9
B4:  None
B3n: B3         <- why does this return name B3?! (should return None or 9)

从输出中我们看到 Tab 总是为参数 0x03 返回 B1 而不是 B3。看起来 A + 0x02 被计算为 0x01 用作参数。我做错了什么，还是一些 Z3py 实现错误？还是这与 BitVec 术语的工作方式有关？

Answer 1

这看起来与这篇文章中的问题相同：How to correctly use Solver() command in Python API of Z3 with declared function。

问题在于if N == 0x01: ... 没有创建Z3 if-then-else 表达式；它从字面上检查N 是否是一个具体值为1 的Python-int。要获得所需的表达式，您需要使用Z3 的If(...) function。