python - 如何在 Z3py 中创建一个约束来检查一个列表是否是另一个列表的排列？

Question

我是 Z3py 的初学者，现在我已经为此苦苦挣扎了将近一个星期......我没有找到足够的信息来帮助我在教程中找到一个很好的例子(函数存在)可以帮我。

Answer 1

免责声明:如果您的问题只是您正在努力使用 Z3py 编码问题，那么我的建议不会帮助您，因为它们不是 关于 Z3py。但是，我认为您的问题实际上更为根本。

答案:公理化 Z3/SMTLIB 中的列表一点也不简单，特别是因为您的公理化需要针对您的(forall-quantified)公理的良好触发策略(模式)，这样您的公理化就不会产生匹配循环。

我建议查看 Boogie prelude of Dafny看看序列的公理化看起来如何。 Dafny是一个自动化的软件验证器和Boogie是一种中间验证语言。 Boogie 的语法很容易理解(对于熟悉 SMTLIB 语法的人来说)，您应该能够使用表达序列排列的公理(或多个公理)扩展现有的序列公理化。

其他灵感来源可能是 this或 this论文，这两篇论文都讨论了公理触发器和匹配循环。