在Z3中使用不同的後端求解器

Question

我正在使用Z3 Python接口爲我的實驗創建公式。然後我將這個公式發送給Z3解算器。如果我是正確的Z3使用它自己的求解器！

如何在Z3py中使用不同的SAT/SMT解算器？

我在CBMC（C有界模型檢查器）中使用它的方式：運行程序並吐出中間DIMAC表示（在文件中），然後將該文件用作其他SAT求解器的輸入。我可以在Z3做類似的事情嗎？謝謝。

Answer 1

所有SMT解算器都支持SMT2輸入格式，因此您可以使用Z3和其他SMT解算器進行相同的操作。 Z3py可以將求解器和目標對象轉換爲符合SMT2的字符串（一些複雜的變量聲明，例如某些數據類型可能會丟失）。

Z3py是一個特定於Z3的API（如名稱所示），它不提供使用其他SMT求解器的方法。

Answer 2

聽起來像你應該真的使用解算器不可知的SMT接口，而不是Z3py。已經有一些嘗試創建這樣的接口，有不同程度的支持多種解算器：

• https://github.com/pysmt/pysmt是求解不可知的Python API來SMT求解。我自己並沒有使用它，但它確實聽起來很有希望，特別是如果你想Python作爲你的頂級API。

• https://github.com/sosy-lab/java-smt是一個類似的項目，它使用Java作爲主機語言。

• http://leventerkok.github.io/sbv/是我自己嘗試爲使用SMT解算器提供解算器不可知的API，這是用Haskell編寫的。

絕不意味着這是一份詳盡的清單。我敢肯定，還有其他的語言，不同程度的成熟度。您應該選擇哪一個取決於您的主機語言偏好以及每個系統提供的功能;這可能差別很大。