What will Z3 return when model_completion is set to false?

Question

When querying a model, with model_completion set to false in Z3_model_eval: What will Z3 return to signify that an interpretation is a "don't care"?

In case someone wants to suggest that: I guess it's probably not the return value of the function Z3_model_eval, since the z3++.h file (the C++ API) contains the lines:

Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
check_error();
if (status == Z3_FALSE)
    throw exception("failed to evaluate expression");

In general: How does Z3 signify that a certain constant is a "don't care" in a model?

Answer 1

For true don't-cares, the model will not assign any value. Consequently, calls to eval or Z3_model_eval with model_completion set to false will keep the original constants untouched and only replace those for which a model value is assigned (and it will potentially simplify the expression). Here's an example:

context c;
expr e = c.int_const("x");

solver s(c);
s.add(e == e);
model m = s.get_model();

std::cout << m.eval(e, false) << std::endl;
std::cout << m.eval(e, true) << std::endl;

Note that the first line of output prints x, i.e., the original expression is untouched, while the call to eval with model_completion set to true will print 0.