Jestem nowy w Z3 i sprawdzałem samouczek online python.Sprawdź przepełnienie za pomocą Z3
Potem pomyślałem, że mogę sprawdzić zachowanie przepełnienia w BitVecs.
NapisaĹ,em ten kod:
x = BitVec('x', 3)
y = Int('y')
solve(BV2Int(x) == y, Not(BV2Int(x + 1) == (y + 1)))
i oczekiwał [Y = 7, x = 7] (to znaczy, gdy wartości są takie same, ale następcy nie ponieważ x + 1 będzie wynosiła 0, y + 1 będzie 8)
Ale odpowiedzi Z3 [y = 0, x = 0].
Co robię źle?
Nie sądzę, że robisz coś złego, wygląda BV2Int jest wadliwy:
x = BitVec('x', 3)
prove(x <= 3)
prove(BV2Int(x) <= 3)
Z3py udowadnia pierwszy, ale daje kontrprzykład x=0 na sekundę. To nie brzmi dobrze. (Jedynym wyjaśnieniem może być dziwna rzecz Pythona, ale nie rozumiem.)
Należy również zauważyć, że otrzymany model będzie zależał od tego, czy + traktuje wektor bitowy jako liczbę podpisaną w powiązaniach Pythona, w moim przekonaniu. Jednak BV2Int może tego nie robić, traktując to jako wartość bez znaku. To dodatkowo komplikowałoby sprawy.
W każdym razie wygląda na to, że BV2Int nie jest całkiem koszerny; Trzymałbym się z dala od tego, dopóki nie pojawi się oficjalna odpowiedź od ludzi Z3.
Dla innych, którzy są tym zaniepokojeni, wydaje się, że zostało to rozwiązane w pewnym momencie. Właśnie powtórzyłem ten przykład z najnowszą wersją Z3 (kilka lat po pierwszym wpisie) i zwraca 7,7.