Read Func Interp of a Z3 Array from the Z3 Model

Read func interp of a z3 array from the z3 model

The representation for array models is indeed a bit confusing. The meaning of

(define-fun some_array_1 () (Array Int Int)   
  (_ as-array k!0)) 

is that the model for array some_array_1 is the function k!0 which is to be interpreted as an array (signified by the call to as-array. The latter is a parametric function, which has no arguments, therefore, to get at the actual definition of the model function for some_array_1, we have to look up which function as-array calls. In the given example, we can do that as follows, first making sure that we actually have an array model in the expected format by checking a few of assertions:

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 function declaration model_fd then holds the actual function assigned by the model (k!0) and we can get the function interpretation via

  func_interp fun_interp = m.get_func_interp(model_fd);

Retrieving array from model in Z3Py

You can ask the model to evaluate (eval(...)) the array at a particular point by constructing a call to the associated array model function. Here's an example:

b = Array('b', IntSort(), BitVecSort(8))
s = Solver()
s.add(b[0] == 21)
s.add(b[1] == 47)
s.check()

m = s.model()
print(m[b])

print(m.eval(b[0]))
print(m.eval(b[1]))

which produces

[1 -> 47, 0 -> 21, else -> 47]
21
47

Z3: Extract array interpretation

Yes, this is possible. A very similar question has been asked recently and the answer with examples can be found here: Read func interp of a z3 array from the z3 model

Extract value from const array in Z3

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.

Understanding the index of all constants of a model

Thanks Tushar for answering the post. You are right that the additional variables come from the existential quantifier. Z3 will skolemize these variables and as it currently stands, the model returned by Z3 includes constants from skolemized existential quantifiers.
This is evidently confusing and we may in the future filter
such variables (and functions) away from the model construction. On the other hand, the naming conventions used for the existential variables retain the names from the quantifiers so that it may be possible, at least manually, to track back the origin of those extra variables.

If I mark it after (get-model)?

As Patrick commented, it's really hard to decipher what you're asking. Please provide some code snippets to show what you get and what you hope to achieve.

Having said that, I'll take a wild guess that you are in a situation where the solver is unsat, i.e., (check-sat) returns an unsat response. Yet, your script has (get-model) in the next line, which of course errors out since there's no model. And you'd like a way to avoid the error message.

This is a known limitation of SMTLib command language: You cannot programmatically inspect the output of commands, unfortunately. The usual way to solve this sort of problem is to have a "live" connection to the solver (typically in the form of a text pipe), and read a line after issuing (check-sat), and programmatically continue depending on the response. This is how most systems built on top of SMT-solvers work.

Alternatively, you can use higher-level APIs in other languages (C/C++/Java/Python/Haskell..) and program z3 that way; and use the facilities of the host language to direct that interaction. This requires you to learn another interface on top of SMTLib, but for serious uses of this technology, you probably don't want to limit yourself to a pure SMTLib interface anyhow.

Also see this answer for a related discussion: Executing get-model or unsat-core depending on solver's decision

Hope this addresses your issue, though it's hard from your question whether this is what you were getting at.

Problem with function from_file() at z3py

Separately reading the files and loading to solver is your best bet, as you found out.

Unless efficiency is of paramount importance, I would not worry about trying to optimize this any further. For any reasonable problem, your solver time will dominate any time spent in loading the assertions from a few (or a few thousand!) files. Do you have a use case that really requires this part to be significantly faster?

---

Related Topics