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

Question

我是Z3py的初学者，我一直在为此奋斗了近一个星期......我没有找到足够的信息来帮助我在那里没有一个很好的例子（函数Exists），可以帮我。

Answer 1

免责声明：如果你的问题是仅你是用编码用Z3py的问题所困扰，那么我的建议不会帮助你，因为他们不约 Z3py。但是，我认为你的问题实际上是更基本的。

答： Axiomatising名单在Z3/SMTLIB是不是在所有直接的，特别是因为你的axiomatisation需要你（FORALL量化的）公理良好的触发战略（模式），让你的axiomatisation不会产生匹配循环。我建议看看Boogie prelude of Dafny看看如何看看序列的公理化。 Dafny是一款自动化软件验证程序，Boogie是一种中级验证语言。 Boogie的语法很容易理解（对于熟悉SMTLIB语法的人），并且您应该能够使用表达序列排列的公理（或多个公理）扩展现有的序列公理化。

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