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

Question

Per this answer the Z3 set sort is implemented using arrays, which makes sense given the SetAdd and SetDel methods available in the API. It is also claimed here that if the array modification functions are never used, it's wasteful overhead to use arrays instead of uninterpreted functions. Given that, if my only uses of a set are to apply constraints with 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))

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

Answer 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，并使用所有这三个想法来实现它，并对您的问题域进行基准测试以查看最有效的方法；请记住，如果您开始处理不同的问题，答案可能会有所不同。请报告您的发现！

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

What alternatives exist for representing sets in Z3?

z3

z3py