ошибка z3py при преобразовании int в bitvec

From (Z3: возможно ли суммировать BitVec и Real?), я попытался преобразовать int в bitvec, используя

x = Int('x')
reg = BitVecRef(Z3_mk_int2bv(BitVecVal(x.ctx_ref(), 16, x)), x.ctx)

но я всегда получаю сообщение об ошибке: «Объект 'Ast' не имеет атрибута 'ref'», кажется, эта функция может преобразовывать только целое число в битвек, есть ли другой способ преобразовать Int в битвек?

Также я знаю, что эта функция на данный момент рассматривается как не интерпретируемая, нужно ли мне перекомпилировать мою локальную версию из (bv-enable-int2bv-propagation option) ?

Заранее спасибо!


z3 z3py
person Pounce    schedule 20.04.2015    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Код, который вы предлагаете, сначала пытается преобразовать x в значение битового вектора (BitVecVal), т. е. фактическое число, но x не является значением (числом). Правильное выражение можно построить следующим образом:

x = Int('x')
raw = Z3_mk_int2bv(x.ctx_ref(), 16, x.as_ast())
reg = BitVecRef(raw, x.ctx)
print reg

Исправление int2bv-propagation было добавлено задолго до последнего выпуска Z3, поэтому, если вы используете версию менее года назад, вам не нужно ничего перекомпилировать.

person Christoph Wintersteiger    schedule 21.04.2015