Я использую Z3py, чтобы попытаться провести некоторые эксперименты по проблеме ошибки округления, выясняется, что я должен подвести итог битвеку и реалу. Однако, когда я пытаюсь сделать это, я получаю ошибку «несоответствие сортировки». Это мой код:Z3: Можно ли суммировать битвек и реальный?
x = BitVecVal(8, 6)
y = Real('y')
solve(y + x == 5)
Есть ли способ суммировать BitVec и Real? или просто получить значение Int BitVec?
API на основе Z3 C содержит функции преобразования от бит-векторов к цифрам (целые числа), а целые числа могут быть принудительно применены к действиям. Однако питон API не предоставляет соответствующую функцию непосредственно, но вы можете обернуть его:
x = BitVecVal(2,8)
y = Real('y')
def to_int(x):
return ArithRef(Z3_mk_bv2int(x.ctx_ref(), x.as_ast(), 0), x.ctx)
print solve(to_int(x) + y == 5)
Вы можете преобразовать значение вектора битного в подписанном давно:
x = BitVecVal(8, 6)
y = Real('y')
solve(y + x.as_signed_long() == 5)
# [y = -3]
Кстати, я нашел as_signed_long осматривая y, как один обычно делает в Python, а именно, print dir(y).
Спасибо за ваш ответ, я действительно ценю это. Кстати, метод as_signed_long доступен только для BitVecVal, а не для BitVec. Что, если я хочу, чтобы x был BitVec вместо константы? Там в любом случае? – vutran
Извините, я не знаю, что делать с «BitVec». –
Отличный ответ, спасибо, человек. Я не видел этого в документации. Однако влияет ли эта функция переноса на производительность Solver? – vutran
В вашем примере значение 'x' является значением. Таким образом, эффективность не влияет. Препроцессор Z3 преобразует 'to_int (x)' в действительное число '2'. Однако, если 'x' не является значением, то есть серьезное влияние на производительность. 'To_int' будет« взорван »в большой термин' if-then-else', который «строит» целое число, основанное на битах 'x'. Мы получаем термин 'if-then-else' для каждого бита. Есть «умные» способы обработки 'to_int', но Z3 в настоящее время использует этот простой/наивный подход. –