Z3：Z3py表情從求解對象

Question

這個問題轉換爲SMT-LIB2非常相似：Z3: convert Z3py expression to SMT-LIB2?

是否有可能生成求解對象SMT-LIB2輸出？

Answer 1

Solver類有方法稱爲assertions()。它返回所有的公式被斷言到給定的求解器中。在我們提取斷言之後，我們可以使用上一個問題中使用的相同方法。這裏是一個快速和骯髒的修改

def toSMT2Benchmark(f, status="unknown", name="benchmark", logic=""): 
    v = (Ast * 0)() 
    if isinstance(f, Solver): 
    a = f.assertions() 
    if len(a) == 0: 
     f = BoolVal(True) 
    else: 
     f = And(*a) 
    return Z3_benchmark_to_smtlib_string(f.ctx_ref(), name, logic, status, "", 0, v, f.as_ast()) 

下面是一個例子（also available online at here）

s = Solver() 
print toSMT2Benchmark(s, logic="QF_LIA") 
a, b = Ints('a b') 
s.add(a > 1) 
s.add(Or(a < 1, b < 2)) 
print toSMT2Benchmark(s, logic="QF_LIA") 

EDIT我們可以使用下面的腳本來顯示SMTLIB 1.x的格式的輸出（也可在線獲得here）。請注意，SMTLIB 1.x非常有限，並且不支持多種功能。 我們也強烈鼓勵所有用戶遷移到SMTLIB 2.x.

def toSMTBenchmark(f, status="unknown", name="benchmark", logic=""): 
    v = (Ast * 0)() 
    if isinstance(f, Solver): 
    a = f.assertions() 
    if len(a) == 0: 
     f = BoolVal(True) 
    else: 
     f = And(*a) 
    Z3_set_ast_print_mode(f.ctx_ref(), Z3_PRINT_SMTLIB_COMPLIANT) # Set SMTLIB 1.x pretty print mode 
    r = Z3_benchmark_to_smtlib_string(f.ctx_ref(), name, logic, status, "", 0, v, f.as_ast()) 
    Z3_set_ast_print_mode(f.ctx_ref(), Z3_PRINT_SMTLIB2_COMPLIANT) # Restore SMTLIB 2.x pretty print mode 
    return r 

s = Solver() 
print toSMTBenchmark(s, logic="QF_LIA") 
a, b = Ints('a b') 
s.add(a > 1) 
s.add(Or(a < 1, b < 2)) 
print toSMTBenchmark(s, logic="QF_LIA") 

編輯完