如何z3py表達式轉換爲smtlib 2格式

Question

我的問題是關於：Z3: convert Z3py expression to SMT-LIB2?

我想z3py從表達到smtlib2格式轉換。使用下面的腳本，但是轉換後，當我喂結果Z3或任何其他SMT，我得到：

「語法錯誤，意外讓」

有什麼辦法，我可以帶它使用z3py在smtlib2格式，以便我不必再次寫長表達式。

下面是我使用的轉換代碼：

def convertor(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()) 

x = Int('x') 
y = Int('y') 
s = Solver() 
s.add(x > 0) 
s.add(x < 100000) 
s.add(x==2*y) 
print convertor(s, logic="QF_LIA") 

，這是輸出：

(set-info :status unknown) 
(set-logic QF_LIA) 
(declare-fun y() Int) 
(declare-fun x() Int) 
(let (($x34 (= x (* 2 y)))) 
(let (($x31 (< x 100000))) 
(let (($x10 (> x 0))) 
(let (($x35 (and $x10 $x31 $x34))) 
(assert $x35))))) 
(check-sat) 

Answer 1

這也涉及到另外一個問題here。

很可能，這個問題是因爲Z3的過時版本。曾有還沒有使它成爲主分支尚未使用的不穩定分支（或預編譯的二進制夜間here）我得到不同的結果，這是由Z3接受沒有錯誤的大量bug修正：

(set-info :status unknown) 
(set-logic QF_LIA) 
(declare-fun y() Int) 
(declare-fun x() Int) 
(assert 
(let (($x34 (= x (* 2 y)))) 
(let (($x31 (< x 100000))) 
(let (($x10 (> x 0))) 
(and $x10 $x31 $x34))))) 
(check-sat)