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_to_app 如有必要)，其他 AST 类型可能没有要遍历的参数(例如，vars 和数字，请参阅 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屋！