我正在尝试制作 z3 (我正在使用 z3py)来简化我的一些公式(以便我可以或多或少地获得人类可读的输出)。使用 ctx-solver-simplify 策略对我来说似乎是一个不错的选择，因为在几次传递中它会产生漂亮的紧凑公式。但很快我就遇到了一种情况，ctx-solver-simplify 的输出似乎并不等于原始公式(它看起来更像是可满足性等价的)。另外，也可能是我没有正确处理战术。
这就是我想要做的:http://rise4fun.com/Z3Py/g5sX 。因此，我构造了一个公式 Set2(定义 Set2 之前的所有内容都只是定义它所需的设置)，它具有特定的令人满意的赋值。应用 ctx-solver-simplify 后，我得到了一个公式(作为目标)，但此作业无法满足该公式。那我错了什么？
- 我是否错误地假设
ctx-solver-simplify会产生等效公式？ - 我是否以错误的方式处理策略及其输出？
- 还有什么吗？
谢谢。
最佳答案
我一直在研究这个问题，但到目前为止还无法直接重现该错误 与我们当前的分支机构。上下文简化器中的一个错误不久前已修复，它可以 Z3 的在线版本体现了这一点。 我还可以做一些事情来仔细检查我们是否可以重现该错误 我将根据我的发现更新这篇文章。
关于z3 - ctx-solver-simplify(和类似的策略)是否会产生等效的公式，或者只是 SAT 等效的公式，或者我做的事情完全错误？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/13040538/