我正在尝试对 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)))
)
)
)
其中一对(真,_)编码无穷大,而(假,5.0)编码实数5。这有效,我可以非常快速地解决对它的约束。
我尝试了类似的 Z3py 方法,在以下数据类型上使用 z3 公理:
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 方法的等价物是什么?
谢谢
在 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()