從z3模型聲明定義不產生

Question

我有一些斷言，我給z3可以滿足。當我致電(check-sat)時，z3會返回sat。然後我打電話(get-model)，並查看特定變量的定義，%%P2_*_143。它看起來像這樣：

(define-fun %%P2_*_143() JS (NUM 2.0)) 

如果我拿這個定義，再次把它變成斷言

(assert (= %%P2_*_143 (NUM 2.0))) 

，並呼籲(check-sat)，Z3返回unsat。此外，如果我再撥打(get-unsat-core)，z3會返回()。

我的理解是，由z3產生的模型給所有變量提供了令人滿意的分配，所以斷言分配也應該是可滿足的。這是不正確的，還是我在其他地方有一個錯誤？

整套斷言是在這個要點：https://gist.github.com/2966738。增加的主張是在最底層。

我在Mac OS X 10.7.4上使用Z3版本3.2。我還能夠使用在線界面http://rise4fun.com/z3重現此行爲。

Answer 1

幾天前曾有類似的錯誤報告過。線性實數算術包中模型構造中存在一個缺陷。該錯誤已得到修復。 Z3使用無窮小來處理嚴格的不等式，細節描述在以下文章中：http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf

請注意，該錯誤不會影響解算器的健全性。也就是說，sat/unsat的答案是正確的。但是，該模型不是。您的示例中的第二個查詢不可用，因爲該模型不正確。如果你需要，我可以製作一個新的二進制文件來解決這個問題。同時，您可以通過在腳本中添加以下命令來解決該錯誤：

(declare-fun delta() Real) 
(assert (< 0.0000001 delta)) 
(assert (< delta 0.0000002))