z3 und z3PY unterschiedliche Ergebnisse

Question

geben Wenn ich in z3 folgenden versucht, I Ergebnis Timeout

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

Gleiche, als ich versuchte in z3py mit folgenden Code bekam, habe ich unsat deren Ergebnis ist falsch

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

Ich freue mich auf Vorschläge.

Answer 1

Mein Vorschlag ist es, den eingebauten not-Operator durch die Z3-Funktion Not, z.

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

wird False durch Python vereinfacht vor Z3 es zu sehen bekommt, während

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

die gewünschte Bedeutung hat.