python - 定点 Z3 中的解释

Question

当我在定点 Z3Py 中启用解释生成选项时，我得到一个包含以下消息的核心转储。

设置“DL_GENERATE_EXPLANATIONS”时出错，原因：未知选项。
抛出“z3_error”实例后调用终止（核心转储）

我在 Ubuntu 12.04 上使用 Z3 4.2，并且在“说明”部分的 Z3Py 文档中给出的示例出现错误。

我想知道可能是什么导致了这个问题。

Answer 1

定点引擎的选项将在 4.2 中发生变化。该文档适用于最后一个版本 4.1。您可以通过直接在定点对象上设置选项来将选项设置为 Z3。这类似于在求解器对象和策略对象上管理选项的方式。例子，

fp = Fixedpoint()
fp.set(engine='datalog',generate_explanations=True)

Answer 2

以上对我不起作用。我用了：

fp.set('datalog.generate_explanations', True)

使用 z3 4.8.5 python 包。