KodKod 中的传递闭包

Question

我在使用 closure() 方法处理关系时遇到问题。如果有人可以解释传递闭包在 KodKod 中是如何工作的。

我们举个例子：

Relation r1 = Relation.nary("r1",4);
Relation r2 = Relation.binary("r2");
Relation i = Relation.unary("i");
Relation j = Relation.unary("j");
Formula f = r.in(r2.product(i).product(j));

我想知道怎么说：一个变量 k Oneof(j) 不在关系 r1 的传递闭包中

Answer 1

在您的示例中，关系r1 的Arity 为4，传递闭包只能应用于二元关系。

假设r1 是二进制的，类似于k.in(r1.closure()).not()，其中k 是计算结果为二进制关系的任何表达式，应该可以工作。