In Z3Py, I have a formula. How can I retrieve the list of variables using in the formula?
Thanks.
Vu Nguyen contributed several useful procedures to Z3Py.
He implemented a procedure get_vars
to collect the list of used variables.
This procedure and many others can be found here.
His contributions will be available in the next official release.
Here is a version of get_vars
that can be executed online at rise4fun.
# Wrapper for allowing Z3 ASTs to be stored into Python Hashtables.
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)
def get_vars(f):
r = set()
def collect(f):
if is_const(f):
if f.decl().kind() == Z3_OP_UNINTERPRETED and not askey(f) in r:
r.add(askey(f))
else:
for c in f.children():
collect(c)
collect(f)
return r
x,y = Ints('x y')
a,b = Bools('a b')
print get_vars(Implies(And(x + y == 0, x*2 == 10),Or(a, Implies(a, b == False))))
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With