CODEWITHSUNDEEP
z3z3py
Tom
Tom

Reputation: 934

z3 and z3PY giving different results

When I tried following in z3, I got result 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)

Same when I tried in z3py using following code, I got result unsat which is wrong 

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

Looking forward to Suggestions.

Upvotes: 1

Views: 136

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8402

My suggestion is to use replace the built-in not operator by the Z3 function called Not, e.g.

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

is simplified to False by Python before Z3 gets to see it, while 

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

has the desired meaning.

Upvotes: 1

Related Questions