量指定子の使用はZ3のパフォーマンスに影響しますか？

Question

this questionへの回答では、機能を定義するために量子を使用することを提案しました。私は関数を1回だけ適用する必要があると仮定し、量限定子を使用することはZ3の性能に影響するか？

パラメータを持たず、量指定子を使用しない関数を宣言した場合（私は関数を1回しか使用しないため）と比較するとどうでしょうか？

Answer 1

オプションsmt.macro_finder = trueを使用して、数量化された等式をマクロに変換できます。デフォルトではオフになっていますので、一度しか適用しない関数のマクロを定義する方がよいでしょう。また、Z3は一般的な量子ベースのソルバーを使用して終了することを意味します。場合によっては、 "define-fun"コマンドを使用してマクロで定義された関数は、純粋にビットベクトルまたは純粋に線形算術である式の場合に便利です。このような場合、Z3はより効率的な設定を使用します。たとえば、Z3では、「関連性」の伝播を使用して余分な量子化のインスタンス化を回避します。関連性の伝播には、数量化された公式には許容される独自のオーバーヘッドがありますが、数量化されていない公式には適していません。