z3 - Z3py: 数式から変数のリストを取得する方法は?

Question

Z3Py には式があります。数式で使用して変数のリストを取得するにはどうすればよいですか?

ありがとう。

Answer 1

Vu Nguyenは、Z3Pyにいくつかの有用な手順を提供しました。get_vars彼は、使用された変数のリストを収集する手順を実装しました。この手順と他の多くの手順はここにあります。彼の貢献は、次の公式リリースで利用できるようになります。これは、 rise4funget_varsでオンラインで実行できるバージョンです。

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