z3 获取符号变量 C++ API 的大小

Question

我正在使用Z3_parse_smtlib2_string 来解析 smtlib2 公式。公式如下：

(set-logic QF_AUFBV)(declare-fun SymVar_0 () (_ BitVec 32))(declare-fun SymVar_1 () (_ BitVec 8))...

我使用以下方法解析它：

Z3_ast ast = Z3_parse_smtlib2_string(ctx, (Z3_string)formula, 0, 0, 0, 0, 0, 0);

假设我现在想要获得SymVar_0 的大小（它应该返回 32）。我该怎么做？

谢谢

Answer 1

名为Z3_get_bv_sort_size 的函数应该可以完成这项工作。请注意，这是一个 C（不是 C++）函数，因此您还必须提供上下文。

为了其他面临类似问题的用户的利益：Z3 中没有可让您查找名称类型的符号表。您可以通过遍历所有子表达式并记录在此过程中遇到的所有符号及其类型来自己创建一个。有关 Python 中的示例，请参阅Z3py: how to get the list of variables from a formula?。