如何从 func_interpr 条目中获取变量的索引？

Question

一个函数模型包含成对的条目<condition_on_args, return_value>。

return_value 表达式可以引用输入参数，例如(f!4 (k!3 (:var 0)))。这里(:var 0)指的是函数模型的第0个输入参数，它的类型是Z3_VAR_AST。

我想将return_value 转换为一些内部程序表示，但不知道如何将(:var 0) 与函数模型的第 0 个输入参数相关联。

如何通过 c/c++ API 从种类 Z3_VAR_AST 的 expr (:var 0) 获取变量的索引，即 0？

谢谢！

Answer 1

您必须使用以下 API：

    /**
       \brief Return index of de-Brujin bound variable.

       \pre Z3_get_ast_kind(a) == Z3_VAR_AST

       def_API('Z3_get_index_value', UINT, (_in(CONTEXT), _in(AST)))
    */
    unsigned Z3_API Z3_get_index_value(__in Z3_context c, __in Z3_ast a);