2

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

4

2 回答 2

2

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

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

于 2012-10-27T00:23:24.520 回答
1

The input format is described in the following online tutorials.

于 2012-10-26T21:39:43.407 回答