Standardize explanations in arrays (#4804)

Standardize explanations in arrays (#4804)

Some internal inferences had a non-standard way of providing (disjunctive) reasons and a custom way of explaining them.

This PR simplifies the array solver so that its explanations are analogous to the other equality engine based theory solvers (strings, datatypes, sets, ...). This is done in preparation for the incorporation of the proof equality engine in arrays, which follows a standard design for reasons/explanations.

The performance impact on QF arrays is negligible