Z3py get_vars(f) equivalent for Java

Question

Following up on this post: There is an example implementation how to get free variables with python here which I wanted to re-implement in Java. How do I access the children of an Expr? I did not find a getter or visitor.

Answer 1

You can visit subexpressions by recursing over the following three cases:

1. An expression can be a variable Expr.isVar()
2. An expression can be a quantifier Quantifier.isUniversal()/isExistential(), call getBody() to get child.
3. An expression can be an application, Expr.isApp(), use Expr.getArgs() to access the children.