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]

I think that the code in this PR is technically correct (the best kind of correct!) and without major flaws; as such, I'd be OK with merging it provided the remarks regarding comments/documentation are addressed.

However, I have concerns regarding regarding long-term maintainability (and some performance issues but those are probably minor) regarding the SimpleDomains_make functor, explained below.

To the best of my understanding, Alt-Ergo currently generates a Subst equality r → rr when r gets assigned to a new representative rr exactly two cases¹:

• r is a leaf (in the sense of X.is_a_leaf), or
• r is a term representative, i.e. there is a term t in the problem such that r = X.make t = Uf.make uf t

This means that my assertion "if we see r1 = r2 as Other then we will see r1 = rr and r2 = rr as Subst equalities", reproduced here in a comment, is not entirely correct (sorry! I keep forgetting about this edge case) if either r1 or r2 is not a term representative. For the Enum theory it does not matter because all enum semantic values are necessarily term representatives², but looking forward to #1087 we can have ADTs that are not class term representatives (see below for an example).

This is the reason why the Domains_make functor has a leaves_map field that it uses during substitution (see also discussion in #1040), so that we catch this edge case. SimpleDomains_make does not, and thus will miss domain updates in the presence of such synthetic representatives.

For the enum and ADT theories, this has zero impact on the correctness: the only way to generate synthetic representatives would be if they are argument of an ADT constructor (for instance, an ADT constructor with a bit-vector argument), but once we know the constructor, the unknown domain is the tightest possible! It does mean that the theory will go through different paths depending on whether a synthetic representative was substituted (we will not find it in the map, so we will return its unknown value) or no synthetic representative was substituted (we will find it in the map), which could easily cause subtle bugs in the future.

For these reasons, I think it would be preferrable 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 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). 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.

Footnotes

1. I think there is also a variant of the 2nd case where r results from the AC-completion of term representatives, but it does not really matter here. ↩

2. Except if users define an AC symbol over enums, but I'd classify this as an AC(X) bug since it impacts many theories, see Preserve mapping between old and new representatives with AC symbols #823 ↩

[bclement-ocp]

If this case can happen, it must not raise an Invalid_argument exception as per the documentation of Invalid_argument:

As a general rule, this exception should not be caught, it denotes a programming error and the code should be modified not to trigger it.

[bclement-ocp]

Forgot to update, but it looks like this case can no longer happen because we do check the types before calling Domains.add, so the code is correct but the comment no longer is.

[Halbaroth]

So why do you use invalid_arg in the very same situation in Bitv_rel?

[bclement-ocp]

Because in the Bitv_rel case it can't happen (there is a check for the type)! In fact, as noted in my 2nd comment, it is also the case here; the code is right but the comment that says "this case can happen" is wrong.

[bclement-ocp]

I think the following would be correct (e.g. would allow usage with Domains_make):

Suggested change

	let fold_leaves _f _rr _d _ = assert false
	let map_leaves _f _rr _ = assert false
	let fold_leaves f r d acc = f r d acc
	let map_leaves f r acc = f r acc

[bclement-ocp]

Isn't the function needed for models generation is add_rec? This comment is on add.

[bclement-ocp]

This change makes the documentation (and the function unknown) unclear: a "full domain" means that all values are possible, so it shouldn't depend on the semantic value.

What this does currently is that it returns a full domain in the Bitv theory, and either a full domain or a singleton domain for the Enum theory. It would be more foolproof to keep the unknown function as-is and to add a val create : X.r -> t (or val default) that returns a default domain for the representative r (it is a bit weird that unknown r is able to represent a precise singleton domain which is not "unknown" at all).

(Essentially this boils down to a difference in the way that the Domains_make and SimpleDomains_make functors want to use this function: Domains_make wants to call it on the leaves, then use map_leaves to build up a larger combined domain; SimpleDomains_make wants to call it on every value.)

[bclement-ocp]

Nit: this (and assume_distinct above) might make the intent clearer if written:

match Domain.as_singleton d with
| Some c -> ...
| None -> eqs

[bclement-ocp]

This does not replace it, it intersects it, and r is only marked changed if this causes the domain to change. The documentation should also make it clear that the new domain must have had any explanations justifying that it applies to r already added.

[Halbaroth]

Actually, Domain.update is only used in assume_distinct where nd is always a subset of the old domain, so we don't need to perform an intersection here.

