set operations over Z3 expressions

Question

Are there functions defining set operations , e.g set, intersection, union, members etc , over Z3 expressions ? Also, are there functions to check if a formula is a cnf or dnf ?

If not I can try to implement them in the z3utils file.

Leonardo de Moura Leonardo de Moura · Accepted Answer · 2013-01-13T17:41:34

We can use Python sets to encode sets of expressions. The only problem is that the operator __eq__ for Z3Py expressions will build a new expression instead of comparing whether to expressions are equal or not. To fix that, we can use a wrapper that invokes the correct compares Z3 expressions. Here is a sample (available online at rise4fun).

class AstRefKey:
    def __init__(self, n):
        self.n = n
    def __hash__(self):
        return self.n.hash()
    def __eq__(self, other):
        return self.n.eq(other.n)
    def __repr__(self):
        return str(self.n)

def askey(n):
    assert isinstance(n, AstRef)
    return AstRefKey(n)

x = Int('x')
s = set()
s.add(askey(x+1))
s.add(askey(x))
print s
print askey(x + 1) in s
s2 = set()
s2.add(askey(x+2))
s2.add(askey(x))
print s2
print s.union(s2)

The only inconvenience is that we have to keep using askey. We can avoid this inconvenience by defining a class ASTSet that wraps a Python set object an invokes askey for us.

Regarding, dnf and cnf recognizers. This functionality is not exposed in the external APIs.

set operations over Z3 expressions

1 Answers