Z3 4.3 : get complete model

Question

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

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

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

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

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

Answer 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。