Z3：编码范围为子集的函数答案

【问题标题】：Z3 : Encoding functions whose ranges are set of subsetsZ3：编码范围为子集的函数
【发布时间】：2015-08-28 16:19:48
【问题描述】：

我想问我如何编码范围是一组子集的函数。

例如，我有一个集合 Proc = {1, 2, 3} 和一个集合 Number = {4, 5, 6}。现在我想将 Proc 中的函数“fcn”声明为 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”的范围。

非常感谢。

【问题讨论】：

标签： z3

【解决方案1】：

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

【讨论】：

非常感谢，尼古拉。