显示来自 Z3 模型的所有值 (Python)答案

【问题标题】：Display all values from Z3 model (Python)显示来自 Z3 模型的所有值 (Python)
【发布时间】：2015-10-18 11:20:45
【问题描述】：

当我想获取 SMT2 实例中所有变量的值时，我使用命令(set-option :auto-config false)。在 Z3py 中，设置此选项不起作用 - 模型不显示我定义但未在任何约束中使用的变量。如果我询问这些变量的值，我会得到None。我已经尝试了这些选项，但它们都没有产生我想要的结果：

set_option('model_evaluator.completion', True)
set_option('smt.auto-config', False)
set_option('auto-config', False)

我应该怎么做才能获得这些变量的具体值？

【问题讨论】：

标签： z3 smt z3py

【解决方案1】：

auto-config 选项不会告诉 Z3 打印或省略部分模型；它只是启用或禁用求解器的自动配置（基于静态公式功能）。

当一个变量在模型中没有被赋值时，它就是无关紧要的，也就是说，你可以为它补任何值，它仍然是一个正确的模型。根据您使用的求解器/策略，选项 model_evaluator.completion 可能会解决该问题，但最安全的方法是在模型评估时启用模型完成，即使用 eval(..) 函数和 model_completion=True

【讨论】：