合金 - 集合差异导致变量和子句，集合并不会导致

Question

我很好奇何时开始评估，显然某些运算符会转换为子句而不是评估：

abstract sig Element {}
one sig A,B,C extend Element {}

one sig Test {
    test: set Element
}

pred Test1 { Test.test = A+B }
pred Test2 { Test.test = Element-C }

并分别运行

Test1

和

Test2

将为变量/子句提供不同的数字，具体来说：

Test1: 0 vars, 0 primary vars, 0 clauses
Test2: 5 vars, 3 primary vars, 4 clauses

因此，尽管

Element

是

abstract

并且其所有成员及其基数都是已知的，但差值似乎没有提前计算，而总和却是。我不想做任何假设，所以我对为什么会这样感兴趣。

+

运算符是否特殊？

为了提供一些背景信息，我尝试限制关系的域，并发现仅使用

+

似乎更有效，即使这些集合事先完全已知。

Answer 1

为了提供一些上下文，我尝试限制关系的域，并发现仅使用 + 似乎更有效，即使预先完全知道集合也是如此。

这几乎是正确的结论。原因是合金分析器试图从某些合金习语中推断关系范围。它使用保守的近似值，对于集合并集和乘积总是合理的，但对于集合差值则不然。这就是为什么对于上面示例中的

Test1

，合金分析器会推断

test

关系 (

this/Test.test: [[[A$0], [B$0]]]

) 的固定界限，因此无需调用求解器；对于

Test2

，

test

关系的边界不能缩小，因此被设置为最宽松的 (

this/Test.test: [[], [[A$0], [B$0], [C$0]]]

)，因此需要调用求解器来找到满足给定边界约束的解决方案。