在 Z3 中表示集合有哪些替代方法？答案

【问题标题】：What alternatives exist for representing sets in Z3?在 Z3 中表示集合有哪些替代方法？
【发布时间】：2021-12-05 17:16:42
【问题描述】：

根据this answer，Z3 集合排序是使用数组实现的，考虑到 API 中可用的 SetAdd 和 SetDel 方法，这很有意义。 here 还声称，如果从不使用数组修改函数，那么使用数组而不是未解释的函数是浪费的开销。鉴于此，如果我对集合的唯一用途是使用 IsMember 应用约束（在单个值上或作为量化的一部分），那么使用从底层元素排序到布尔值的未解释函数映射是一个更好的主意吗？所以：

from z3 import *
s = Solver()
string_set = SetSort(StringSort())
x = String('x')
s.add(IsMember(x, string_set))

变成

from z3 import *
s = Solver()
string_set = Function('string_set', StringSort(), BoolSort())
x = String('x')
s.add(string_set(x))

这种方法有什么缺点吗？开销更少的替代表示？

【问题讨论】：

标签： z3 z3py

【解决方案1】：

这些确实是您唯一的选择，只要您想将自己限制在标准界面即可。过去，我也很幸运能够在求解器之外表示集合（以及一般关系），将处理完全保持在外部。这就是我的意思：

from z3 import *

def FSet_Empty():
    return lambda x: False

def FSet_Insert(val, s):
    return lambda x: If(x == val, True, s(val))

def FSet_Delete(val, s):
    return lambda x: If(x == val, False, s(val))

def FSet_Member(val, s):
    return s(val)

x, y, z = Ints('x y z')

myset = FSet_Insert(x, FSet_Insert(y, FSet_Insert(z, FSet_Empty())))

s = Solver()
s.add(FSet_Member(2, myset))

print(s.check())
print(s.model())

请注意我们如何通过一元关系对集合进行建模，即从值到布尔值的函数。您可以将其推广到任意关系并且这些想法得以延续。这打印：

sat
[x = 2, z = 4, y = 3]

您可以轻松地添加并集（本质上是 Or）、交集（本质上是 And）和补集（本质上是 Not）操作。做基数比较难，特别是在存在补码的情况下，但对于所有其他方法也是如此。

与此类建模问题一样，没有一种方法可以最有效地解决所有问题。他们都会有自己的长处和短处。我建议创建一个 API，并使用所有这三个想法来实现它，并对你的问题域进行基准测试，看看什么效果最好；请记住，如果您开始处理不同的问题，答案可能会有所不同。请报告您的发现！

【讨论】：