位操作難題

Question

此C表達式總是評估爲真？

((x+y)<<4) + y - x == 17*y +15*x 

從我可以告訴算法是正確的，但我對是什麼將溢出的情況下發生的不確定 的唯一的事情。

我的理解是，C乘法表達式處理溢出 相同的方式作爲位移，但我不確定。

有沒有人知道這個答案？

Answer 1

答案是「否」，特別是在溢出的情況下。

正如你可以從答案here看到的，大多數計算機是二進制補碼，但它們不一定是（並且歷史上已經有一些補充計算機），並且溢出錯誤因此是未定義的行爲。

它可能在您的計算機上工作，但不能保證可以工作。

Answer 2

您可以通過SAT solver運行此類示例來檢查您剛纔指定的方程或公式的可滿足性。

我沒有找到它滿足您的任何約束X或Y（即：不存在在這個等式產生收入差距的任何X或Y）

(declare-const x (_ BitVec 32)) 
(declare-const y (_ BitVec 32)) 

(assert (not (= (bvsub (bvadd (bvshl (bvadd x y) #x00000004) y) x) 
       (bvadd (bvmul #x00000011 y) (bvmul #x0000000f x))))) 

(check-sat) 
(get-model) 

在問候溢出，邏輯上bitvectors一般不提供有符號位數和無符號位數作爲數字。相反，比特向量理論提供了算術運算的特殊簽名版本，不管該比特向量是作爲有符號還是無符號處理，它都有所不同。我已經使用適當的操作符到您指定的公式。當然，您可以將結果代數化爲(x+y)<<4 == 16y + 16x，但SMT解算器處理像溢出這樣的情況很難正式確定）。

無論你的指令字大小，沒有X或Y可以產生不平等。