Z3：將Z3py表達式轉換爲SMT-LIB2？

Question

給定Z3py中的表達式，我可以將它轉換爲SMT-LIB2語言嗎？ （因此，我可以將此SMT-LIB2表達式提供給支持SMT-LIB2的其他SMT解算器）

如果可以，請舉一個例子。

非常感謝。

Answer 1

我們可以使用C API Z3_benchmark_to_smtlib_string。 C API中的每個函數都可以在Z3Py中使用。此功能最初用於轉儲SMT 1.0格式的基準，並且早於SMT 2.0。這就是爲什麼它有一些看起來沒有必要的參數。現在，默認情況下，它將顯示SMT 2.0格式的基準。輸出是而不是意味着人類可讀。 我們可以寫出下面的Python功能，使其更加方便使用：

def toSMT2Benchmark(f, status="unknown", name="benchmark", logic=""): 
    v = (Ast * 0)() 
    return Z3_benchmark_to_smtlib_string(f.ctx_ref(), name, logic, status, "", 0, v, f.as_ast()) 

下面是使用它的一個小例子（也可在網上here）

a = Int('a') 
b = Int('b') 
f = And(Or(a > If(b > 0, -b, b) + 1, a <= 0), b > 0) 
print toSMT2Benchmark(f, logic="QF_LIA")