2

Z3 でブール式の自動簡略化を無効にすることはできますか?

たとえば、式 2 > 1 は、2 > 1 のままにしたいのですが、自動的に True になります。

>>> t = 2 > 1
>>> t
True

Z3Py で help_simplify() を呼び出して、いくつかのオプションを見つけました。しかし、それらのどれも私の問題に関連していないようです。

別のチュートリアル ( http://citeseerx.ist.psu.edu/viewdoc/download?rep=rep1&type=pdf&doi=10.1.1.225.8231 ) では、オプション "CONTEXT SIMPLIFIER" が言及されています。 -数式を真または偽にします。" ただし、Z3Py ではこのオプションを見つけることができませんでした。

背景: And(2>1, 1!=2) のような式を使用できるようにしたいと考えています。ここで、2>1 と 1!=2 は以前に自動的に生成され、変数 (定数) を含まない場合があります。Z3Py はこれを And(True, False) に簡略化しますが、これは受け入れられません。これは、「引数の少なくとも 1 つが Z3 式またはプローブでなければならない」ためです。したがって、簡素化は抑えたいと思います。または、And(True, False) を受け入れられる式にする方法はありますか?

前もって感謝します！

4

1 に答える 1

1

実際、これは 2>1 のような単純な式が Python によって True/False に単純化されているためです。ほとんどの演算子 (Implies、Xor など) はこれで問題ありませんでしたが、And および Or 演算子はそうではありませんでした。これらは式だけでなくプローブにも使用できるため、実装が異なります。他のブール演算子のように動作するように、もう少しコードを追加しました (修正については、こちらを参照してください)。これにより、プローブに新たな問題が発生することなく、この問題が解決されることを願っています。他の人がこれをもう少しテストできるとありがたいです。

于 2014-05-29T16:36:03.470 に答える