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

Question

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

Answer 1

免责声明：如果您的问题只是您正在努力使用 Z3py 编码问题，那么我的建议将无济于事你因为他们不关于 Z3py。但是，我认为您的问题实际上更为根本。

答案：公理化 Z3/SMTLIB 中的列表一点也不简单，特别是因为您的公理化需要一个良好的触发策略（模式）来满足您的需求（forall-quantified）公理，这样你的公理化就不会产生匹配循环。

我建议看看Boogie prelude of Dafny to see how an axiomatisation of sequences can look. Dafny is an automated software verifier and Boogie是一种中间验证语言。 Boogie 的语法很容易理解（对于熟悉 SMTLIB 语法的人来说），您应该能够使用表达序列置换的公理（或多个公理）扩展现有的序列公理化。

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

Answer 2

w̶o̶w̶，̶̶这个问题是否要求纯粹的象征性比较？如果没有，这个（更基本的）答案可能会提供一些有用的东西。

如果您只想找到已知唯一值列表的特定排列，您可能可以在不公理化任何东西的情况下完成。

只需生成 O(n²) 对等式，然后将它们分组添加为 AtLeast(…, 1) 形式的 n 约束。代码示例会更好地解释：

from itertools import combinations
import z3

solver = z3.Solver()

source_list = ['tau', 'eta', 'mu']
permuted = z3.Strings(['X', 'Y', 'Z'])

for var1, var2 in combinations(permuted, 2):
    solver.add(var1 != var2)

#-- here's where we do O(n²) pairwise EQs
for var_ref in permuted:
    possible_assigns = [(var_ref == z3.StringVal(s)) for s in source_list]
    solver.add(z3.AtLeast(*possible_assigns, 1))

#-- TODO: add here the rest of constraints that matter to you

#-- start search
while solver.check() == z3.sat:
    model = solver.model()
    print(model)
    this_solution = z3.And(*[
        var_ref == z3.StringVal(model[var_ref].as_string())
        for var_ref in permuted
        ])
    solver.append(z3.Not(this_solution))

print("No more solutions.")

#-- output:
# [Z = tau, X = mu, Y = eta]
# [Z = tau, X = eta, Y = mu]
# [Z = mu, X = eta, Y = tau]
# [Z = eta, X = mu, Y = tau]
# [Z = mu, X = tau, Y = eta]
# [Z = eta, X = tau, Y = mu]
# No more solutions.

如果 permuted 列表允许有欺骗，这将需要一些调整。

如果两个列表都存在，这将不起作用 "in-z3"。 请参阅 Malte 对这种情况的回答。

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

How do I create a constraint in Z3py to check if a list if a permutation of another?

python

z3

z3py