z3 - Z3 4.0：获取完整模型

Question

我需要一个完整的 SMTLIB2 公式模型：

http://pastebin.com/KiwFJTrK

Z3（版本 3.2 和 4.0）返回所有变量的值，但不返回var4的值。我尝试了一些配置设置，例如

MODEL_COMPLETION = true 

但它似乎没有用。有人有建议吗？相比之下，CVC3 返回一个模型（包括 var4），因此这不是 SMTLIB 或我的示例的问题。

我需要这个的原因在这里详细解释。简而言之：我想使用 C API 进行增量求解。出于这个原因，我必须多次使用函数Z3_parse_smtlib2_string 。此函数需要先前声明的函数和常量作为参数。我无法通过Z3_get_smtlib_decl获取此信息，因为此类函数仅在调用z3_parse_smtlib_string时才起作用，而不是Z3_parse_smtlib2_string。

Answer 1

您可以通过在脚本开头添加以下选项来避免此问题。

(set-option :auto-config false)

我会在下一个版本中修复它。这是对正在发生的事情的简短解释。Z3 有一个 0-1 整数问题的求解器。预处理后，您的脚本被 Z3 标记为 0-1 整数问题。当问题被视为 0-1 问题时，的值var4是“无关紧要”，但当问题被视为整数问题时，它不是“无关紧要”（var4必须为 0 或 1） . 默认情况下，Z3 不会显示“无关”变量的值。

当您请求模型中未包含的常量的值时，这MODEL_COMPLETION=true将完成模型。例如，如果我们执行(eval var4)，Z3 将产生对 的解释var4。