z3 проверка переполнения битвектора из python?

Question

C API для z3 имеет такие функции, как Z3_mk_bvadd_no_overflow, но они, похоже, недоступны из Python API. Прежде чем приступить к взлому, чтобы решить эту проблему, я просто хочу убедиться, что это так, а также попросить, чтобы они были добавлены в официальную версию.

Я пытаюсь добавить такие вещи в z3.py, но до сих пор не удалось получить правильные детали. Предложения о том, где я иду не так, будут оценены. Я работаю над веткой Contribu.

def Bvadd_no_overflow(a, b, si, ctx=None):
    """Create a Z3 bvadd_no_overflow expression.

    """
    ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
    # argh can't hard-code the 32
    s = BitVecSort(32,ctx)
    a = s.cast(a)
    b = s.cast(b)
    # this function requires a bool as the last argument but is it a python bool, a
    # z3 bool, or what?
    return BitVecRef(Z3_mk_bvadd_no_overflow(ctx.ref(), a.as_ast(), b.as_ast(), 1), ctx) 

Answer 1

Действительно, кажется, что эти функции еще не доступны в API более высокого уровня. Что-то в этом роде может помочь вам:

def bvadd_no_overflow(x, y, signed=False):
    assert x.ctx_ref()==y.ctx_ref()
    a, b = z3._coerce_exprs(x, y)
    return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed))

Вот пример использования этой функции, которая работает для меня:

q = BitVec('q', 32)
r = BitVec('r', 32)
s.add(bvadd_no_overflow(q, r))
print(s)

который печатает

[Extract(32, 32, ZeroExt(1, q) + ZeroExt(1, r)) == 0]

(Внутренне это представляется как взятие + двух битовых векторов и затем извлечение наиболее значимого бита.)

Answer 2

Я столкнулся с той же проблемой через 8 лет после публикации последнего ответа. Итак, вот обновление:

Z3 Python API теперь имеет функциюBVAddNoOverflowкоторый определяется как таковой:

      def BVAddNoOverflow(a, b, signed):
    """A predicate the determines that bit-vector addition does not overflow"""
    _check_bv_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(),
                   b.as_ast(), signed), a.ctx)

Эквивалентные функции также существуют для переполнения и потери значимости для других арифметических операций: BVSubNoOverflow, BVMulNoUnderflow, так далее.

Я публикую это здесь для потомков, так как именно здесь я приземлился, пытаясь ответить на аналогичный вопрос.