Changes to the FormulaManager.equal and FormulaManager.distinct API

[daniel-raffler]

As suggested by @PhilippWendler:

• We now allow Iterables as arguments for FormulaManager.equal and FormulaManager.distinct
• The methods have been renamed to makeEqual and makeDistinct
• We use FluentIterable to avoid unnecessary copying

See #559 for the discussion

[baierd]

LGTM

[PhilippWendler]

I would simply use Arrays.asList here. FluentIterable has no benefit, and just creates one more object for wrapping the array.

[daniel-raffler]

Done

[PhilippWendler]

This change doesn't make sense. If you really need a size, it is better to require Collection. Right now you force an unnecessary eager copy on every caller, even if they already have a Collection (as long as it does not happen to be an ImmutableCollection). If you would require Collection, only callers that do not have one need to copy.

I was thinking that you do not need the size and can accept Iterable at no cost. Checking whether the input is empty or has one element does not need the size. And it could anyway be done after the copy that is already made later on in the method.

[daniel-raffler]

It's possible to remove the check entirely, see 7009c86. However, we then have to handle the special case for each solver separately

Should I keep it this way, or revert to Collection for the argument type?

[PhilippWendler]

That is up to the maintainers to decide. It just wanted to say that it does not make sense to force an eager copy of an Iterable if using Collection would get rid of the copy, in particular given that there was yet another eager copy made.

Either requiring a Collection with no eager copy, or allowing Iterable with just one eager copy, or allowing Iterable with no eager copy (and decentralized length checks) might be meaningful options. And there is also the alternative to check whether the Iterable has more than one element by using the iterator manually.