Z3 4.3 : get complete model

Question

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

我正在建模a simple state machine for an elevator 。有两层楼和两个按钮向上和向下。我将转换建模为谓词 Action x Elevator x Elevator (Elevator = State)，使得 T(a,s,s') 保持 iff 的操作 < em>a 可能会导致从 s 到 s' 的转换，其中一个操作是插入 向上 或 s'>向下按钮。问题的可满足性并不取决于按下按钮的人，但我希望 Z3 为函数 subject : Action -> Person 分配一些解释。

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

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

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

Answer 1

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

该修复将在下一个正式版本中提供。 如果需要，您可以下载unstable(正在进行中)分支并编译它。要下载，您只需点击上面链接中的下载按钮即可。

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

(set-option :model_evaluator.completion true)

而不是

(set-option :model_completion true)

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

(eval <term> :completion true)

而不是

(eval <term> :model_completion true)

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