Z3 4.3：获取完整模型答案

【问题标题】：Z3 4.3: get complete modelZ3 4.3：获取完整模型
【发布时间】：2013-01-25 14:55:16
【问题描述】：

这个问题与this one 几乎相同，但该解决方案对我不起作用。抱歉，我想对该答案发表评论，而不是提出新问题，但我没有足够的声誉......

我正在建模a simple state machine for an elevator。有两层楼和两个按钮Up和Down。我已经将转换建模为谓词 Action x Elevator x Elevator（Elevator = State），这样 T(a,s,s') 成立，如果动作 a 可能会导致从 s 到 s' 的转换，其中一个动作正在推动 Up 或向下按钮。问题的可满足性并不取决于按下按钮的人，但我希望 Z3 对函数 subject : Action -> Person 进行一些解释。

我们的目标是找到状态机的k-trace，这可能有助于理解电梯的行为。

我尝试了不同的选项组合，包括auto-config=false 和model-completion=true，但没有成功。我也尝试强制完成模型，询问 (subject Action0) 的值，但 Z3 仍然没有为 subject 分配解释。

我的 Z3 版本是 4.3.1，在 Linux amd64 上运行。

【问题讨论】：

标签： z3

【解决方案1】：

参数:model-completion的问题已修复。该修复程序已在 http://z3.codeplex.com/SourceControl/changeset/a895506dac75 上提供。

该修复程序将在下一个正式版本中提供。如果你愿意，你可以下载unstable (work-in-progress) 分支，并编译它。要下载，您只需点击上方链接中的Download 按钮即可。

顺便说一句，新的 Z3 有一个新的参数设置框架，允许我们设置内部模块参数。在下一个版本中（以及在unstable 分支中）。我们必须使用

(set-option :model_evaluator.completion true)

而不是

(set-option :model_completion true)

因为我们正在设置模块model_evaluator的参数。此外，我们必须使用

(eval <term> :completion true)

而不是

(eval <term> :model_completion true)

因为我们正在设置模型评估器的参数completion。

【讨论】：

【解决方案2】：

很好的例子。抽象排序 Person 没有出现在断言中，并且返回 Person 的函数也没有在断言。

您可以通过将参数直接传递给函数来强制eval完成模型：

http://rise4fun.com/Z3/Pslt4

换句话说，使用

   (eval <term> :model-completion true)

而不是

   (eval <term>)

另一种方法是确保您要评估的术语包含在原始模型中：http://rise4fun.com/Z3/Yukv

【讨论】：