如何使用量词访问 Z3 表达式 [英] How to visit Z3 expressions with quantifiers

问题描述

我想访问一个z3::expr.示例目录提供了以下代码段:

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.

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

1. When e.is_quantifier() is true, how to I get which quantifier (exists or for all) I have?

我知道 Z3 在内部使用 De Bruijn 索引，我对它们没意见.但是当 e.is_var() 为真时，我如何获得索引?

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?

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

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)

推荐答案

我设法编写了一些基于 C API 的 C++ API，复制了 Z3 中已经实现的类似功能.

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

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

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

这篇关于如何使用量词访问 Z3 表达式的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！