Z3のconst配列から値を抽出する

Question

私の質問は、Z3 C/C++ APIでは、Z3によって生成されたモデルから（インデックス、値）のペアを取得する方法です。

私はしかし、そのソリューションは、常に私のために動作しません Read func interp of a z3 array from the z3 model

、同じ問題が発生しました。

assert(Z3_get_decl_kind(c, some_array_1_eval_func_decl) == Z3_OP_AS_ARRAY); 
assert(Z3_is_app(c, some_array_1_eval)); 
assert(Z3_get_decl_num_parameters(c, some_array_1_eval_func_decl) == 1); 
assert(Z3_get_decl_parameter_kind(c, some_array_1_eval_func_decl, 0) == 
     Z3_PARAMETER_FUNC_DECL); 
func_decl model_fd = func_decl(c, 
        Z3_get_decl_func_decl_parameter(c, some_array_1_eval_func_decl, 0)); 

最初のアサーションは機能するので、失敗する可能性がある

Z3_get_decl_kind(c, some_array_1_eval_func_decl)

Z3_OP_CONST_ARRAYを返し

。

この場合、どのように抽出すればよいのでしょうか。

(define-fun |choice.pc.1:1|() Bool 
    false) 
(define-fun pc() (_ BitVec 4) 
    #x0) 
(define-fun pc_miter_output() Bool 
    true) 
(define-fun rom() (Array (_ BitVec 4) (_ BitVec 4)) 
    (_ as-array k!0)) 
(define-fun |choice.pc.1:2|() Bool 
    true) 
(define-fun k!0 ((x!0 (_ BitVec 4))) (_ BitVec 4) 
    (ite (= x!0 #x0) #x0 
    #x0)) 

そして、私はそれが "ROM" を評価するために使用します。

モデルです。結果を印刷すると、

((as const (Array (_ BitVec 4) (_ BitVec 4))) #x0) 

私はその宣言を得ることができます。それは私が最初にアサーションエラーを無視して続行する場合は、第四アサーションが失敗する可能性が

(declare-fun const ((_ BitVec 4)) (Array (_ BitVec 4) (_ BitVec 4))) 

あり、それは実際にZ3_PARAMETER_SORTです。

私は答えが古いバージョンのZ3ライブラリで動作することがわかりましたが、新しいバージョンにはto_smt2（）関数があるため、新しいバージョンを使用する必要があります。

ありがとうございます！

Answer 1

Christophのヒントに感謝します。私は、次のコードでこの問題を解決：次に

mval = model.eval(...); 
mfd = mval.decl(); 

は考え、

while(Z3_get_decl_kind(c.ctx(), mfd) == Z3_OP_STORE) { 
    expr addr = mval.arg(1); 
    expr data = mval.arg(2); 
    // put them into the stack, say __stack__ for later use 
    // I omit the code for using them 
    mval = mval.arg(0); 
    mfd = mval.decl(); 
    // recursively handle the OP_STORE case, because the first 
    // argument can still be an Z3_OP_STORE 
} 
// now that we peel the Z3_OP_STORE 
if(Z3_get_decl_kind(c.ctx(), mfd) == Z3_OP_CONST_ARRAY) { 
    expr arg0 = mval.arg(0); 
    // we can just use it directly since it is a constant 
    std::string sdef(Z3_get_numeral_string(context, arg0)); 
    // I omit the code for using that value 
} 
else if(Z3_get_decl_kind(c.ctx(), mfd) == Z3_OP_AS_ARRAY) { 
    // HERE is the original code for handling original case. 
    // in the question from the link: 
    // http://stackoverflow.com/questions/22885457/read-func-interp-of-a-z3-array-from-the-z3-model/22918197#22918197?newreg=1439fbc25b8d471981bc56ebab6a8bec 
    // 
} 

は、それが他の人に役立つことができます願っています。