Как получить индекс переменной из записи func_interpr?

Question

Как получить индекс переменной из записи func_interpr?

Функциональная модель содержит записи пар <condition_on_args, return_value>,

return_value выражение может ссылаться на входные аргументы, например (f!4 (k!3 (:var 0))), Вот (:var 0) ссылается на 0-й входной аргумент модели функции и имеет вид Z3_VAR_AST.

Я хочу преобразовать return_value к некоторому внутреннему представлению программы, но не знаю, как относиться (:var 0) 0-й входной аргумент функциональной модели.

Как получить индекс переменной, то есть 0от expr (:var 0) типа Z3_VAR_AST через c / c ++ API?

Спасибо!

1

api c++z3

Решение

Другие решения

Других решений пока нет …

Источник

Accepted Answer

Вы должны использовать следующий 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);

1