为什么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

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

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

Answer 2

造成结果不同的原因是因为输入的不一样。例如，表达式

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

这会产生所需的结果。

为什么Z3 online和Z3PY的结果不一样？

Why result of Z3 online and Z3PY are different?

z3

z3py