如何使用量词访问 Z3 表达式

Question

我想访问z3::expr。示例目录提供了这个 sn-p：

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
    }
}

函数应用部分我没问题，但是遇到量词时我错过了一些。

1. 当e.is_quantifier() 为真时，我如何获得我拥有的量词（存在或全部）？

2. 我了解 Z3 内部使用 De Bruijn 索引，我可以接受。但是e.is_var()为真时如何获取索引呢？

3. 不太重要，但 Z3 仍然保留绑定变量的名称，即使知道 De Bruijn 索引在技术上使其冗余，因为如果我将表达式发送到 std::cout 变量名称就会出现。我如何得到它？我可以假设它们是一致的，即，如果我盲目地用每个变量的名称替换每个变量，那么变量会以正确的方式绑定吗？ （如果我没记错的话，这相当于没有变量在其使用和原始绑定位点之间再次被量化）

Answer 1

我设法在 C API 的基础上编写了一些 C++ API，复制了 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;
}

这仍然没有对我的问题中第 3 点的后半部分给出明确的答案，但它是一个首发。