1

有限ドメインの変数 (ブール型や列挙型など) のすべての可能な値を取得しようとしていますが、Z3 で正しい方法がわかりません。以下のようなことを書きましたが、Z3 でこれを行うためのより良い方法があるかどうかを知りたいです。また、変数が有限ドメインか無限ドメインかを判断する方法はありますか?

以下では、vsort は変数のソート値です (例: Int('x').sort()) 

if vsort.kind() == Z3_BOOL_SORT:
    return [BoolVal(True), BoolVal(False)]
elif vsort.kind()  == Z3_DATATYPE_SORT:
    return [vsort.constructor(i)()
            for i in range(vsort.num_constructors())]
else:
    raise AssertionError('dont know how to deal with this sort')
4

1 に答える 1

2

あなたは正しい方向にいます。ただし、コードには 2 つの重要なケースがありません。ビットベクトルと、列挙型ではない有限データ型 (有限型のペアなど) です。これら 2 つの追加のケースを考慮したコードを次に示します。この関数universe(s)は、 sort のユニバース内の要素を返しますs。

ところで、考えられる改善は、リストの代わりにイテレータを使用することです。したがって、整数や再帰的なデータ型 (リストなど) などの無限の並べ替えをサポートし、必要に応じて要素を生成することもできます。

from z3 import *
import itertools

def universe(vsort):
    found = set()
    def rec(vsort):
        id = Z3_get_ast_id(vsort.ctx_ref(), vsort.as_ast())
        if id in found:
            raise AssertionError('recursive sorts are not supported')
        found.add(id)
        ctx = vsort.ctx
        if vsort.kind() == Z3_BOOL_SORT:
            return [ BoolVal(False, ctx), BoolVal(True, ctx) ]
        elif vsort.kind() == Z3_BV_SORT:
            sz = vsort.size()
            return [ BitVecVal(i, vsort) for i in range(2**sz) ]
        elif vsort.kind()  == Z3_DATATYPE_SORT:
            r = []
            for i in range(vsort.num_constructors()):
                c = vsort.constructor(i)
                if c.arity() == 0:
                    r.append(c())
                else:
                    domain_universe = []
                    for j in range(c.arity()):
                        domain_universe.append(rec(c.domain(j)))
                    r = r + [ c(*args) for args in itertools.product(*domain_universe) ]
            return r
        else:
            raise AssertionError('dont know how to deal with this sort')
    return rec(vsort)

ここではいくつかの例を示します。

print universe(BoolSort())
>> [False, True]
print universe(BitVecSort(4))
>> [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
S, elems = EnumSort('S', ['a', 'b', 'c', 'd'])
print universe(S)
>> [a, b, c, d]


# Create a Pair (Bool, S)
d = Datatype('Pair')
d.declare('mkpair', ('bval', BoolSort()), ('sval', S))
D = d.create()
print universe(D)
>> [mkpair(False, a), mkpair(False, b), mkpair(False, c), mkpair(False, d), mkpair(True, a), mkpair(True, b), mkpair(True, c), mkpair(True, d)]

# Create a Choice sort where each element is a Pair or a BitVector of size 4.
c = Datatype('Choice')
c.declare('aspair', ('pval', D))
c.declare('asbv', ('bval', BitVecSort(4)))
C = c.create()
print universe(C)
>> [aspair(mkpair(False, a)), aspair(mkpair(False, b)), aspair(mkpair(False, c)), aspair(mkpair(False, d)), aspair(mkpair(True, a)), aspair(mkpair(True, b)), aspair(mkpair(True, c)), aspair(mkpair(True, d)), asbv(0), asbv(1), asbv(2), asbv(3), asbv(4), asbv(5), asbv(6), asbv(7), asbv(8), asbv(9), asbv(10), asbv(11), asbv(12), asbv(13), asbv(14), asbv(15)]

l = Datatype('List')
l.declare('cons', ('car', BoolSort()), ('cdr', l))
l.declare('nil')
List = l.create()
print universe(List)
>> Traceback (most recent call last):
>> ...
>> AssertionError: recursive sorts are not supported
于 2013-01-24T22:23:18.550 に答える