4

The C API for z3 has functions such as Z3_mk_bvadd_no_overflow, but these do not seem to be available from the Python API. Before I start hacking to solve this I'd just like to verify that this is the case and also request that these be added to the official version.

I'm trying adding things like this to z3.py, but so far haven't managed to get the details right. Suggestions about where I'm going wrong would be appreciated. I'm working on the contrib branch.

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)
4

1 回答 1

4

事实上，似乎这些功能在更高级别的 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]

（在内部，这表示为取两个位向量的 +，然后提取最高有效位。）

于 2014-03-24T11:44:45.310 回答