title: How to extract sub-formulas(predicates, terms) in Z3 efficiently?
body: <p>Suppose I want to extract all sub-formulas(predicates, terms) from a given constraint with  the type of BoolExpr and here are two examples: </p>
  
  <pre><code>(f(x)=2 and f(y)=3) or (f(z)=1 and f(y)=3)
  The output should be f(x)=2, f(y)=3 and f(z)=1.
  
  (p and q) or (p or r) and (p and (q or r))
  The output should be p, q and r.
  </code></pre>
  
  <p>A naive way would be traversing the entire AST and recording all the unique sub-formulas. This is unpleasant when there are bunch of redundant nodes in the AST and we have to perform such extraction frequently.
  I was wondering if there exists a clean and efficient way to do this.</p>
  
  <p>I am using the Java API for Z3.</p>