从Z3（版本4）的无核心

Question

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

有没有一种方法可以在不通过第4版假设的情况下获得不合格核心？长期的解决方案当然是转向最新版本，但是如果有一个不太具有破坏性的解决方案将会很好。例如，有没有一种方法可以从不合格证明中提取不合格核心（由Z3.solver_get_proof返回）？

谢谢！

Answer 1

如果您使用Solver模块中的assert_and_track函数，则同样在Solver模块中的get_unsat_core将返回跟踪的断言相对应的一组跟踪文本。在UnsatCoreAndProofExample2方法和Java（https://github.com/Z3Prover/z3/blob/master/examples/java/JavaExample.java）中使用assert_and_track作为C＃API的示例。 ML样本中没有相应的例子，但是对OCaml的翻译不应太复杂。