В Z3Py у меня есть формула. Как я могу получить список переменных, используемых в формуле?
Спасибо.
В Z3Py у меня есть формула. Как я могу получить список переменных, используемых в формуле?
Спасибо.
Ву Нгуен внес в Z3Py несколько полезных процедур. Он реализовал процедуру get_vars
для сбора списка используемых переменных. Эту и многие другие процедуры можно найти здесь. Его работы будут доступны в следующем официальном выпуске. Вот версия get_vars
, которую можно запустить в Интернете по адресу 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))))