c++ - How to get an index of a variable from func_interpr entry?

Question

A function model contains entries of pairs <condition_on_args, return_value>.

The return_value expression may refer to input arguments, for example (f!4 (k!3 (:var 0))). Here (:var 0) refers to the 0th input argument of the function model, and it is of kind Z3_VAR_AST.

I want to transform return_value to some internal program representation, but don't know how to relate (:var 0) to 0th input argument of the function model.

How to get an index of the variable, that is 0, from expr (:var 0) of kind Z3_VAR_AST via c/c++ API?

Thanks!

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