为什么 CVC4 产品运算符不适用于套装?

Why is CVC4 product operator not applying to sets?

提问人:dde 提问时间:5/2/2019 更新时间:12/4/2020 访问量:56

问:

我正在修补 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

评论


答:

0赞 Vladi 12/4/2020 #1

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

此链接可能会有所帮助: https://cvc4.github.io/sets-and-relations 因此,有限集的运算通常可以在没有元组的情况下进行操作,而有限关系则需要元组。

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