Z3 SMT 2.0 vs Z3 py implementation

Question

I'm trying to encode an arithmetic for positive reals with a constant infinity in Z3. I successfully obtained the result in SMT2 with the following pair encoding

(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2)))))
(declare-const infty (Pair Bool Real))
(assert (= infty (mk-pair true 0.)))
(define-fun inf-sum ((p1 (Pair Bool Real)) (p2 (Pair Bool Real))) (Pair Bool Real)
  ( ite
     (first p1)
     p1
     (ite
       (first p2)
       p2
       (mk-pair false (+ (second p1) (second p2)))
      )
  )
)

where a pair (true, _) encodes infinity while (false, 5.0) encodes the real 5. This works and I can solve constraints over it very fast.

I tried a similar approach with Z3py using z3 axioms over the following datatype:

MyR = Datatype('MyR')
MyR.declare('inf');
MyR.declare('num',('r',RealSort()))

MyR = MyR.create()
inf = MyR.inf
num  = MyR.num
r  = MyR.r

r1,r2,r3,r4,r5 = Consts('r1 r2 r3 r4 r5', MyR)
n1,n2,n3 = Reals('n1 n2 n3')

msum = Function('msum', MyR, MyR, MyR)

s = Solver()

s.add(ForAll(r1, msum(MyR.inf,r1)== MyR.inf))
s.add(ForAll(r1, msum(r1,MyR.inf)== MyR.inf))
s.add(ForAll([n1,n2,n3], Implies(n1+n2==n3, 
  msum(MyR.num(n1),MyR.num(n2))== MyR.num(n3))))
s.add(msum(r2,r4)==MyR.num(Q(1,2)))
print s.sexpr()
print s.check()

I can't get it to work (it times out). I guess the problem is in trying to prove the consistency axioms. However I couldn't find another way to encode my arithmetic in Z3py.

Is anyone aware of what is the equivalent of the Z3 SMT2 approach of above in z3py?

Thank you

Leonardo de Moura Leonardo de Moura · Accepted Answer · 2012-12-11T20:14:37

In Z3Py, you should define msum as:

def msum(a, b):
    return If(a == inf, a, If(b == inf, b, num(r(a) + r(b))))

This is equivalent to what you did in the SMT2 frontend. After you do that and remove the universal axioms, Z3Py will also find the solution.

Here is the complete example (available online at http://rise4fun.com/Z3Py/Lu3):

MyR = Datatype('MyR')
MyR.declare('inf');
MyR.declare('num',('r',RealSort()))

MyR = MyR.create()
inf = MyR.inf
num = MyR.num
r   = MyR.r

r1,r2,r3,r4,r5 = Consts('r1 r2 r3 r4 r5', MyR)
n1,n2,n3 = Reals('n1 n2 n3')

def msum(a, b):
    return If(a == inf, a, If(b == inf, b, num(r(a) + r(b))))

s = Solver()
s.add(msum(r2,r4) == MyR.num(Q(1,2)))
print s.sexpr()
print s.check()
print s.model()

Z3 SMT 2.0 vs Z3 py implementation

1 Answers