如何克服断言表达式中的skolemization问题

Question

我有以下简单的例子。

sig B {}
pred P2 {some x1, x2: lone B | x1 != x2}
run P2 for 2

我的问题是如何在断言中重写pred约束而不会出现skolemization错误？

assert S { some x1, x2: lone B | x1 != x2} 
check S for 2

Answer 1

删除断言中单独的额外量词可以解决问题。

assert S { some x1, x2:  B | x1 != x2} 

你想评估什么？我怀疑使用lone B是你打算做的。