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

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

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

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)

z3 z3py
person John Regehr    schedule 21.03.2014    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Действительно, кажется, что эти функции пока недоступны в 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]

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

person Christoph Wintersteiger    schedule 24.03.2014
comment
Кристоф, спасибо! При вызове этот код умирает с несоответствием сортировки аргумента в позиции 2, но я уверен, что это близко, я продолжу попытки. - person John Regehr; 24.03.2014
comment
Что ж, я пробовал много небольших вариаций на эту тему и все время получаю одно и то же сообщение об ошибке, аргх. - person John Regehr; 24.03.2014
comment
Я обновил это вызовом z3._coerce_exprs (что делает API). У меня работает и эта, и предыдущая версия. Я добавил пример его использования на всякий случай, если проблема заключается в нем. - person Christoph Wintersteiger; 25.03.2014
comment
Спасибо Кристоф! Я отправлю запрос на вытягивание, как только я это интегрирую. - person John Regehr; 26.03.2014