私はz3（私はz3pyを使用しています）を作成して、いくつかの数式を単純化しようとしています（これにより、多かれ少なかれ人間が読める形式の出力を得ることができます）。戦術を使用ctx-solver-simplifyすることは、2、3回のパスで、優れたコンパクトな数式を生成するため、私にとっては良い選択のように思われました。しかし、すぐに、の出力がctx-solver-simplify元の式と同等ではないように見える状況に遭遇しました（充足可能性と同等かそこらのように見えます）。また、戦術を正しく扱っていない場合もあります。
これが私がやろうとしていたことです：http：//rise4fun.com/Z3Py/g5sX。そこで、私は、特定の満足のいく割り当てを持つ式Set2（の定義の前のすべては、それを定義するために必要なセットアップにすぎません）を作成します。Set2を適用した後ctx-solver-simplify、この割り当てが満たされない単一の式を（目標として）取得します。それで、私は何が間違っているのですか？
ctx-solver-simplifyそれが同等の式を生成すると仮定するのは間違っていますか？- 戦術とその出力を間違った方法で処理していますか？
- 他に何か？
ありがとう。