表示Z3中的集合有哪些替代方案？ [英] What alternatives exist for representing sets in Z3?

问题描述

PERthis answerZ3集合排序是使用数组实现的，考虑到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))

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

推荐答案

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

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中的集合有哪些替代方案？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！