爲什麼Z3在線和Z3PY的結果不一樣？

Question

下面的代碼我在在線和離線Z3試圖

(set-option :smt.mbqi true) 
(declare-var X Int) 
(declare-var X_ Int) 
(declare-var a_ Int) 
(declare-var su_ Int) 
(declare-var t_ Int) 
(declare-var N1 Int) 
(assert (>= X 0)) 
(assert (forall ((n1 Int)) (=> (< n1 N1) (>= X (* (+ n1 1) (+ n1 1)))))) 
(assert (= X_ X)) 
(assert (= a_ N1)) 
(assert (= su_ (* (+ N1 1) (+ N1 1)))) 
(assert (= t_ (* (+ N1 1) 2))) 
(assert (< X (* (+ N1 1) (+ N1 1)))) 
(assert (not (< X (* (+ a_ 1) (+ a_ 1))))) 
(check-sat) 

結果造成不滿意

下面的代碼我已經在Z3PY

set_option('smt.mbqi', True) 
s=Solver() 
s.add(X>=0) 
s.add(ForAll(n1,Implies(n1 < N1,((n1+1)**2)<=X))) 
s.add(((N1+1)**2)>X) 
s.add(X_==X) 
s.add(a_==N1) 
s.add(su_==((N1+1)**2)) 
s.add(t_==(2*(N1+1))) 
s.add(Not(((a_+1)**2)>X)) 

result-未知

是處理能力不同的嘗試？

Answer 1

原因在結果之間的差異是因爲輸入的是不一樣的。例如，所述表達

(N1+1)**2 

在語義上是相同

(* (+ N1 1) (+ N1 1)) 

但由於句法差異，Z3不會簡化式的東西，它可以很容易地解決。 Python中的語法等價問題是：

s.add(X>=0) 
s.add(ForAll(n1,Implies(n1 < N1,((n1+1)**2)<=X))) 
s.add(((N1+1)*(N1+1)) > X) 
s.add(X_==X) 
s.add(a_==N1) 
s.add(su_==((N1+1)*(N1+1))) 
s.add(t_==(2*(N1+1))) 
s.add(Not(((a_+1)*(a_+1))>X)) 

它會產生所需的結果。

Answer 2

約束是否相同？ 我沒有看到蟒蛇的變體：

(assert (< X (* (+ N1 1) (+ N1 1))))