ADT reasoning on distinct literals is incomplete

[Halbaroth]

The current implementation of the ADT theory is incomplete. By incomplete I mean the reasoning isn't capable to notice inconsistency of some ground problems involving only ADT and boolean symbols. I notice this flaw while documenting the module Adt_rel, see #1013.

For instance, Alt-Ergo answers Unknown on this input file:

(set-logic ALL)
(declare-datatype Data (
   (cons1 (d1 Bool))
   (cons2)
))
(declare-const x Data)
(declare-const y Data)
(declare-const z Data)
(assert ((_ is cons1) x))
(assert ((_ is cons1) y))
(assert ((_ is cons1) z))
(assert (distinct x y z))
(check-sat)

The expected answer is unsat. If we remove the second constructor cons2, Alt-Ergo will promote the ADT Data to a record and we got the correct answer.

This issue comes from the fact the assume function in Adt_rel ignores silently disequations when the involved constructors have payloads. Let's imagine we have two constructor applications: x = cons1 u and y = cons2 v and we assume that x <> y. Then we have to propagate u <> v to CC(X).

But if we have payloads with at least two fields? If x = cons1 u1 u2 and y = cons1 v1 v2 and we assume x <> y, then we have to propagate u1 <> v1 \/ u2 <> v2. In this case we have to propagate a clause but AE relations can only propagate literals!

The current code of assume does nothing if one of the involved constructor has a payload. We can do better if the payload has only one field but if we want to treat the general case, we have to work more.

This issue resembles a lot to the issue with the distinct literal. When I tried to propagate this literal in CC(X), I couldn't do it because its negation isn't literal but a clause.

A possible solution would be to change our definition of facts. Currently a fact is just an annotated literal but we could consider annotated clauses instead.

Another one would be to use a kind of union-find structure in Adt_rel to keep in mind all these constraints until we can produce a literal.