Z3 API：是否可以检查AST [英] Z3 API: Is inspection of AST possible

问题描述

Z3中没有直接方法遍历表达式中已经存在的 Z3_ast ，从API看来，这对我来说似乎很清楚。但是，是否存在一种间接方式，例如，如何拆分连词，用 Z3_ast 中的术语代替，例如 Z3_parse_smtlib2_string 或作为通过 Z3_get_interpolant 获得的插值（这些是从Z3输出的，因此能够检查它们很有意义）。

There is no direct way in Z3 to traverse an already existing Z3_ast for an expression, that much seems clear to me from the API. Is there however an indirect way how to, e.g., split a conjunction, substitute a term for a term in a Z3_ast obtained for example by Z3_parse_smtlib2_string or as an interpolant obtained with Z3_get_interpolant (these are output from Z3, so it makes sense to be able to examine them).

推荐答案

可以进行遍历，在C API中，其功能为 Z3_get_app_num_args 和 Z3_get_app_arg 。但是，仅当AST是函数应用程序（通过 Z3_to_app投射的应用程序（如果需要），其他AST类型可能没有遍历的参数（例如，变量和数字，请参见 Z3_ast_kind ）。

Traversal is possible, in the C API the functions for that are Z3_get_app_num_args and Z3_get_app_arg. However, this works only if the AST is a function application (an app, cast via Z3_to_app if necessary), other AST types may not have arguments to traverse (e.g., vars and numerals, see Z3_ast_kind).

这篇关于Z3 API：是否可以检查AST的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！