Какие значения могут быть представлены с BitVecs в z3?

Question

Я думаю, что я не понимаю, как BitVecs работает в z3. Я написал следующий код:

>>> import z3
>>> s = z3.Solver()
>>> a = z3.BitVec("a", 32)
>>> s.add(z3.ForAll(a, z3.Not(z3.And(a > 2147483647, a < 2147484671))))

Я ожидаю, что это будет "ненадежным", потому что есть значения внутри и за пределами этого диапазона. Но когда я бегу s.check(), Я получил:

>>> s.check()
sat

Это сбивало меня с толку, поэтому я догадался, что это переполнение. Но потом я попробовал:

>>> b = z3.BitVec("b", 32)
>>> s = z3.Solver()
>>> s.add(b == 2147484671)
>>> s.check()
sat
>>> s.model()
[b = 2147484671]

Это меня сильно смущает, поскольку предполагает, что z3 может смоделировать это число, используя 32-битные бит-коды. Дополнительно я побежал:

>>> s = z3.Solver()
>>> c = z3.BitVec("c", 32)
>>> s.add(z3.And(c > 2147483647, c < 2147484671))
>>> s.check()
unsat

Что еще больше смутило меня, потому что оно кажется явно несовместимым со вторым примером...

Answer 1

Операторы> и <подписаны. 2147484671 является отрицательным числом при интерпретации как 32-разрядное число. Вот почему вы ограничены. Вы можете использовать UGT / ULT вместо> / <, чтобы игнорировать знаковый бит.

Итог: битовые векторы представляют числа, но вам нужно знать, какова подпись используемых вами операций. В Python API все перегрузки операторов являются подписанными операциями.