不幸的是，我没有足够的声誉来评论其他问题的答案。所以我必须开始一个新的问题。
基本上我有与这里描述的相同的问题。我想使用 Z3 进行增量求解。为了让约束进入 Z3，我使用 smtlib2 字符串。第一组约束一切正常，我可以将变量声明等直接放入 smtlib2 字符串中。当增量添加附加约束时，Z3_parse_smtlib2_string 需要接收先前声明的数量 (unsigned num_decls)、声明 (Z3_func_decl const decls[]) 及其名称 (Z3_symbol const decl_names[])。对于 smtlib 字符串，Parser 接口提供检索此信息的函数，例如“Z3_get_smtlib_num_decls”和“Z3_get_smtlib_decl”。但是，它们不适用于 smtlib2 字符串。
有一个使用模型的解决方法。对于此解决方法，Z3 必须返回包含每个已声明变量的模型（“完整模型”），默认情况下似乎并非如此。此处已描述了此问题的解决方案（针对 Z3 4.0）。不幸的是，这不再适用于 Z3 4.3。
有人知道我如何从 Z3 获得完整的模型，而不是依赖于使用的版本吗？甚至更好：同时是否有更直接的方法来检索声明？大约一年前，Leonardo de Moura 提到未来会有“Parser”对象支持检索 decl、公式等（参见Z3 4.0：获取完整模型）。这里有什么我还没有在文档中发现的新东西吗？
非常感谢！
伊丽莎白