来自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]

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