1

So, I can obtain the names associated with bounds of the quantifier using Z3_get_quantifier_bound_name called on the expression representing quantifier. But suppose I'm traversing an AST of quantified subformula. Is it possible to access the name of the index at that point? Thank you.

if (z3_expr.is_var())
{
    // is it possible at this point to get the name of the quantified variable, 
    // which was associated with it at quantifier creation?
}
Egbert
  • 157
  • 9

1 Answers1

1

Expressions that are variables don't have names directly associated with them. The way we access the names is by maintaining a stack of the names from the quantifiers that were traversed on the way down. So maintain a vector (stack/list) of symbols, and whenever you traverse a quantifier push the bound names from the quantifier onto the vector. You will have to pop the names after you are done traversing the quantifier.

You use the following APIs to access the names of bound variables:

 unsigned Z3_API Z3_get_quantifier_num_bound(__in Z3_context c, __in Z3_ast a);

 Z3_symbol Z3_API Z3_get_quantifier_bound_name(__in Z3_context c, __in Z3_ast a, unsigned i);

Note that indices of quantified variables are ordered right-to-left. So if Z3_get_quantifier_num_bound(context, expr) returns 2, and x = Z3_get_quantifier_bound_name(context, expr, 0) y = Z3_get_quantifier_bound_name(context, expr, 1) then y has index 0 and x has index 1.

Nikolaj Bjorner
  • 8,229
  • 14
  • 15
  • Thanks, I see, I expected that. What happens when we have nested quantifiers? does the numeration of indexes continue? I assume, I should use Z3_get_index_value to get the index number given a variable expression. – Egbert Nov 13 '12 at 12:52
  • Yes X2, the enumeration continues, and `Z3_get_index_value` retrieves the de-Bruijn index of a variables. See this answer for more code examples: http://stackoverflow.com/questions/11816626/understanding-the-indexing-of-bound-variables-in-z3 – Leonardo de Moura Nov 13 '12 at 13:46