什麼是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。