Preserve Subst literals

[bclement-ocp]

If we propagate the same literal with multiple origins in a single CC(X) step (i.e. they end up in the same fact list), we only keep one. We must make sure to keep the one with Subst origin, because those are used by the union-find communicate with the relations about representative changes.

Fixes #883

[bclement-ocp]

To clarify why this is correct: in #869 I claimed that equalities of Other origin were subsumed by equalities of Subst origin, but that equalities of CS origin were not, and so we needed to take care of them. These claims were somehow both correct and wrong.

• "Equalities of Subst origin" really just mean "substitutions". These are the equalities that are generated after calling X.solve in CC(X), which includes the equalities generated by actual congruence closure (and some additional equalities from AC(X)). These equalities are oriented: there is always a term (or AC symbol) on the left-hand side.
• "Equalities of Other" origin are arbitrary equalities that have to be processed, e.g. from user assertions, SAT or theory propagations, SAT decisions, etc. See Theory.assume in particular.
• "Equalities of CS origin" are chosen by case-splits
• "Equalities of NCS origin" are the negation of the choices chosen by case split. They can (to my understanding) only occur if we prove that the original CS choice is unsat.

(Side note: I guess i will make a separate documentation PR adding this information to Th_util…)

Note that it it more correct to state "atom" rather than "equalities" in all of the above, because they can also be comparisons or other predicates, except for the Subst origin which can only be equalities.

Since we are computing delayed functions, we only care about Subst equalities, which (roughly) correspond to updates of the union-find structure (updates of the class representative). This is why I stated "equalities of Other origin are subsumed`.

On the other hand, the reason I stated "we need equalities of CS origin" was empirical, and a rather unfortunate shortcut in my thinking: I could see cases where the theory makes a case split and the appropriate propagation was not performed, because we only saw the CS equality — never the Subst equality — and I (incorrectly) assumed this was because equalities of CS origin were treated differently. The confusion comes from the fact that I wrote this fix quite some time ago, and forgot that it never made it into a PR — so I thought that the issue was specific to CS equalities, which sort of makes sense (they are "special" in the sense that they are theory-level decisions).

In fact, it is because of the bug that this PR fixes: when an equality is processed, we remove all duplicate equalities that appear during its processing — in particular, for an equality already in solved form (as CS equalities often are, but not always), we generate an identical Subst equality, that gets promptly thrown away.

Hence:

• We need to make sure that when removing duplicates, we prefer keeping Subst equalities rather than CS or Other equalities, restoring the fact that both are subsumed by Subst equalities.
• We don't need to treat CS equalities differently in delayed functions processing, because they are now correctly subsumed by Subst equalities (like they should always have been)