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でのZ3SMT2アプローチに相当するものを知っている人はいますか？

ありがとうございました

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 に答える