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

【问题标题】：What is the definition of underflow in Z3 terminologyZ3术语中下溢的定义是什么
【发布时间】：2015-09-13 20:19:21
【问题描述】：

玩Z3_mk_bvadd_no_underflow() 和Z3_mk_bvadd_no_overflow() 我感觉underflow 的定义与我在文献（维基百科、INTEL 编程手册、stackoverflow、... ):

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

在intel编程手册中，上溢/下溢都是用carry和overflow标志处理的：

进位标志 — 如果算术运算产生进位或进位，则设置借用结果的最高位；清除否则。该标志表示溢出条件无符号整数算术。它也用于多精度算术。

溢出标志 — 如果整数结果太大，则设置为正数数字或太小的负数（不包括符号位）以适应在目标操作数中；否则清除。该标志表示有符号整数（二进制补码）算术的溢出条件。

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

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

【问题讨论】：

标签： z3

【解决方案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。

【讨论】：