为什么CVC4产品运营商不适用于套装？答案

【问题标题】：Why is CVC4 product operator not applying to sets?为什么CVC4产品运营商不适用于套装？
【发布时间】：2019-09-20 19:32:34
【问题描述】：

我正在修改 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 元组的集合。

是否有任何基本问题阻止它出现这种行为？

【问题讨论】：

标签： smt cvc4

【解决方案1】：

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

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

另外，我发现这篇论文有助于理解 CVC4 中 set 实现背后的理论：https://homepage.cs.uiowa.edu/~tinelli/papers/MenEtAl-CADE-17.pdf

【讨论】：