Я использую интерфейс z3 python и пытаюсь упростить некоторые выражения битовых векторов.
Моя цель - получать выражения только с константой справа.
Для арифметических выражений использование функции упрощения с опцией arith-lhs = true работает нормально, но для битовых векторов это не работает (я полагаю, это не было предназначено для этого).
Например, распечатывается следующий код
4294967295 <= x
дважды,
и я хочу напечатать
x >= 4294967295.
x = BitVec('x',32)
a = BitVecVal(-1, 32)
print(simplify(a<=x))
print(simplify(a<=x,arith_lhs=True))
Есть ли способ заставить z3 сделать это?