(:var 0) 在 z3 量词的主体中

Question

当我得到 Z3 OCaml API 的量词正文时，例如一个字符串为

的量词

(exists ((u_1 Int)) (= u_1 x5))

通过Quantifier.get_body，我得到表达式

(= (:var 0) x5)

我猜这个表达式中的 (:var 0) 是将 u_1 重命名为一个新变量，但我不知道表达式 (:var 0) 是什么类型以及如何匹配当我们想要从它的主体及其绑定变量重建量词时，它回到 u_1 。

有人可以提出解决方案吗？非常感谢。

Answer 1

我得到了解决方案。表达式 e

(:var 0)

是VAR_AST的表达式。您可以通过

查看

AST.is_var (Expr.ast_of_expr e)

然后，您可以通过

得到它的索引，例如0

Quantifier.get_index e

使用索引，您可以轻松地将表达式 e 与其绑定变量相匹配。注意一个量词的绑定变量列表可以通过

获得

Quantifier.get_bound_variable_names