z3 和 z3PY 给出不同的结果

Question

当我在 z3 中尝试跟随时，结果超时

(set-option :smt.mbqi true)
(declare-fun R(Int) Int)
(declare-fun Q(Int) Int)
(declare-var X Int)
(declare-var Y Int)
(declare-const k Int)
(assert (>= X 0))
(assert (> Y 0))
(assert (forall ((n Int)) (=> (= n 0) (= (Q n) 0))))
(assert (forall ((n Int)) (=> (= n 0) (= (R n) X))))
(assert (forall ((n Int)) (=> (> n 0) (= (R (+ n 1) ) (+ (R n) (* 2 Y))))))
(assert (forall ((n Int)) (=> (> n 0) (= (Q (+ n 1) ) (- (Q n) 2)))))
(assert (forall ((n Int)) (=> (> n 0) (= X (+ (* (Q n) Y) (R n))))))
(assert (forall ((n Int)) (= X (+ (* (Q n) Y) (R n)))))
(assert (= X (+ (* (Q k) Y) (R k))))
(assert  (not (= (* X 2) (+ (* (Q (+ k 1)) Y) (R (+ k 1))))))
(check-sat)

同样，当我在 z3py 中尝试使用以下代码时，我得到了错误的结果 unsat

from z3 import *
x=Int('x')
y=Int('y')
k=Int('k')
n1=Int('n1')
r=Function('r',IntSort(),IntSort())
q=Function('q',IntSort(),IntSort())
s=Solver()
s.add(x>=0)
s.add(y>0)
s.add(ForAll(n1,Implies(n1==0,r(0)==x)))
s.add(ForAll(n1,Implies(n1==0,q(0)==0)))
s.add(ForAll(n1,Implies(n1>0,r(n1+1)==r(n1)-(2*y))))
s.add(ForAll(n1,Implies(n1>0,q(n1+1)==q(n1)+(2))))
s.add(x==q(k)*y+r(k))
s.add(not(2*x==q(k+1)*y+r(k+1)))
if sat==s.check():
    print s.check()
    print s.model()
else :
    print s.check()

期待建议。

Answer 1

我的建议是使用名为 Not 的 Z3 函数替换内置 not 运算符，例如

not(2*x==q(k+1)*y+r(k+1))

在 Z3 看到它之前被 Python 简化为 False，而

Not(2*x==q(k+1)*y+r(k+1))

具有所需的含义。

z3 和 z3PY 给出不同的结果

z3 and z3PY giving different results

z3

z3py