列挙型の式の量指定子除去戦術を試しています。何らかの方法でソルバーを調整してパフォーマンスを向上させる方法があるかどうかを知りたいです。ソースコードをざっと見た後、量指定子を削除するためのさまざまな戦略 (qe_lite.cpp など) があるように思われるが、それらは qe タクティックのパラメーターとして公開されていないという結論に達しました。私の場合、数式は単純な命題構造を持ち、量化された変数が数式に含まれていないこともありますが、手続きは数千回呼び出すことができます。だから私は推測します、私の質問は次のとおりです：
- Z3 には量指定子の除去 (アプリケーション モード?) のためのある種のキャッシュがあり、類似または同一の数式をより高速に処理できますか?
- Z3 に、有限領域の式で量指定子を削除するためのさまざまなアプローチを使用するように指示できますか?
- Z3 で一般的に使用されている方法を知ることは興味深いでしょう。代入＋簡略化だけなのか、それとももっと凝ったテクニックを使っているのか。
ありがとうございました。