Функция возвращает отрицательное значение на основе параметра (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 всегда возвращает B1 для параметра 0x03 вместо 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 Python-int конкретным значением 1. Чтобы получить желаемое выражение, вам нужно использовать Z3's If(...) function.