爲什麼0 = 0.5？

Question

當使用.smt2文件時，我注意到了Z3 4.3.1的一些奇怪行爲。

如果我這樣做(assert (= 0 0.5))這將是滿足的。但是，如果我切換訂單並執行(assert (= 0.5 0))，則不能滿足要求。

我爲所發生的事情的猜測是，如果第一個參數是一個整數，它施放他們都爲整數（四捨五入0.5下降到0），然後做比較。如果我將「0」更改爲「0.0」，則按預期工作。這與我所使用的大多數編程語言形成了鮮明對比，如果其中任何一個參數都是浮點數，它們都會被轉換爲浮點數並進行比較。這真的是Z3的預期行爲嗎？

Answer 1

嚴格來說，Z3默認情況下不符合SMT 2.0標準，這就是其中一種情況。我們可以添加

(set-option :smtlib2-compliant true) 

然後這個查詢確實被拒絕了。

Answer 2

我們的一個實習生，誰SMT2保守延伸與多態性的工作已經注意到了同樣的奇怪的行爲，當他試圖在理解公式混合整數和實數是如何類型檢查：

Z3（http://rise4fun.com/z3）說，下面的例子是SAT，並且發現模型X = 1

(set-logic AUFLIRA) 
(declare-fun x() Int) 
(assert (= x 1.5)) 
(check-sat) 
(get-model) 
(exit) 

但是，它說，下面的 「等效」 的例子在UNSAT

(set-logic AUFLIRA) 
(declare-fun x() Int) 
(assert (= 1.5 x)) 
(check-sat) 
(exit) 

所以，這不符合對稱性謂詞的對稱性。所以，我認爲這是一個錯誤。

Answer 3

我認爲這是缺少類型檢查的結果; z3太寬鬆了。它應該簡單地拒絕這樣的查詢，因爲它們根本沒有形成。

根據該SMT-Lib的標準，V2（http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r10.12.21.pdf）;第30頁;核心理論正是如此定義：

(theory Core 
:sorts ((Bool 0)) 
:funs ((true Bool) (false Bool) (not Bool Bool) 
     (=> Bool Bool Bool :right-assoc) (and Bool Bool Bool :left-assoc) 
     (or Bool Bool Bool :left-assoc) (xor Bool Bool Bool :left-assoc) 
     (par (A) (= A A Bool :chainable)) 
     (par (A) (distinct A A Bool :pairwise)) 
     (par (A) (ite Bool A A A)) 
    ) 
:definition 
"For every expanded signature Sigma, the instance of Core with that signature 
is the theory consisting of all Sigma-models in which: 
    - the sort Bool denotes the set {true, false} of Boolean values; 
    - for all sorts s in Sigma, 
     - (= s s Bool) denotes the function that 
     returns true iff its two arguments are identical; 
     - (distinct s s Bool) denotes the function that 
     returns true iff its two arguments are not identical; 
     - (ite Bool s s) denotes the function that 
     returns its second argument or its third depending on whether 
     its first argument is true or not; 
     - the other function symbols of Core denote the standard Boolean operators 
     as expected. 
     " 
    :values "The set of values for the sort Bool is {true, false}." 
) 

因此，通過定義平等，需要輸入各種各樣是相同的;因此上述查詢應被拒絕爲無效。

有可能是Z3的交換機或迫使越來越嚴格的類型檢查比它在默認情況下其他一些設置;但是我希望這個案例能夠被最輕鬆的實現所捕獲。

Answer 4

一種可能的解決方案是

(declare-fun x() Real) 
(declare-fun y() Real) 
(assert (= x 0)) 
(assert (= y 0.5)) 
(check-sat) 
(push) 
(assert (= x y)) 
(check-sat) 
(pop) 

並且輸出是

sat 
unsat 

Answer 5

Z3不是唯一SMT求解器，類型檢查這些例子：

• CVC4接受他們（即使帶有選項--smtlib-strict），並在上述兩個公式的情況下都回答UNSAT。

• Yices接受他們和答案UNSAT（改變邏輯QF_LIA後，因爲它不支持AUFLIRA）。

• 有（組邏輯QF_LIA），Z3發出一個錯誤：（錯誤 「行3列17：邏輯不支持實數」）。

• Alt-Ergo在這兩種情況下都會提示「輸入錯誤：Int和Real無法統一」。但是，Alt-Ergo的SMT2解析器非常有限，並沒有經過嚴格測試，因爲我們專注於它的本地多態語言。所以，不應該把它作爲參考。

我認爲開發人員通常假設Int和Real之間存在「隱式」的子類型關係。這就是爲什麼這些例子通過Z3，CVC4和Yices（也可能是其他類型）成功進行類型檢查的原因。

Answer 6

不要依賴任何求解器的隱式類型轉換。相反， 使用to_real和to_int進行顯式類型轉換。只發送 井型公式給求解器。然後Mohamed Iguernelala的例子成爲以下內容。

(set-logic AUFLIRA) 
(declare-fun x() Int) 
(assert (= (to_real x) 1.5)) 
(check-sat) 
(exit) 

(set-logic AUFLIRA) 
(declare-fun x() Int) 
(assert (= 1.5 (to_real x))) 
(check-sat) 
(exit) 

這兩個都返回UNSAT在Z3和CVC4。相反，如果您真的想要找到 的模型，那麼x = 1您應該使用以下的一個 。

(set-option :produce-models true) 
(set-logic AUFLIRA) 
(declare-fun x() Int) 
(assert (= (to_int 1.5) x)) 
(check-sat) 
(get-model) 
(exit) 

(set-option :produce-models true) 
(set-logic AUFLIRA) 
(declare-fun x() Int) 
(assert (= x (to_int 1.5))) 
(check-sat) 
(get-model) 
(exit) 

這兩個與x = 1在Z3和CVC4返回飽和

一旦你使所有的類型轉換都是顯式的，並且只處理良好類型的公式，那麼等於的參數順序就不再重要了（爲了正確性）。

Answer 7

Jochen Hoenicke給出了關於「混合實數和整數」的答案（在SMT-LIB郵件列表中）。它是：

I just wanted to point out, that the syntax may be officially correct. There is an extension in AUFLIRA and AUFNIRA.

From http://smtlib.cs.uiowa.edu/logics/AUFLIRA.smt2

"For every operator op with declaration (op Real Real s) for some sort s, and every term t1, t2 of sort Int and t of sort Real, the expression - (op t1 t) is syntactic sugar for (op (to_real t1) t) - (op t t1) is syntactic sugar for (op t (to_real t1)) - (/ t1 t2) is syntactic sugar for (/ (to_real t1) (to_real t2)) "