Refactoring `Enum_rel` using domains on class representatives only

[Halbaroth]

This PR refactors the Enum relations in order to use a proper type for the domains of enum semantic values.

Now, we only store domains for class representatives and I believe that the new implementation is simpler to understand and to maintain.

I don't use the functor Domains_make of Rel_utils as domain's propagations performed in Enum_rel are much simpler than the propagations in the BV theory.

[bclement-ocp]

To clarify the type of cases I have in mind when writing the comment above, I believe that using the SimpleDomains_make functor for the ADT theory and this test case:

(set-logic ALL)
(declare-datatype Opt_BV ((None) (Some (val (_ BitVec 8)))))
(declare-const x (_ BitVec 8))
(declare-const y Opt_BV)
(assert (= y (Some x)))
(assert (= ((_ extract 0 0) x) #b0))
(assert (= ((_ extract 1 1) x) #b0))
(check-sat)

would result in a bogus entry in the table of the form Some(val : .kX[7] @ 0[1]) -> Some with a mapping .kX[7] -> .kY[6] @ 0[1] in the union-find.

[Halbaroth]

For these reasons, I think it would be preferable to either use the more general Domains_make (adding back the propagate function; doing this will be more computationally expensive), or folding the SimpleDomains_make definition into the enum theory and inlining it for that theory specifically. Inlining it for that theory allows some optimizations because we can make use of the remark above (once we know the constructor we know the domain) to avoid looking in the map if we have a constructor (in both find and update). This has the disadvantage that the code needs to be copy-and-pasted from enum to adt, but if the plan is to merge both, that will be an acceptable temporary situation; since the SimpleDomains makes use of some specificity of these theories, it also makes sense for the implementation to be there rather than in the more generic Rel_utils module.

I think that inlining the functor is the best choice here.

[Halbaroth]

Inlining it for that theory allows some optimisations because we can make use of the remark above (once we know the constructor we know the domain) to avoid looking in the map if we have a constructor (in both find and update).

I'm no sure it's correct to do this optimization. As we only store domains for the current class representatives, we cannot return the default domain when we see a constructor. Let's imagine we have a semantic value r with the default domain in our map and after some computation in CC(X), we discover that r has to be equal to the constructor c. In our map, we substitute the r key by c but the explanation of this semantic value shouldn't be empty! We have to explain why the domain of r represented by the c key is a singleton. So I believe we should keep this implementation:

  let add r t =
    match MX.find r t.domains with
    | _ -> t
    | exception Not_found ->
      let nd = Domain.default r in
      internal_update r nd t

  let get r t =
    try MX.find r t.domains
    with Not_found -> Domain.default r

[bclement-ocp]

I am no sure it's correct to do this optimization. As we only store domains for the current class representative, we cannot return the default domain when we see a constructor. Let's imagine we have a semantic value r with the default domain in our map and after some computation in CC(X), we discover that r has to be equal to the constructor c. In our map, we substitute the r key by c but the explanation of this semantic value shouldn't be empty!

The semantics of an entry x → d in the map is that the domain for x is d, and the explanation stored in d is a justification of that fact. After substitution, the key in the map for which we are storing a domain is c, no longer r. The domain of c being the singleton { c } is a tautology, so we don't need to keep any explanations from the domain of r. The justification for r being equal to c is stored in the union-find data structure.

[bclement-ocp]

More formally: an entry x → d in the map is valid iff the implication explanation(d) ⇒ x ∈ d is true at level 0. The formula c ∈ { c } is always true, so an entry c → { c } in the map is always valid without additional explanations.