配列式の評価

Question

私はQF_AUFBVの問題を解決するためにZ3-3.2のc-api（on 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_declsを繰り返し処理し、get_symbol_stringを比較することによってその配列の正しいものを見つけることによって、望ましい情報を得ることができました。情報はZ3のどこかで利用できるように見えますが、それはすてきな解決策とはみなされません。

ありがとうございました。

敬具は、 フロリアン

Answer 1

評価者は、もう少し強力な配列の値にアクセスするためのAPIを超えています。 関数is_array_valueは、表現された配列の形式が の場合にのみ成功します（store（store（store（...））..）..）））） または配列as-array [f ]ここで、fは有限単項関数である。

is_array_valueとget_array_value機能は、既存のAPI を使用して実装することができ、利便性 のために露出されている（あなたが説明するように、我々は、文字列の比較を使用しないようにし、代わりに列挙種類です 関数宣言で比較を使用することができます除きます）。 あなたのケースでもっとサポートできるように聞こえますが、モデル値 がどのように見えるのか不思議です。合格しない例についての追加情報を提供できますか？ （印刷しますか？）

ありがとうございました