ctx-solver-simplify（和类似的策略）是否产生等效的公式，或者只是 SAT 等效，或者我做的事情完全错误？

Question

我正在尝试制作 z3（我正在使用 z3py）来为我简化一些公式（这样我就可以或多或少地获得人类可读的输出）。使用ctx-solver-simplify 策略对我来说似乎是一个不错的选择，因为在几次传递中它会产生很好的紧凑公式。但很快我就遇到了ctx-solver-simplify 的输出似乎与原始公式不等价的情况（它看起来更像是可满足性等价的）。另外，我可能没有正确处理战术。

这就是我想要做的：http://rise4fun.com/Z3Py/g5sX。所以，我构造了一个公式Set2（Set2 定义之前的所有内容都只是定义它所需的设置），它有一个特别令人满意的分配。应用ctx-solver-simplify 后，我得到了一个公式（作为目标），但这个任务并不令人满意。那我到底哪里错了？

• 假设ctx-solver-simplify 会产生等效公式，我错了吗？
• 我是否以错误的方式处理战术及其输出？
• 还有别的吗？

谢谢。

Answer 1

我一直在研究这个问题，但到目前为止无法直接重现该错误 与我们当前的分支。上下文简化器中的一个错误已在不久前修复，它可以 通过 Z3 的在线版本来表现自己。 我仍然可以做一些事情来仔细检查我们是否可以重现错误 我会用我的发现更新这篇文章。