2

There is no direct way in Z3 to traverse an already existing Z3_ast for an expression, that much seems clear to me from the API. Is there however an indirect way how to, e.g., split a conjunction, substitute a term for a term in a Z3_ast obtained for example by Z3_parse_smtlib2_string or as an interpolant obtained with Z3_get_interpolant (these are output from Z3, so it makes sense to be able to examine them).

jakubdaniel
  • 2,233
  • 1
  • 13
  • 20

1 Answers1

1

Traversal is possible, in the C API the functions for that are Z3_get_app_num_args and Z3_get_app_arg. However, this works only if the AST is a function application (an app, cast via Z3_to_app if necessary), other AST types may not have arguments to traverse (e.g., vars and numerals, see Z3_ast_kind).

Christoph Wintersteiger
  • 8,234
  • 1
  • 16
  • 30
  • The examples contain visitor patterns. For example under examples/c++ you will find the function called "visit". void visit(expr const & e) { if (e.is_app()) { unsigned num = e.num_args(); for (unsigned i = 0; i < num; i++) { visit(e.arg(i)); } // do something // Example: print the visited expression func_decl f = e.decl(); std::cout << "application of " << f.name() << ": " << e << "\n"; } else if (e.is_quantifier()) { visit(e.body()); ...etc. – Nikolaj Bjorner Sep 09 '15 at 09:30
  • Thanks, so is every AST that gets constructed from other ASTs always a function application (e.g. `eq`, `lt`, `+`, `and`)? I guess that would make sense. Then I guess that variables and such can be examined via `get_symbol` (to get the name), and `get_sort` (to get the sort), right? @NikolajBjorner: I completely missed there were examples. Thank you – jakubdaniel Sep 09 '15 at 09:31
  • No, but those that you mentioned are all function applications. Others include numerals, sort declarations, function declarations, bound (quantified) variables, and quantified expressions (they have a body, but no args), see Z3_ast_kind. – Christoph Wintersteiger Sep 09 '15 at 15:19
  • I am for example puzzled how to get a symbol for a `VAR_AST`. – jakubdaniel Sep 12 '15 at 12:19
  • VAR_ASTs are de-brujin indexed, bound variables, so primarily they have an index. To get a variable's name you need the corresponding QUANTIFIER_AST, which keeps a list of names that can be accessed via [Z3_get_quantifier_bound_name](http://z3prover.github.io/api/html/group__capi.html#gab554587e623297f7d953b030d71d08a6). – Christoph Wintersteiger Sep 14 '15 at 09:15
  • See also [Understanding the indexing of bound variables in Z3](http://stackoverflow.com/questions/11816626/understanding-the-indexing-of-bound-variables-in-z3), [Understanding the indexing of bound variables in Z3](http://stackoverflow.com/questions/11249646/z3-c-api-manage-z3-var-ast). – Christoph Wintersteiger Sep 14 '15 at 09:16