Z3非線形算術によるパフォーマンス

Question

私は、非線形算術を扱うZ3の一部であると信じているところで、パフォーマンスの問題に遭遇しています。 Z3（バージョン4.1）で検証したときに完了するまでに長い時間（3分程度）がかかる簡単な具体的なBoogieの例を次に示します。

const D: int; 
function f(n: int) returns (int) { n * D } 

procedure test() returns() 
{ 
    var a, b, c: int; 
    var M: [int]int; 
    var t: int; 

    assume 0 < a && 1000 * a < f(1); 
    assume 0 < c && 1000 * c < f(1); 
    assume f(100) * b == a * c; 

    assert M[t] > 0; 
} 

は整数変数ならびに（未知の）整数値の乗算に範囲仮定、問題は機能の相互作用によって引き起こされると思われます。最後の主張は証明できないはずです。 Z3はすぐに失敗するのではなく、メモリ消費量が約300 MBに急激に増加するため、何らかの理由で多くの用語をインスタンス化する方法を持っていると思われます。

これはバグかどうか、またはZ3が現在問題を解決しようとしている特定の方向に検索を停止する必要がある場合にヒューリスティックスを改善できるかどうか疑問です。

一つ興味深いのは、

function {:inline} f(n: int) returns (int) { n * D } 

を使用して機能をインライン化すると、検証が非常に迅速に終了しますということです。

背景：検証者のChaliceに見られる問題の最小限のテストケースです。そこでは、Boogieプログラムは、おそらく同様の種類の複数の仮定を持って、ずっと長くなります。多くの場合、検証はまったく終了していないようです。

アイデア？

Answer 1

はい、非終端は非線形整数計算によるものです。 Z3は新しい非線形ソルバを備えていますが、これは「非線形実数」のためのもので、算術演算のみを使用する量限定子の問題には使用できません（例のような未解釈関数はありません）。 したがって、あなたの例では古い算術ソルバーが使用されます。このソルバーは、整数演算のサポートが非常に限られています。あなたの分析は正しいです。 Z3は、非線形整数制約のブロックの解を見つけるのに問題があります。 f(100) * b == a * cをf(100) * b <= a * cに置き換えると、Z3はすぐに「不明な」回答を返すことに注意してください。

Z3の非線形算術推論の数を制限することで、非終了を避けることができます。 NL_ARITH_ROUNDS=100オプションは、Z3クエリごとに最大100回、非線形モジュールを使用します。これは理想的な解決策ではありませんが、少なくとも、非終了を回避します。