Z3 4.0：得到完整的模型(Z3 4.0: get complete model)

我需要一个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的问题。 的值var4是“不关心”的时候，问题被看作是一个0-1的问题，但它不是一个“不关心”的时候，问题被看作是一个整数问题（ var4必须为0或1）。 默认情况下，Z3将不显示“不关心”变量的值。

该MODEL_COMPLETION=true为你要求值不包含在模型常数将完成模型。 例如，如果我们执行(eval var4) ，Z3将产生一个interepretation var4 。

文章来源: Z3 4.0: get complete model