5

非線形演算を扱う Z3 の一部であると私が信じている部分で、パフォーマンスの問題が発生しています。これは、Z3 (バージョン 4.1) で検証すると、完了までに長い時間 (3 分程度) かかる簡単で具体的なブギーの例です。

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 がいつ検索を停止すべきかについてのヒューリスティックを改善することができるのかどうか疑問に思っています。

興味深いことの 1 つは、次を使用して関数をインライン化することです。

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

検証を非常に迅速に終了させます。

背景: これは、ベリファイア Chalice で見られる問題の最小限のテスト ケースです。そこでは、Boogie プログラムがはるかに長くなり、同様の種類の複数の仮定が含まれる可能性があります。多くの場合、検証はまったく終了していないように見えます。

何か案は？

4

1 に答える 1

3

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

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

于 2012-09-21T15:33:24.507 に答える