什么是Z3术语

Question

下溢的定义与Z3_mk_bvadd_no_underflow()和Z3_mk_bvadd_no_overflow()打我有感觉的下溢的定义不匹配什么我在文献中找到其他地方（维基百科，INTEL编程手册，计算器，... ）：

• 据我所知，溢流是当相加的结果比可以表示给定的在其上的操作数被编码的比特的数量的最大数量。这是平常的。

• 对于下溢，我知道（在Z3术语中），当结果小于可以表示的最小整数时，给定操作数编码的位数。这是可以的，但是在我看到的文献中不常见（例如wikipedia），因为这个概念只适用于浮点数。

在Intel编程手册，上溢/下溢的处理携带和溢出国旗：

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

溢出标志 - 设置如果整数结果太大正 数或过小的负数（排除符号位），以适应目标操作数 ;否则清除。该标志指示有符号整数（二进制补码）算术的一个 溢出条件。

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

我建议将其添加到文档中，以及减法的假定方式（从第二个操作数中减去第一个操作数，再从第一个操作数中减去第二个操作数），这可以从Z3的其他API中获得。

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。