爲什麼Z3中的運算符'/'和'div'會給出不同的結果？

Question

我試圖用兩個整數表示一個實數，用它們作爲實數的分子和分母。我寫了下面的程序：

(declare-const a Int) 
(declare-const b Int) 
(declare-const f Real) 

(assert (= f (/ a b))) 
(assert (= f 0.5)) 
(assert (> b 2)) 
(assert (> b a)) 

(check-sat) 
(get-model) 

程序返回SAT結果如下：

sat 
(model 
    (define-fun f() Real 
    (/ 1.0 2.0)) 
    (define-fun b() Int 
    4) 
    (define-fun a() Int 
    2) 
) 

不過，如果我寫 '（斷言（= F（DIV AB）））' 而不是「（ assert（= f（/ ab）））'，那麼結果是UNSAT。爲什麼div不會返回相同的結果？另外，對於我來說主要關心的是，我沒有找到在z3 .Net API中使用運算符'/'的方法。我只能看到函數MkDiv，它實際上是運算符'div'。有沒有辦法讓我可以在z3 .Net API的情況下應用運算符'/'？先謝謝你。

Answer 1

嚴格地說既不這些公式是SMT-LIB2柔順的，因爲/是一個函數，它有兩個實輸入，併產生一個真正的輸出，而div是一個函數，它兩個int輸入，併產生一個Int（見SMT-LIB Theories） 。 Z3更放鬆並自動轉換這些對象。如果我們啓用選項smtlib2_compliant=true那麼它確實會在兩種情況下報告錯誤。

的原因div版本爲不可滿足的是，有確實沒有解決方案，其中f是根據(= f (/ a b))的整數，但確實沒有整數，其滿足(= f 0.5)