当model_completion设置为false时，Z3会返回什么？

Question

当查询模型时，model_completion设置为falseZ3_model_eval：Z3返回的含义是什么，表示解释是“不关心”？

如果有人想表明：我想这可能不是功能Z3_model_eval的返回值，因为z3++.h文件（C++ API）包含线路：

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

一般来说：如何Z3表示某个常数在模型中是“不关心”的吗？

Answer 1

对于真正的不在乎，模型不会分配任何值。因此，调用eval或Z3_model_eval并将model_completion设置为false将保持原始常量不变，并仅替换为其指定模型值的那些（并且这可能会简化表达式）。下面是一个例子：

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; 

注意，输出打印x，即第一行中，原始表达式是不动，而该呼叫与model_completion设置为true将打印0 EVAL。