Wert aus const Array in Z3 extrahieren

Question

Meine Frage ist, in Z3 C/C++ API, wie kann ich das (Index, Wert) Paar von einem Modell von Z3 generiert.

begegnete ich das gleiche Problem wie, Read func interp of a z3 array from the z3 model

Allerdings ist diese Lösung nicht immer für mich arbeiten.

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)); 

Die erste Behauptung fehlschlagen kann, weil die Funktion:

Z3_get_decl_kind(c, some_array_1_eval_func_decl)

kehrt Z3_OP_CONST_ARRAY.

Ich frage mich nur in diesem Fall, wie ich es extrahieren soll.

Das Modell ist:

(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)) 

Und ich benutze es die "rom" zu bewerten. Wenn ich das Ergebnis drucke, das ist

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

Ich kann seine Erklärung erhalten. Das ist

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

Wenn ich die erste Behauptung Fehler ignorieren und weiterhin kann die vierte Behauptung fehlschlagen, ist es tatsächlich Z3_PARAMETER_SORT.

Ich fand, dass Antwort könnte mit einer alten Version der Z3-Bibliothek arbeiten, aber ich muss eine neuere Version verwenden, weil der neuere hat to_smt2() -Funktion.

Danke!

Answer 1

Dank Christophs Hinweis. Ich löse dieses Problem durch den folgenden Code:

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

annehmen Dann

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

Hoffe, dass es für andere hilfreich sein kann.