0

I am using Z3py and trying to get the set of all the variables in any constraint in a Solver. I can call Solver.assertions() to get an ASTVector, then loop over this vector and get objects of type BoolRef, for example, but then I'm stuck. How can I recursively iterate over an assertion, a BoolRef instance for example, to get the individual variables?

Stanley Bak
  • 543
  • 3
  • 16
  • 1
    The set of variables/declarations exists inside the Solver, although the last I checked, it is not visible outside the C/C++ APIs (see, e.g.: http://stackoverflow.com/questions/13054054/parse-smt-lib2-string-using-declarations-in-existing-context ). Unless that's changed, an alternative is to just keep track of all the variables/declarations you've used yourself, then you'll have all of them available. If you want to go the recursive route instead, there are methods to walk the AST: http://stackoverflow.com/questions/15236450/substituting-function-symbols-in-z3-formulas/15237285#15237285 – Taylor T. Johnson Sep 10 '14 at 15:53

1 Answers1

1

Thanks Taylor for your answer. I think the second link addresses the question. In more detail, the python script that Leo added in the previous answer walks an AST, the AstMap ensures that shared sub-expressions are only walked once.

Nikolaj Bjorner
  • 8,229
  • 14
  • 15