Как создать ограничение в Z3py, чтобы проверить, является ли список перестановкой другого?

Отказ от ответственности: если ваша проблема заключается исключительно в том, что вы пытаетесь закодировать проблему с помощью Z3py, то мои предложения вам не помогут, поскольку они не по поводу Z3py. Однако я предполагаю, что ваша проблема на самом деле более фундаментальна.

Ответ: Аксиоматизация списков в Z3/SMTLIB совсем не проста, в частности потому, что для вашей аксиоматизации требуется хорошая стратегия срабатывания (шаблоны) для ваших (количественных) аксиом, так что ваши аксиоматизация не приводит к совпадению петель.

Я предлагаю посмотреть прелюдию Дафни в стиле буги, чтобы увидеть, как можно посмотреть аксиоматизацию последовательностей. Dafny — это автоматизированный верификатор программного обеспечения и Boogie — это промежуточный язык проверки. Синтаксис Boogie прост для понимания (для тех, кто знаком с синтаксисом SMTLIB), и вы сможете расширить существующую аксиоматизацию последовательности с помощью аксиомы (или нескольких аксиом), выражающих перестановку последовательности.

Другими источниками вдохновения могут быть это или < href="http://research.microsoft.com/en-us/um/people/leino/papers/rmkrml183.pdf" rel="nofollow">эта статья, в которой обсуждаются триггеры аксиом и соответствующие петли.

W̶o̶w̶,̶ ̶w̶h̶a̶t̶ ̶t̶h̶e̶ ̶h̶e̶c̶k̶.̶.̶.̶ ̶T̶h̶a̶t̶ ̶l̶i̶t̶e̶r̶a̶t̶u̶r̶e̶ ̶l̶i̶s̶t̶ ̶i̶s̶ ̶i̶n̶t̶i̶m̶i̶d̶a̶t̶i̶n̶g̶.̶ Forgive me my arrogance; Вопрос требует чисто символического сравнения? Если нет, этот (гораздо более простой) ответ может предложить что-то полезное.

Если все, что вам нужно, это просто найти определенную перестановку известного списка уникальных значений, вы, вероятно, можете обойтись без аксиоматизации чего-либо.

Просто сгенерируйте O(n²) попарных равенств, а затем добавьте их в группы как n ограничения AtLeast(…, 1) формы. Пример кода объяснит лучше:

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". См. ответ Мальте для этого случая.