固定点Z3中的说明

Question

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

Error setting 'DL_GENERATE_EXPLANATIONS', reason: unknown option.
terminate called after throwing an instance of 'z3_error' Aborted (core dumped)

我在Ubuntu12.04上使用Z3 4.2，在Z3Py文档的“解释”部分得到了错误。在

我想知道是什么引起了这个问题。在

Answer 1

以上这些对我不起作用。我用过：

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

使用z34.8.5python包。在

Answer 2

对于4.2，fixedpoint引擎的选项将发生变化。 最后一个版本是文档。 通过直接在fixedpoint对象上设置选项，可以将选项设置为Z3。 这与如何在解算器对象和策略对象上管理选项类似。 例如

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