Как представить отрицательное число в битвекторе?
Название говорит само за себя. Я пытаюсь представить -1 как следующее: (_ bv-1 32)и z3 жалуется.
Как мне представить такое ограничение, как 3x - 5y <= 10 в битовом векторе? По какой-то причине я не хочу использовать линейное целое число.
1 ответ
Решение
Обычно это делается с помощью кодирования двух дополнений. Короткая версия
-x = flip(x) + 1
где flip(x) просто переворачивает все биты в x,