1

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

(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。这很有效，我可以非常快速地解决对它的约束。

我在以下数据类型上使用 z3 公理尝试了与 Z3py 类似的方法：

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 中编码我的算术的另一种方法。

有谁知道 z3py 中上述 Z3 SMT2 方法的等价物是什么？

谢谢

4

1 回答 1

2

在 Z3Py 中，您应该定义msum为：

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

这相当于您在 SMT2 前端所做的。在你这样做并删除通用公理之后，Z3Py 也会找到解决方案。

这是完整的示例（可在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()
于 2012-12-11T20:14:37.200 回答