为什么CVC4产品运营者不应用于sets？

Question

我正在修改CVC4对集合和关系的支持，并希望能够使用product运算符来构建两个集合的笛卡尔乘积。然而，这个运算符只适用于关系。

这是一个输入到CVC4的示例：

(set-logic ALL_SUPPORTED)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun es1 () (Set S1))
(declare-fun es2 () (Set S2))
(declare-fun es1s2 () (Set (Tuple S1 S2)))
(assert (= es1s2 (product es1 es2)))

这将导致以下错误消息：

(error " Relational operator operates on non-relations (sets of tuples)")

然后，我发现CVC4期望product操作符应用于元组集。成功地处理了下列事项：

(set-logic ALL_SUPPORTED)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun e1 () (Set (Tuple S1)))
(declare-fun e2 () (Set (Tuple S2)))
(declare-fun es1s2 () (Set (Tuple S1 S2)))
(assert (= es1s2 (product e1 e2)))

CVC4可以在这里考虑将一个集合作为包含该集合元素的1-元组的集合。

• 有什么根本的问题阻止它有这种行为吗？

Answer 1

这正是CVC4语法的工作方式。我把它用于工作，我们专门处理集合理论。对于大多数有限关系集上的运算，CVC4期望有元组。

这个链接可能会有所帮助：https://cvc4.github.io/sets-and-relations因此，有限集的运算一般可以不带元组操作，而有限关系则需要元组。

此外，我发现本文有助于理解在CVC4：https://homepage.cs.uiowa.edu/~tinelli/papers/MenEtAl-CADE-17.pdf中实现set的理论。