z3 - Z3的数据记录格式的输入

Question

我正在寻找 fixpoint Z3 接受的数据记录输入格式的示例、规范或文档。我在源代码分发中寻找过它们，但没有找到。它们是否可以在线或在任何报告/论文中使用？

Answer 1

我想你的问题是关于带有“.datalog”后缀的文件。
在线教程说:“使用 BDDBDDB 格式解析后缀为 .datalog 的文件。该格式可用于与 BDDBDDB 工具进行基准比较。”
我相信应该有相当数量的文件示例
BDDBDDB 工具从该工具的分发页面接受。我们的解析器可能有一些不兼容，因为我不知道这种语言的规范。

您还可以以 SMT2 格式输入数据记录问题。
SMT2 的扩展很少，我们在 http://research.microsoft.com/en-us/people/nbjorner/bmr-smt.pdf 中对其进行了描述。