Z3py:如何从公式中获取变量列表? [英] Z3py: how to get the list of variables from a formula?

问题描述

在 Z3Py 中，我有一个公式.如何检索公式中使用的变量列表?

In Z3Py, I have a formula. How can I retrieve the list of variables using in the formula?

谢谢.

推荐答案

Vu Nguyen 为 Z3Py 贡献了几个有用的过程.他实现了一个过程 get_vars 来收集使用过的变量列表.可以在此处找到此过程和许多其他过程.他的贡献将在下一个正式版本中提供.这是一个 get_vars 版本，可以在 rise4fun 上在线执行.

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))))

这篇关于Z3py:如何从公式中获取变量列表?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！