爲什麼Z3在網頁和本地報告不同的查詢狀態（分別爲不分/不分）？

http://rise4fun.com/Z3/MlnZ 爲什麼Z3在網頁和本地報告不同的查詢狀態（分別爲不分/不分）？

正確的結果應該是UNSAT（在線版），但是本地Z3 3.2報告SAT。它還生成一個有趣的model，其中包含枚舉類型（數據類型）的Universe和基數約束。想法？謝謝！

2012-05-08 Ayrat

這是一個錯誤。 Z3 3.2不會爲您的腳本安裝遞歸數據類型引擎。因此，Q和T類別被視爲未解釋的類別。 Z3 4.0修復了這個錯誤。在線版本已經運行Z3 4.0。這就是爲什麼你使用在線版本獲得正確結果的原因。您可以在Z3 3.2中使用以下解決方法。

（設置選項：自動配置錯誤）

來源

2012-05-08 18:32:58

謝謝！這樣可行！第二個問題 - Z3仍然沒有簡化並返回'（get-value（（tau t_0 i_stop））））'（例如）的具體值。它產生：'（ite（= t_0 t_3）t_3（ite（= t_0 t_2）t_0（ite（= t_0 t_1）t_3 t_0）））））'這正是't_0'。想法如何克服？ – Ayrat

這已在Z3 4.0中修復。在線版本中你仍然得到這種輸出嗎？我們應該在本週發佈Z3 4.0。 –

不適用，僅限本地版本。好，期待！ – Ayrat

等待已經結束。 4.0已經發布。

來源

2012-05-09 02:28:25

爲什麼Z3在網頁和本地報告不同的查詢狀態（分別爲不分/不分）？

回答

相關問題