Некорректного результат суммы ИНТ-литого BitVec с помощью Z3, Z3py

Question

Я использую следующий код питона, чтобы найти два двоичных чисел, что:

• суммы определенного число
• своих высокие биты отлитых в целые числа должны сумма до 2

Второе ограничение более важно для меня; и в моем случае он будет масштабироваться: допустим, это может означать, что наивысшие биты номера [N] должны суммироваться с [M].

Я не уверен, почему z3 не дает правильного результата. Любые намеки? Большое спасибо.

def BV2Int(var): 
    return ArithRef(Z3_mk_bv2int(ctx.ref(), var.as_ast(), 0), var.ctx) 

def main(): 
    s = Solver() 
    s.set(':models', True) 
    s.set(':auto-cfgig', False) 
    s.set(':smt.bv.enable_int2bv',True) 

    x = BitVec('x',4) 
    y = BitVec('y',4) 
    s = Solver() 
    s.add(x+y == 16, Extract(3,3,x) + Extract(3,3,y) == 2) 
    s.check() 
    print s.model() 
    # result: [y = 0, x = 0], fail both constraint 

    s = Solver() 
    s.add(x+y == 16, BV2Int(Extract(3,3,x)) + BV2Int(Extract(3,3,y)) == 2) 
    s.check() 
    print s.model() 
    # result: [y = 15, x = 1], fail the second constraint 

Update: Спасибо ответ от Кристофа. Вот быстро исправить:

• экстракт (3,3, х) -> ZeroExt (С.З., экстракт (3,3, х)), где СЗ ширина немного RHS минус 1.

Answer 1

(в стороне:. авто-cfgig должен быть автоматически конфигурация)

Обратите внимание, что bv2int и int2bv по существу рассматривается как необработанном, так что, если эта часть имеет решающее значение для вашей проблемы, то не используйте их (см documentation и previous questions).

Проблема с этим примером - это ширина бит-векторов. Оба x и y являются 4-битные переменные и цифра 16 как 4-битового вектора а является 0 (по модулю 2^4), таким образом, действительно x + y равно 16 когда это x=0 и y=0.

Далее, Extract(...) термины извлечения 1-битных векторов, что означает, что сумма Ex.. + Ex.. снова является 1-битное значение, и числом 2 как 1-битового вектора а является 0 (по модулю 2^1), то есть, его это действительно так, что Ex... + Ex... = 2.