c++ - 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? .