Ensuring variables are distinct

[maxeeem]

Given two variables x and y and a goal below, it will match to both (1, 2) and (1, 1):

>>> x, y = var(), var()
>>> run(1, [x, y], eq((x, y), (1, 2)))
([1, 2],)
>>> run(1, [x, y], eq((x, y), (1, 1)))
([1, 1],)

If I want to restrict the matching to only distinct values for x and y, I can add a constraint:

>>> run(1, [x, y], eq((x, y), (1, 1)), neq(x, y))
()

The situation gets a bit more complicated when there are more than two variables involved but the basic recipe is the same. I found I have to add multiple neq constraints covering all of the possible combinations. So for three variables that would be:

...neq(x, y), neq(x, z), neq(y, z)

My question is whether this is the correct way of making sure all my variables are distinct or if there is another better way of doing it?

[brandonwillard]

There are a few other ways of which I can imagine right now, but they're all syntactical variations of the same thing. For example, you can write a simple Python function to generate all pairs of distinct logic variables and create neq goals for them.

[maxeeem]

Thanks! That's exactly what I ended up doing :) Just wanted to double check.