Z3术语中下溢的定义是什么

Question

玩 Z3_mk_bvadd_no_underflow() 和 Z3_mk_bvadd_no_overflow() 我觉得 underflow 的定义与我在其他文献中找到的不匹配（维基百科， INTEL 编程手册,Whosebug,...):

我理解溢出是指加法的结果大于在给定操作数编码位数的情况下可以表示的最大数。这很正常。
对于下溢，我的理解是（在 Z3 术语中）当结果小于给定操作数编码的位数时可以表示的最小整数。这没关系，但根据我所见（例如 wikipedia）在文献中不常见，因为此概念仅适用于浮点数。

在intel编程手册中，overflow/underflow处理进位和溢出标志：

Carry flag — Set if an arithmetic operation generates a carry or a borrow out of the most significant bit of the result; cleared otherwise. This flag indicates an overflow condition for unsigned-integer arithmetic. It is also used in multiple-precision arithmetic.

Overflow flag — Set if the integer result is too large a positive number or too small a negative number (excluding the sign-bit) to fit in the destination operand; cleared otherwise. This flag indicates an overflow condition for signed-integer (two’s complement) arithmetic.

能否确认下溢在 Z3 术语中的确切定义？

我建议将其添加到文档中，以及假设的减法方式（从第二个操作数中减去第一个操作数与从第一个操作数中减去第二个操作数），它适用于许多其他 API Z3.

Answer 1

下溢谓词的最佳定义是代码本身，参见 Z3_mk_bvadd_no_underflow；它执行以下操作（减去引用计数）：

Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2) {
    Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1));
    Z3_ast r = Z3_mk_bvadd(c, t1, t2);
    Z3_ast l1 = Z3_mk_bvslt(c, t1, zero);
    Z3_ast l2 = Z3_mk_bvslt(c, t2, zero);
    Z3_ast args[2] = { l1, l2 };
    Z3_ast args_neg = Z3_mk_and(c, 2, args);
    Z3_ast lt = Z3_mk_bvslt(c, r, zero);
    Z3_ast result = Z3_mk_implies(c, args_neg, lt);
    return result;
}

请注意，下溢谓词假定参数是带符号的位向量，但 Z3_mk_bvsub_no_underflow 除外，它具有启用无符号语义的标志。

最后的评论：Z3_mk_bvsub(c, t1, t2) 总是计算 t1-t2。

Z3术语中下溢的定义是什么

What is the definition of underflow in Z3 terminology

z3