CODEWITHSUNDEEP
pythonz3
Vu Nguyen
Vu Nguyen

Reputation: 1007

Z3: finding all possible values of a variable

I try to obtain all possible values of a variable of a finite domain (e.g. Bool and Enumerated type) but not sure what would be the correct way to do so in Z3. I've written something like below but want to know if there is better way for doing so in Z3. Also, is there a way to figure out if a variable has a finite or infinite domain ?

In the following, vsort is the sort value of a variable (e.g. 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')

Upvotes: 1

Views: 1004

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

You are in the right direction. However, the code is missing two important cases: bit-vectors, and finite datatypes that are not enumeration types (example, a pair of finite types). Here is the code that consider these two extra cases. The function universe(s) returns the elements in the universe of sort s.

BTW, a possible improvement is to use iterators instead of lists. Thus, we could even support infinite sorts such as integers and recursive datatypes (e.g., lists), and generate the elements on demand.

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)

Here are some examples:

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

Upvotes: 2

Related Questions