z3 - z3 を使用した式で「not」を削除する

Question

スクリプトhttp://rise4fun.com/Z3/XwGtを使用して式の「not」を削除しようとしましたが、うまくいきません。結果にはまだありません。誰か助けてくれますか?

Answer 1

あなたの例の出力目標は、簡略化された式です。どのゴールにも冗長なアサーションはありません。t1 <= t2Z3 の簡略化された形式では、やなどの非厳密な不等式が常に使用されt1 >= t2ます。のような厳密な不等式t1 < 0は、否定を使用してエンコードされます。つまり、t1 < 0としてエンコードされnot t1 >= 0ます。アイデアは、大きな式をエンコードするために使用されるアトムの数を減らすことです。

出力から sを削除する必要がある理由を理解しておくと役立ちnotます。そのための便利なアプリケーションがあれば、変換を実行する新しい戦術を (次のリリースで) 含めます。