ocaml - Z3 的 Unsat 核心（版本 4）

Question

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

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

谢谢！

Answer 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应该不会太复杂。