Add generic equality and distinct to the API

[daniel-raffler]

Hello everyone,
in SMTLIB = and distinct are defined for all sorts and with a variable number of argument:

(par (A) (= A A Bool :chainable))
(par (A) (distinct A A Bool :pairwise))

We already support equality, but it's a different method for each FormulaManager, and only two arguments can be used. Distinct is only supported for bitvectors and numeral formulas, but missing from the other formula managers. While it's possible to simulate distinct by rewriting the formula, this leads to quadratically many terms, which may not always be desirable.

This PR tries to fix the issue by adding two generic methods for equality and distinct to the FormulaManager. The changes to the API are backwards compatible, and I've included a default implementation of distinct and = with multiple arguments for solvers that don't support these operations natively

[kfriedberger]

Overall, a very good idea.

Please check for some special cases, as well as the visitor for a resulting formula, if not yet done somewhere.

[kfriedberger]

Please add futher tests, e.g. for:

• zero items as parameters
• one item as parameters
• visitor of the resulting expression for several theories.

[daniel-raffler]

I've now added a few more tests:

• zero and one parameters are covered by testWrongNumberArgs
• visitors are tested by testEqualityVisitor and testDistinctVisitor

[kfriedberger]

Someone implementing this interface will need to adjust their implementation. We could provide a default implementation throwing UnsupportedOperationException if not overridden.

I am unsure if we ever did it that way in JavaSMT. Maybe we just added new methods as it is done here. Then we can continue with that strategy, i.e., keep the PR as-is. 😄

[daniel-raffler]

Hmm.. I think I'd prefer to keep it unimplemented. The compiler errors were quite helpful in figuring out what still needs to be updated. If we add a default implementation that throws UnsupportedOperationException users would have to read the changelog to find out that new methods were added