Z3 SMT 2.0 vs Z3 py實現

Question

我試圖在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.這工作，我可以在它解決約束非常快。

我嘗試使用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方法的等價物是什麼？

謝謝

Answer 1

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