Z3 4.0 : get complete model

Question

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

http://pastebin.com/KiwFJTrK

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

MODEL_COMPLETION = true 

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

我需要这个的原因解释了 here in detail .简而言之:我想使用 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 整数问题。 var4的值当问题被视为 0-1 问题时是“不在乎”，但当问题被视为整数问题时不是“不在乎”( var4 必须是 0 或 1) .默认情况下，Z3 不会显示“don't care”变量的值。
MODEL_COMPLETION=true当您请求未包含在模型中的常量的值时，将完成模型。例如，如果我们执行 (eval var4) , Z3 将产生对 var4 的解释.