[bclement-ocp]

If the code and the doc disagree fixing either if fine by me :)

(Note that skipping the intersection here is a bit risky because we could end up widening a domain, which is a completeness bug, so this should be called out in the documentation)

[Halbaroth]

I added a heavy assert to check we never update a domain with another one that isn't a subset.

[bclement-ocp]

case_split_limit makes it sound like it will be true if the limit is reached (I understood this on first read and was confused). Maybe call it case_split_ok or can_split?

[bclement-ocp]

I believe the function add can be a no-op; there is no need to add unknown domains since that is the default value returned by get, and the unknown r domain should be stable by propagation (unless some constraint applies, in which case the constraint will trigger the propagation).

[Halbaroth]

I add this function for sake of completeness. If you replace it by no-op, you got regressions. For instance the following problem from the test suite:

type t = A | B

logic f: t , int -> int

goal g8:
  forall x:t.
  forall y:int.
  f(x,y) = f(A,y) or f(x,y) = f(B,y)

is unsat with the current add operation but we got unknown with no-op.
The reason is simple. The map env.domains has two roles. It saves the domains of enum semantic values AND it saves the set of seen semantic values.

In the above test, x is never seen in a constraint before the first case-split round. If we don't add a domain for it in env.domains, the function Domains.fold won't see it while performing case-split and we lost the opportunity to discover the inconsistency here.

We can:

• add a set in the environment of the theory to save seen semantic values and fold on it during the case splits;
• keep the current implementation.

[bclement-ocp]

Ah, it is also used for case splits, that makes sense, thanks for checking it out. I think it would be useful to note that this is useful for case splits in a comment here.

[Halbaroth]

Sure, it wasn't clear at all ;)

[bclement-ocp]

If nd is equal to Domain.unknown r then there is nothing to do, or at least Domain.unknown r should be used instead (I think this is important to make sure domains associated with constants always have an empty explanation).

[Halbaroth]

I believe that we can replace this implementation by the following one:

  let update r d t =
    let od = get r t in
    let nd = Domain.intersect ~ex:Explanation.empty od d in
    if Domain.equal od nd then
      t
    else
      internal_update r nd t

The update function is only used in assume_distinct.
Now, Domain.equal od nd is true if and only if both od and nd are the default domain for the type of r. If r isn't in the map t.domains, this implementation doesn't add it to the map but I think it's ok.

Actually, add_rec ensures that all the enum semantic values of the current context are in the map t.domains.

[Halbaroth]

(I think this is important to make sure domains associated with constants always have an empty explanation).

To my understanding, the previous implementation of update could add unnecessary explanations. Technically, it's correct but if we want to use explanations to produce a proof for instance, we could got useless hypotheses in this proof, right?

[bclement-ocp]

Yeah, using get here should work and is simpler.

Unnecessary explanations translate to useless hypotheses in the proof, yes (depending on the way you see it, it is either useless hypotheses in the proof of the current branch, or unnecessary disjunctions in the proof of the user's statement, where we repeat the same sub-proof in both branches).

[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.

[bclement-ocp]

I think there are still a couple places where constant entries into the map slip through the cracks but otherwise looks good 👍

[bclement-ocp]

Suggested change

	match MX.find r t.domains with
	| _ -> t
	| exception Not_found ->
	if MX.mem r t.domains then t else

[bclement-ocp]

This is only true if r is not a constructor, no? We ignore Cons values in both case_split and get so I don't think entries for them are ever used.

[bclement-ocp]

update should be used rather than internal_update to avoid adding unnecessary explanations (and also avoid storing domains for constants)

[Halbaroth]

If we don't store at all domains for the constructor, we should use get in subst as follows to get the appropriate
intersection:

  let subst ~ex r nr t =
    match MX.find r t.domains with
    | d ->
      let nd = Domain.intersect ~ex d (get nr t) in
      let t = remove r t in
      update nr nd t

    | exception Not_found -> t

[bclement-ocp]

Ah right! In fact this:

      let nnd =
        match MX.find nr t.domains with
        | nd -> Domain.intersect ~ex d nd
        | exception Not_found -> d
      in

was a soundness bug because update does not intersect and so we lose the explanation ex if nr is not in t.domains.

[Halbaroth]

I also rename update into tighten. update isn't a meaningful name.