從Z3中的const數組中提取值

我的問題是，在Z3 C/C++ API中，如何從Z3生成的模型中獲取（索引，值）對。從Z3中的const數組中提取值

我遇到同樣的問題， 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（）函數。

謝謝！

來源

2016-12-01 Hongce Zhang

忽略斷言在這些事情中很少是一個好的解決方案:-)我沒有時間在例子中拼出來，但是你想要的是'（as const ...）的第一個參數'術語。該術語表示常數數組，即該數組對於所有索引具有相同的值。 'Z3_get_app_arg（ctx，term，0）'應該給你價值。 –

非常感謝！ –

請發表問題的答案並接受它 - 這將標記問題已解決並有可能幫助其他人。 –

感謝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 
    // 
}

希望它可以幫助他人。

來源

2016-12-13 20:51:21

從Z3中的const數組中提取值

回答

相關問題