I have an uninterpreted sort Dataset:
Dataset = z3.DeclareSort("Dataset")
When I create constants from this sort:
d = z3.FreshConst(ZDataset)
d2 = z3.FreshConst(ZDataset)
I want the solver to see them as different, so d == d2 should be unsat.
Is there any way to do this by default, so every time I create a constant, it is different from all others already made?
The most straightforward solution I can see is to create a mock uninterpreted function like:
mock = Function(
"mock", ZDataset, z3.IntSort()
)
and each time I create a constant, add a constraint to the solver:
solver.add(mock(d) == 0)
using a Python variable that is incremented each time.
Although it is not the cleanest solution, it makes the solver see them as different.
The mock function you're talking about is probably the easiest way to do this cleanly.
Another way would be to do:
solver.add(Distinct([d, d2, d3, ...]))
right before you call check. You need to do this for all such objects you created, so you might want to keep track of them in some sort of a list as they are created.
I don't think either solution is fundamentally better/worse from a performance perspective, though Distinct might be better as the solver understands it natively and thus might make some internal simplifications kick in earlier. It'd be best to experiment.