【发布时间】：2013-05-20 09:50:13
【问题描述】：
不幸的是，我没有足够的声誉来评论其他问题的答案。所以我必须开始一个新问题。
基本上我遇到了与here 描述的相同的问题。我想使用 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 必须返回包含每个已声明变量的模型（“完整模型”），默认情况下似乎并非如此。已描述了此问题的解决方案here（针对 Z3 4.0）。不幸的是，这不再适用于 Z3 4.3。
有人知道如何从 Z3 获得完整的模型，而不是依赖于使用的版本吗？ 甚至更好：同时是否有更直接的方法来检索声明？大约一年前，Leonardo de Moura 提到将来会有“Parser”对象支持检索decls、公式等（参见Z3 4.0: get complete model）。这里有什么我还没有在文档中发现的新内容吗？
非常感谢！
伊丽莎白
【问题讨论】：
标签： z3