python 中的 z3 位向量溢出检查？

Question

z3 的 C API 具有 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) 

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]

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