Z3Py - Get all formulas containing an expression

Question

In Z3Py, is it possible to get a list of all formulas where some variable/expression occurs? An example:

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

Answer 1

The Z3 API does not contain this functionality. However, it can be implemented on top of the Z3 API. Here is a simple implementation:

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)