1

Wonder if Z3 java bindings has get_vars() API, to get all the variables in the formula?

Betsy
  • 95
  • 5
  • Not sure what this question is about. I just checked, and there doesn't seem to be a get_vars() function in the Z3 Python API. Are you talking about the Python built-in function called vars() that can be used to get class variables etc? – Christoph Wintersteiger Mar 06 '14 at 01:08
  • Are you looking for a function that extracts a list of all "variables" (quantified vars or constant function applications) from a given expression? As far as I know neither is provided in neither API, but it is easy to implement by traversal of Exprs. – Christoph Wintersteiger Mar 06 '14 at 01:10
  • @ChristophWintersteiger Just as this post [link](http://stackoverflow.com/questions/14080398/z3py-how-to-get-the-list-of-variables-from-a-formula) mentioned. – Betsy Mar 06 '14 at 22:19
  • This is an external contribution to the Python API only, it's not available in the other APIs. That said however, this particular function can be implemented very similarly in Java. – Christoph Wintersteiger Mar 12 '14 at 15:51

0 Answers0