當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。