【发布时间】：2012-10-26 20:20:29
【问题描述】：
我正在寻找 Fixpoint Z3 接受的数据记录输入格式的示例、规范或文档。我在源代码分发中寻找过它们，但没有找到。它们是在线提供还是在任何报告/论文中提供？
【问题讨论】：
标签： z3
【发布时间】：2012-10-26 20:20:29
【问题描述】：
我认为您的问题是关于带有“.datalog”后缀的文件。 在线教程说：“使用 BDDBDDB 格式解析后缀为 .datalog 的文件。该格式可用于与 BDDBDDB 工具进行基准比较。” 我相信应该有相当数量的文件示例 BDDBDDB 工具从该工具的分发页面接受。我们的解析器可能有一些不兼容的地方，因为我不知道这种语言的规范。
您还可以输入 SMT2 格式的数据记录问题。 SMT2 的扩展很少，我们在http://research.microsoft.com/en-us/people/nbjorner/bmr-smt.pdf 中描述了它们
【讨论】：
-
bddbddb 支持 "Gt("a", "d")?" 形式的查询。我将此查询添加到“基本数据记录”部分下的定点 Z3 文档中给出的示例数据记录程序的末尾，并运行了 bddbddb 和 Z3。但是，Z3 似乎不支持这种语法。 Z3的“.datalog”输入格式是否有其他语法查询？
输入格式在以下在线教程中有所描述。
- http://rise4fun.com/Z3/tutorial/fixedpoints（SMT 2.0 前端）
- http://rise4fun.com/Z3Py/tutorial/fixedpoints（Python 前端）
【讨论】：
-
非常感谢！顺便说一句，上面的python doc页面没有描述输入数据日志文件的输入格式。
-
是的，没错。它展示了如何使用 Python 直接访问数据记录引擎。