Simplify n-ary and/or with duplicate operands like and(x, y, x)

[PhilippWendler]

SMTInterpol already does this, now we do it for all other solvers as well. This basically re-adds 36e47b5b (which was only for Z3), but in a more memory-efficient way (Stream.distinct() typically uses a regular HashSet, the old commit used a LinkedHashSet).

The performance and memory consumption are O(n) (amortized), just like the existing code. The overhead is basically one additional HashSet.

In the discussion of 36e47b5b it was decided to not do this, and I am also not really convinced this is worth it (we now consistently do simplifications of true and false operands including short-circuiting, this PR would only filter out duplicate operands, which are probably rare). But given the new implementation and that this is the first time we have an implementation that would make the behavior across all solvers consistent, I would like to put this up for discussion. At the least we will have this PR as permanent record of this potential solution.

Cf. #73

[kfriedberger]

As we never communicate towards the user, that formulae are structured as how they are build, I do not see a problem with merging this PR. There are more solvers (coming sooner or later) that do not support automatic simplification on that level. Additionally, this might even replace and simplify user code that does the same filtering on its own.

[PhilippWendler]

Yes, from a functional point of view there is no problem, there is just the overhead that was the cause for rejection in the past.

Not sure how many users actually do filter duplicates themselves, and everything except duplicates is also filtered out without this commit.

[PhilippWendler]

Ping? How about deciding on this one?