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

【问题标题】：Convert SMT-LIBv2 QF_AUFBV to CNF DIMACS format using Z3使用 Z3 将 SMT-LIBv2 QF_AUFBV 转换为 CNF DIMACS 格式
【发布时间】：2015-09-08 03:32:57
【问题描述】：

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

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

【问题讨论】：

标签： z3 smt sat

【解决方案1】：

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

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

【讨论】：

感谢您的回答！我添加了对 m_solver.display_dimacs(std::cout); 的调用到名为 sat_tactic.cpp 的 Z3 文件中的运算符函数。但是，当我使用 smt2 输入文件调用 Z3 时，它只会在 std::out 上打印“sat”。你能告诉我我应该把display_dimacs放在哪里吗？再次感谢！
还有一件事：是否也可以将 SMT2 实例中的变量名的映射作为 CNF DIMACS 文件中的 cmets 输出？