CODEWITHSUNDEEP
z3z3py
Tom
Tom

Reputation: 934

Why result of Z3 online and Z3PY are different?

Following code I have tried in Online and Offline 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)

Result unsat

Following code I have tried in 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))

result- unknown

Is processing power different?

Upvotes: 0

Views: 397

Answers (2)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8393

The reason for the difference in results is because the input is not the same. For instance, the expression

(N1+1)**2

is semantically the same as

(* (+ N1 1) (+ N1 1))

but because of the syntactic difference, Z3 will not simplify the formula to something that it can solve easily. The syntactically equivalent problem in Python is

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

which yields the desired result.

Upvotes: 3

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

Are the constraints the same? I don't see the python variant of:

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

Upvotes: 0

Related Questions