Extract value from const array in Z3

Question

My question is, in Z3 C/C++ API, how can I get the (index,value) pair from a model generated by Z3.

I encountered the same problem as, Read func interp of a z3 array from the z3 model

However, that solution does not always work for me.

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

The first assertion can fail, because the function:

Z3_get_decl_kind(c, some_array_1_eval_func_decl)

returns Z3_OP_CONST_ARRAY.

I just wonder in this case how should I extract it.

The model is:

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

And I use it to evaluate the "rom". If I print out the result, that is

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

I can get its declaration. That is

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

If I ignore the first assertion error and continue, the fourth assertion can fail, it is actually Z3_PARAMETER_SORT.

I found that answer could work with an old version of Z3 library, but I need to use a newer version because the newer one has to_smt2() function.

Thanks!

Answer 1

Thanks to Christoph's hint. I solve this problem by the following code:

suppose

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

Then,

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

Hope it can be helpful to others.