1

因此，我可以使用在表示量词的表达式上调用 Z3_get_quantifier_bound_name 来获取与量词的边界相关联的名称。但是假设我正在遍历量化子公式的 AST。那时是否可以访问索引的名称？谢谢你。

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

1 回答 1

1

作为变量的表达式没有与其直接关联的名称。我们访问名称的方式是维护一个堆栈，这些名称来自在向下遍历的量词中。因此，维护符号的向量（堆栈/列表），并且每当您遍历量词时，将来自量词的绑定名称推送到向量上。遍历完量词后，您必须弹出名称。

您可以使用以下 API 访问绑定变量的名称：

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

请注意，量化变量的索引从右到左排序。因此，如果 Z3_get_quantifier_num_bound(context, expr) 返回 2，并且 x = Z3_get_quantifier_bound_name(context, expr, 0) y = Z3_get_quantifier_bound_name(context, expr, 1) 那么 y 的索引为 0，x 的索引为 1。

于 2012-11-13T08:44:23.607 回答