How to visit Z3 expressions with quantifiers

Question

I would like to visit a z3::expr. The examples directory provides this snippet:

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());
        // do something
    }
    else { 
        assert(e.is_var());
        // do something
    }
}

I am ok with the function application part, but I miss some piece when I encounter quantifiers.

When e.is_quantifier() is true, how to I get which quantifier (exists or for all) I have?
I understand that Z3 internally uses De Bruijn indices, and I am ok with them. But how do I get the index when e.is_var() is true?
Less important, but Z3 still retains the name of the bound variable, even if knowing the De Bruijn index technically makes it redundant, because if I send the expression to std::cout the variable name appears. How do I get it? Can I assume that they are consistent, i.e., if I blindly subtitute each variable with its name, then variables bind in the correct way? (if I am not mistaken, this amounts to the fact that no variable is quantified again between its usage and its original binding site)

Giovanni Mascellani Giovanni Mascellani · Accepted Answer · 2018-04-13T18:51:40

I managed to write some C++ API based on the C API, copying from similar functions that are already implemented in Z3.

unsigned expr_get_num_bound(const z3::expr &e) {
    assert(e.is_quantifier());
    unsigned num = Z3_get_quantifier_num_bound(e.ctx(), e);
    e.check_error();
    return num;
}

z3::symbol expr_get_quantifier_bound_name(const z3::expr &e, unsigned i) {
    assert(e.is_quantifier());
    Z3_symbol sym = Z3_get_quantifier_bound_name(e.ctx(), e, i);
    e.check_error();
    return z3::symbol(e.ctx(), sym);
}

z3::sort expr_get_quantifier_bound_sort(const z3::expr &e, unsigned i) {
    assert(e.is_quantifier());
    Z3_sort sort = Z3_get_quantifier_bound_sort(e.ctx(), e, i);
    e.check_error();
    return z3::sort(e.ctx(), sort);
}

bool expr_is_quantifier_forall(const z3::expr &e) {
    assert(e.is_quantifier());
    Z3_bool is_forall = Z3_is_quantifier_forall(e.ctx(), e);
    e.check_error();
    return static_cast< bool >(is_forall);
}

unsigned expr_get_var_index(const z3::expr &e) {
    assert(e.is_var());
    unsigned idx = Z3_get_index_value(e.ctx(), e);
    e.check_error();
    return idx;
}

This still does not give a definitive answer to the second half of point 3 in my question, but it is a starter.

How to visit Z3 expressions with quantifiers

1 Answers