Z3 的 Unsat 核心（版本 4）答案

【问题标题】：Unsat core from Z3 (version 4)Z3 的 Unsat 核心（版本 4）
【发布时间】：2016-08-08 22:43:37
【问题描述】：

我在过去一年左右一直在使用 Z3 4.0 版的 Ocaml API，主要是位向量理论。现在我需要在执行 Z3.solver_check 后提取 unsat 核心，不幸的是版本 4 没有这种能力。我可以进行重写以使用假设来代表公式中的每个位向量方程，然后得到 unsat 核心，但这是代码的关键部分，它可能会影响整体性能。

有没有一种方法可以在不经过版本 4 假设的情况下获得 unsat 核心？长期的解决方案当然是迁移到最新版本，但如果有一个破坏性较小的解决方案，那就太好了。例如，有没有办法从 unsat 的证明（由 Z3.solver_get_proof 返回）中提取 unsat core？

谢谢！

【问题讨论】：

标签： ocaml z3 proof smt bitvector

【解决方案1】：

如果您使用 Solver 模块中的 assert_and_track 函数，则同样在 Solver 模块中的 get_unsat_core 返回与跟踪的断言对应的跟踪文字集。在 UnsatCoreAndProofExample2 方法和 Java (https://github.com/Z3Prover/z3/blob/master/examples/java/JavaExample.java) 中有一个使用 C# API 的 assert_and_track 的示例。 ML示例中没有对应的例子，但是翻译成OCaml应该不会太复杂。

【讨论】：

Z3 版本 4 中没有函数 Z3.solver_assert_and_track 或类似的东西。我的问题是针对版本 4 的。谢谢。