z3py unsat 核心与 z3.Optimize() 一起使用答案

【问题标题】：Usage of z3py unsat cores together with z3.Optimize()z3py unsat 核心与 z3.Optimize() 一起使用
【发布时间】：2018-06-19 17:33:38
【问题描述】：

我正在使用 z3 python api。我想一方面使用 Z3 的未满足核心功能，另一方面能够针对某些标准进行优化。

因此，如果我确实想使用 unsat 核心，我会执行以下操作：

self.solver = z3.Solver()
self._solver.assert_and_track(constraint1, error_message1)
self._solver.assert_and_track(constraint2, error_message2)
...
self._solver.check()

if len(self._solver.unsat_core()) > 0
  print (self._solver.unsat_core())

效果很好。但我还希望能够使用 z3.Optimize() 中的最大化（）和最小化（）函数。虽然这个求解器实例似乎不提供 unsat 核心。可以一起用吗？

我还在网上看到，除了使用 assert_and_track() 函数之外，还可以使用隐含来跟踪未饱和核心：隐含（p1，约束 1）。这里有什么区别？

【问题讨论】：

标签： python z3 z3py

【解决方案1】：

Z3 不支持同时优化和 unsat-core 生成。这是大约两个月前的相关票证：https://github.com/Z3Prover/z3/issues/1577

请注意，这并不是因为它无法实现：只是他们还没有实现它。在那里注册您的请求可能会激励他们增加支持！

关于您使用暗示跟踪 unsat-cores 的问题：我相信这基本上就是 assert_and_track 所做的。你可以在这里查看它的源代码：https://github.com/Z3Prover/z3/blob/d2c937a989ea360e9cba06583eccaa257c75870f/src/api/python/z3/z3.py#L6418-L6446 难道它不适合你吗？

【讨论】：