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

【问题标题】：What will Z3 return when model_completion is set to false?当 model_completion 设置为 false 时，Z3 会返回什么？
【发布时间】：2014-06-22 01:48:59
【问题描述】：

在查询模型时，Z3_model_eval 中的 model_completion 设置为 false：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 如何表示某个常数在模型中是“无关紧要”的？

【问题讨论】：

Size Z3_model_eval 不是标准 C++ 函数，请编辑您的帖子以提供声明和定义。

标签： c++ c model z3

【解决方案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 的eval 调用将打印0。

【讨论】：