Z3/SMT：我應該什麼時候推/推重置？

我正在使用Z3來解決由符號執行程序產生的路徑條件，它以深度優先順序探索狀態空間，與CUTE，DART或（可能）SAGE十分相似。我們正在嘗試使用Z3的不同方式。在某種極端情況下，我們會將每個查詢發送給Z3並立即（重置）。另一方面，我們（推）每個額外的分支約束，並（回彈）（彈出）回溯到正確削弱路徑條件所需的最小值。問題是，在所有情況下，沒有任何戰略似乎比其他戰略更好。推送似乎提供了最好的優勢，但是我們遇到了幾個例子，在每次查詢之後重置Z3的速度比推/拉快一個數量級。請注意，通信開銷可以忽略不計：幾乎所有的時間都花在check-sat內部。Z3/SMT：我應該什麼時候推/推重置？

有沒有人有任何經驗可以分享，或有關Z3內部保存的狀態（引理等）的一些跡象，這有助於闡明其行爲？那麼其他SMT解算器的行爲呢？

來源

2013-01-11 Pietro Braione

下一版本（v4.3.2）將公開可能對您有用的功能。在Z3中，默認求解器組合了一個非增量求解器和一個增量求解器。當使用push/pop（或使用多個check而不調用reset時），Z3將使用增量求解器。在下一個版本中，我們可以爲增量求解器提供超時。如果增量求解器在給定的超時時間內無法解決問題，Z3將自動切換到非增量求解器。也許，如果你使用這個功能，你將能夠獲得最好的「兩個世界」。爲了得到下一個候選版本的源代碼，您應該使用

git clone https://git01.codeplex.com/z3 -b rc

要編譯它，我們需要使用

cd z3 
python scripts/mk_make.py 
cd build 
make

要設置超時的增量求解，我們提供以下命令行選項：

combined_solver.solver2_timeout=<time in milliseconds>

如果您正在使用的編程API，你可以在新的API：

Z3_global_param_set(Z3_string param_id, Z3_string param_value)

請注意，下一個版本將有一個用於設置參數的新框架。它允許用戶爲內部Z3模塊設置參數。

來源

2013-01-13 18:24:59

謝謝你的回答，並對遲到的反饋抱歉。這隻能部分回答我的問題，因爲它沒有提供給出一系列查詢來確定使用求解器的最佳方式的基本原理，這個問題在我們的案例中可能至關重要。順便說一句，push + reset（沒有彈出）觸發增量求解器嗎？ –

Z3/SMT：我應該什麼時候推/推重置？

回答

相關問題