Z3 SMT 2.0 与 Z3 py 实现 [英] Z3 SMT 2.0 vs Z3 py implementation

问题描述

我正在尝试对 Z3 中具有恒定无穷大的正实数进行算术编码.我在SMT2中使用以下对编码成功获得了结果

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

其中一对 (true, _) 编码无穷大，而 (false, 5.0) 编码实数 5.这是有效的，我可以非常快速地解决它的约束.

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.

我在 Z3py 上尝试了类似的方法，使用 z3 公理对以下数据类型进行处理:

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

我无法让它工作(超时).我想问题在于试图证明一致性公理.但是我找不到在 Z3py 中编码我的算法的另一种方法.

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.

有没有人知道z3py中Z3 SMT2方法的等价物是什么?

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

谢谢

推荐答案

在 Z3Py 中，您应该将 msum 定义为:

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

这相当于你在 SMT2 前端所做的.在你这样做并移除普遍公理之后，Z3Py 也会找到解决方案.

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.

这是完整的示例(可在 http://rise4fun.com/Z3Py/Lu3 在线获得):

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 与 Z3 py 实现的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！