1

While I can see that there exists traversal for Z3 AST in C++ (outlined in this question), I can't find its equivalent method in Java api, is there a way by which I can traverse the Z3 AST in Java?

Thanks!

S. Nabil
  • 319
  • 1
  • 10

1 Answers1

1

I think the relevant functions are found here: https://github.com/Z3Prover/z3/blob/master/src/api/java/Expr.java

(I'm not a Java programmer, nor I have used these myself; so take this with a grain of salt!)

alias
  • 28,120
  • 2
  • 23
  • 40
  • I am not sure which part of it did you mean, I do not see visitor pattern supported there, nor do I see how is it possible access elements/objects for each expression, for example, I would expect to be able to visit lhs and rhs of a binary expression, but as far as I can see this isn't there. – S. Nabil Feb 24 '19 at 20:50
  • Good point. I think this is a better question to ask at their issues site: https://github.com/Z3Prover/z3/issues – alias Feb 24 '19 at 21:16
  • The `visit` function from the C++ example gives the strategy, the Java function names are different only in capitalization and the `get` prefix. In general there is no RHS or LHS; `expr`s have arbitrary numbers of arguments that can be inspected via `Expr.getNumArgs` and `Expr.getArgs()[index]`. – Christoph Wintersteiger Feb 25 '19 at 10:19
  • @ChristophWintersteiger, it isn't exactly the visitor pattern that you'd expect, but yes I guess that should do the job. Thank you very much! – S. Nabil Mar 09 '19 at 06:07