为什么 Z3 online 和 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))

结果未知

处理能力不同吗？

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

约束是否相同？ 我没有看到以下的 python 变体：

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