我正在尝试制作 z3（我正在使用 z3py）来为我简化一些公式（这样我就可以或多或少地获得人类可读的输出）。使用ctx-solver-simplify策略对我来说似乎是一个不错的选择，因为在几次传递中它会产生很好的紧凑公式。但是很快我就遇到了一种情况，即 的输出ctx-solver-simplify似乎与原始公式不等价（它看起来更像是可满足性等价的）。另外，我可能没有正确处理战术。
这是我想做的：http ://rise4fun.com/Z3Py/g5sX 。因此，我构造了一个公式Set2（定义之前的所有内容Set2都只是定义它所需的设置），它具有特定的令人满意的分配。申请后ctx-solver-simplify，我得到了一个公式（作为目标），但这个任务并不令人满意。那么我错了什么？
ctx-solver-simplify假设会产生等效的公式，我错了吗？- 我是否以错误的方式处理战术及其输出？
- 还要别的吗？
谢谢。