Z3 に SMTLIB 2 インターフェイスを使用して、UFLIA 理論で量指定子の削除を依頼しています。そこで、21 個の存在量化された変数を含む式をアサートします。そのうち 7 個は整数で、14 個はブール値です。次に実行すると、Z3 は、とto(apply qe)という名前の 9 つの存在量化変数をまだ含むゴールを返します。それは、戦術が一度にすべての量指定子を排除しないということですか?(x!1 Int)(x!14 Int)(x!14!1 Int)(x!14!7 Int)qe
2 回実行(assert qe)すると、名前が変更された数量化された変数を除いて、目標は同じままです。を試し(repeat qe)ましたが、 が返されますunsupported。また、パラメーターを true に設定して:eliminate-variables-as-blockも何も変わりません。
ただし、目標から量化された式を取得し、それを独自にアサートしてassert qe再度行うと、Z3 は希望どおりに残りの量指定子を削除します。
数式については、以下のリンクを参照してください。Z3 ですべての量指定子を一度に削除するために必要な魔法はありますか?