Forking off discussion about Skolemization from this thread about using disjoint “some” quantification:
https://alloytools.discourse.group/t/a-tip-for-working-with-complex-models
There’s a separate issue here that’s caused by our inability to control Skolemization at a fine grain. Suppose you have two predicates, maybe something like:
sig Node {edges: set Node}
pred containsK3 {
some disj x1, x2, x3: Node |
x1->x2 + x1->x3 + x2->x1 + x2->x3 +
x3->x2 + x3->x1 in edges
}pred someSeparatedNodes {
some disj x1, x2: Node |
x1 not in x2.^edges and
x2 not in x1.^edges
}run {containsK3 and someSeparatedNodes}
for exactly 5 Node
Now the variables in both predicates get Skolemized.
This is great for debugging – I can see where a complete subgraph is and find two nodes that are mutually unreachable. But the more of these predicates I have, the more the Skolem variables start to overwhelm the instance content and the more I rely on symmetry-breaking.
So I went in search for a way to control what gets Skolemized in Alloy, beyond the Skolem depth setting (which is global and doesn’t allow a setting of -1 to disable Skolemization entirely). Amusingly, I can manually control Skolemization by careful use of superfluous disjunction. This prevents all Skolemization:
run {(containsK3 and someSeparatedNodes) or Node != Node}
for exactly 5 Node
and this prevents Skolemization of the 2 variables in someSeparatedNodes:
run {(containsK3 and (someSeparatedNodes or Node != Node))}
for exactly 5 Node
So, that’s a useful trick, although it feels a little clumsy.