0

QF_AUFBV の問題を解決するために、Z3-3.2 の c-api (Linux 上) を使用しています。

式が満足できるものであれば、モデルから自由配列変数の値を読み出したいと思います。

次のコードの行に沿って何かを試しましたが、これを行う方法の一般的な考え方が正しいかどうかを知りたいです:

void evaluate(Z3_context context, Z3_model model, Z3_ast array)
{
  Z3_ast value;
  Z3_bool success = Z3_eval(context, model, array, &value);
  if (success) {
    unsigned num_entries;
    if (Z3_is_array_value(context, model, value, &num_entries)) {
      Z3_ast indices[num_entries];
      Z3_ast values[num_entries];
      Z3_ast def;
      Z3_get_array_value(context, model, array, num_entries, indices, values, &def);

      // do something with indices, values, and def
    }
  }
}

入力 Z3_ast 配列は、間違いなく自由な配列式です。Z3_eval は true を返すので、式の評価は成功したように見えますが、Z3_is_array_value は false を返します。配列式で成功した Z3_eval の結果が配列値になると予想していたのに、そうでないのはなぜですか?

ところで、すべての model_func_decl を反復処理し、get_symbol_string を比較してその配列に適したものを見つけようとすることで、目的の情報を取得することができました。そのため、情報は Z3 のどこかで入手できるようですが、それは優れた解決策とは言えません。

これについて助けてくれてありがとう。

よろしく、フロリアン

4

1 に答える 1

0

エバリュエーターは、配列値にアクセスするためのAPIよりも少し強力です。関数is_array_valueは、表現された配列が（store（store（store（store（...（const v）...）..）..））またはas-array [f]の形式である場合にのみ成功します。ここで、 fは有限の単項関数です。

is_array_value関数とget_array_value関数は、既存のAPIを使用して実装でき、便宜上公開されています（説明したとおり、文字列比較の使用を避け、代わりに列挙型の関数宣言で比較を使用できます）。ですから、あなたのケースではもっとサポートできるように思えますが、モデルの値がどのように見えるのか興味があります。合格しなかった例に関する追加情報を提供できますか？（印刷しますか？）

ありがとう

于 2012-02-09T22:17:59.817 に答える