z3 - Z3 で LIA 量指定子の削除をカスタマイズする

Question

F# と Z3 3.2 API を使用して、LIA で量指定子の削除を行っています。

Z3 にQUANT_ARITHは、Cooper の方法または LIA 量指定子の除去のためのオメガ テストの使用を示す構成がありました。ELIM_QUANTIFIERSしかし、そのオプションはZ3 2.6で置き換えられました( Z3 リリース ノートを参照)。

Z3 3.2 が量指定子の削除に使用する方法をどのように認識しているか内部的に尋ねたいのですが? ユーザーは以前のように方法の選択に影響を与えることができますQUANT_ARITHか?

さらに、戦略仕様言語の導入により、Z3 では、これらのメソッドを拡張または組み合わせることで、量指定子の削除をカスタマイズできますか?

Answer 1

数量子除去モジュールが再実装されました。新しい実装は、より高速で正確になるはずです。最新のZ3には、クーパー法やオメガテストが実装されていません。Z3 で使用されている実際の量指定子の削除手順の詳細については、「抽象的な決定手順としての線形量指定子の削除、Nikolaj Bjørner、IJCAR 2010」を参照してください。

戦略仕様言語に関しては、量指定子の除去を実行するための戦術を最終的に公開します。現在、このインフラストラクチャに取り組んでおり、さらに多くのニュースが近日中に公開されます。