z3 - Z3Py - 获取包含表达式的所有公式

Question

在 Z3Py 中，是否可以获得出现某些变量/表达式的所有公式的列表？一个例子：

s.add(x < 0)
s.add(x > y)
print s[y]
>>> x > y

Answer 1

Z3 API 不包含此功能。但是，它可以在 Z3 API 之上实现。这是一个简单的实现：

from z3 import *

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

# Return True iff f contains t.
def contains(f, a):
    visited = set() # Set of already visited formulas
    # We need to track the set of visited formulas because Z3 represents them as DAGs. 
    def loop(f):
      if askey(f) in visited:
          return False # already visited
      visited.add(askey(f))
      if f.eq(a):
          return True
      else:
          for c in f.children():
              if loop(c):
                  return True
          return False
    return loop(f)

# Return the set of assertions in s that contains x
def assertions_containing(s, x):
    r = []
    for f in s.assertions():
        if contains(f, x):
            r.append(f)
    return r

x = Real('x')
y = Real('y')
s = Solver()
s.add(x < 0)
s.add(x > y)
print assertions_containing(s, y)
print assertions_containing(s, x)