Функция подтверждения Z3Py возвращает неверный контрпример - PullRequest
Новая
       10

Функция подтверждения Z3Py возвращает неверный контрпример

0 голосов
/ 11 октября 2018

Я пытаюсь использовать функцию подтверждения Z3Py, но кажется, что она возвращает неверный контрпример.В чем проблема??(Z3-4.7.1-x86-win, Python-2.7.15) 

>>> import z3
>>> A = z3.BitVec('A', 8)
>>> B = z3.BitVec('B', 8)
>>> C = z3.BitVec('C', 8)
>>> z3.prove((A*B)/C == A*(B/C))
counterexample
[A = 67, B = 86, C = 2]
>>> ((67*86)%256)/2
65
>>> (67*(86/2))%256
65

Ответы [ 2 ]

0 голосов
/ 11 октября 2018

Давайте посмотрим, что делает Z3: 

import z3
A = z3.BitVec('A', 8)
B = z3.BitVec('B', 8)
C = z3.BitVec('C', 8)

s = z3.Solver()
s.add((A*B)/C == A*(B/C))
print s.sexpr()

Когда вы запустите этот скрипт, вы получите: 

$ python a.py
(declare-fun C () (_ BitVec 8))
(declare-fun B () (_ BitVec 8))
(declare-fun A () (_ BitVec 8))
(assert (= (bvsdiv (bvmul A B) C) (bvmul A (bvsdiv B C))))

Ах, он использует bvmul и bvsdiv более 8-битные векторы.Оказывается, умножение не имеет значения для подписанного без знака, но деление имеет значение.Таким образом, отображение фактически выполняется для отображения результата в диапазоне от -128 до 127, а не (как я подозреваю, вы могли ожидать) в 0 до 255.

Итак,если вы выполняете математику, то левая сторона уменьшается до -63, так как умножение дает 5762, что отображается на -126 в 8-битном представлении со знаком.Правая сторона, однако, уменьшается до 65;таким образом, давая вам законный контрпример.

Чтобы избежать этого, вы можете использовать старый добрый тип Int;или попросите Python не использовать подписанное деление с помощью UDiv, см. здесь: https://z3prover.github.io/api/html/namespacez3py.html#a64c02a843a4ac8781dd666a991797906

Если вы используете UDiv, вы можете получить лучший контрпример: 

>>> import z3
>>> A = z3.BitVec('A', 8)
>>> B = z3.BitVec('B', 8)
>>> C = z3.BitVec('C', 8)
>>> z3.prove(z3.UDiv(A*B, C) == A*z3.UDiv(B, C))
counterexample
[A = 95, B = 140, C = 41]
>>> ((95*140)%256/41)%256
5
>>> (95*((140/41)%256))%256
29

что больше соответствует тому, что вы ожидали, я полагаю.

0 голосов
/ 11 октября 2018

Я думаю, что вы видите проблему с арифметикой "по модулю 8" (8-битная ширина): A * B (оба 8-битных значения) не могут быть представлены как 8-битное значение, что приводит к некоторомуобтекание / отсечение.

Эти равенства не применяются в общем случае для математики с фиксированной шириной.

...