Z3 INI選項的詳細文檔

Question

是否有Z3的INI選項的任何詳細文檔。我必須做一個試驗和錯誤的方法來找出QF_BV問題的最佳選擇。我仍然不確定是否有更多的選項可以讓我的z3跑得更快。如果有人能夠指出對INI選項的任何現有的詳細解釋，那將是非常好的。

謝謝。

Answer 1

我們目前正在重組Z3，並且遠離該方法：具有「千」參數的解算器。 我們正在將Z3轉變爲一種更加模塊化和靈活的方法來組合求解器和指定策略。 您可以在以下draft中找到有關此新方法的更多信息。

關於INI選項，其中有幾個已被棄用，並且只存在，因爲我們尚未完成向新方法的轉換。 這些選項中有幾個是爲特定項目添加的，現在已經過時。它們只是爲了向後兼容而存在。

關於QF_BV，Z3 3.2包含兩個QF_BV求解器：舊的（來自2.x的）和新的。新的（官方）產品僅在Z3官方輸入格式中可用：SMT 2.0。 SMT 1.0，簡化和Z3低級輸入格式已過時。 Z3 3.x的大部分性能改進僅在使用SMT 2.0輸入格式時纔可用。

在幾個月內，Z3將正式支持策略規範語言。 我們將有一個教程和文檔描述如何使用它。 與此同時，我強烈建議您對QF_BV等邏輯使用默認配置和SMT 2.0輸入格式。