Z3：范围是子集集的编码函数

Question

我想问一下如何对范围为子集集的函数进行编码。

例如，我有一组 Proc = {1, 2, 3} 和一组 Number = {4, 5, 6}。现在我想声明一个函数 "fcn" 从 Proc 到 Number 的一组子集。我打算通过声明为 Number 的每个子集使用 8 个变量：

    (declare-fun var1 (Int) Bool) 
    (assert (= (var1 4) true)) 
    (assert (= (var1 5) true)) 
    (assert (= (var1 6) true))

    ...

    (declare-fun var8 (Int) Bool) 
    (assert (= (var8 4) false)) 
    (assert (= (var8 5) false)) 
    (assert (= (var8 6) false))

我猜，"fcn" 应该是 (declare-fun fcn (Int) ...)。不幸的是，我不知道如何声明 "fcn".

的范围

非常感谢。

Answer 1

您可以使用数组来编码集合（和集合的集合）。一组 A 被编码为 (Array A Bool)。那么A的一组集合就是(Array (Array A Bool) Bool)。您可以使用 "store" 从此类集合中添加和删除元素。您可以使用 "map" 函数获取并集和交集。也可以看看，广义、高效的阵列决策程序。莱昂纳多·德莫拉，尼古拉·比约纳。 FMCAD 2009。MSR-TR-121 中的扩展版本。 http://research.microsoft.com/apps/pubs/?id=102329

Z3：范围是子集集的编码函数

Z3 : Encoding functions whose ranges are set of subsets

z3