z3 - 使用 Z3 将 SMT-LIBv2 QF_AUFBV 转换为 CNF DIMACS 格式

Question

我可以将具有 SMT-LIBv2 格式并包含 set-logic QF_AUFBV 的输入文件转换为 CNF 吗？如果是这样，我该如何使用 Z3 命令行统一性来做到这一点？

更新：我还需要将变量从 SMT-LIBv2 实例映射到 CNF DIMACS 文件作为注释。用Z3可以吗？

Answer 1

QF_AUFBV 包含数组和未解释的函数。我不认为 CNF DIMACS 了解这些。

通过程序化 API，您可以应用将公式转换为 CNF 的策略。然后，您可以遍历这些公式并以您喜欢的任何形式漂亮地打印它们。Z3 源代码还包含一些我们将中间结果转储到 DIMACS 的地方，但我们没有为此公开准备使用的功能（但您始终可以为此需要编译您自己的 Z3 版本，例如，使用“目标::display_dimacs”实用程序。