Refactoring Adt_rel using domains on class representatives only

[Halbaroth]

This PR is rebased on #1078 and #1086.

[Halbaroth]

As explained offline, we cannot use X.extract_term as we was done in casesplit in a previous version of this PR because there is no implementation of term_extract for AC symbols. For instance the following input file:

type t = A | B of { d : int }
logic e1, e2 : t
logic ac u : t, t -> t 

axiom a1 : e1 <> e2
axiom a2 : (u(e1, e2) ? B)
goal g : (u(e2, e1) ? B)

raises an exception with Alt-Ergo v2.5.3 for the same reason because we used X.term_extract in deduce_is_constr.

In the new implementation of casesplit, we produces a semantic literal instead of a syntactical one.

[Halbaroth]

@bclement-ocp ping

[bclement-ocp]

I have not done a very exhaustive side-by-side comparison with the previous implementation, but the new one looks correct. There are some nitpicks here and there, and I'd really like the raise_notrace removed for the reasons explained inline, but overall I am OK with this change.

[bclement-ocp]

There was some nice documentation for the corresponding type in the old implementation that could be moved here.

[bclement-ocp]

Suggested change

	raise_notrace @@ Inconsistent ex
	raise @@ Inconsistent ex

I am uneasy about using raise_notrace here, because this is the only place where we raise the Inconsistent exception for all the possible cases in the module, and it will make debugging errors in this module difficult.

(In contrast, in the SatML module, raise_notrace is used in a function that has exactly one caller — although in retrospect I think that using it there was a mistake)

[Halbaroth]

I agree. Actually I hesitated to remove it because I had to replace it by raise in order to debug the implementation.

[bclement-ocp]

This part should be moved to the doc of Domain.t type.

[bclement-ocp]

This looks like it checks whether c is an enum constructor of ty, is that correct? If so is_enum_constructor would be a more clear name, or a short comment on is_tightenable to explain this.

[Halbaroth]

I believe it's matter of taste. If I rename it into is_enum_constructor, I have to explain why we use this filter in assume_distinct. I suggest to rename it but I'll add a comment in assume_distinct too.

[Halbaroth]

I suggest this slightly different implementation:

let assume_distinct =
  let aux ~ex r r' env =
    let d = Domains.get r env.domains in
    match Domain.as_singleton d with
    | Some (c, ex') when is_enum_cons (X.type_info r) c ->
      let ex = Ex.union ex ex' in
      let nd = Domain.remove ~ex c d in
      tighten_domain r' nd env
    | Some _ | None ->
      (* If `d` is a singleton domain but its constructor has a payload,
         we cannot tighten the domain of `r'` because they could have
         distinct payloads. *)
      env
  in fun ~ex r1 r2 env ->
    aux ~ex r1 r2 env |> aux ~ex r2 r1

[bclement-ocp]

That looks OK to me and I agree, an explanatory comment is probably warranted whatever the name is.

I'd still suggest to do match Shostak.Adt.embed r with Constr { c_args = []; _ } -> ... in aux and get rid of is_tightenable / is_enum_cons entirely.

[Halbaroth]

Actually this implementation was buggy :p but thanks to the distinct_same_constructor I caught the bug. I removed the constructor from the singleton domain!

let assume_distinct =
  let aux ~ex r1 r2 env =
    let d1 = Domains.get r1 env.domains in
    let d2 = Domains.get r2 env.domains in
    match Domain.as_singleton d1 with
    | Some (c, ex') when is_enum_cons (X.type_info r1) c ->
      let ex = Ex.union ex ex' in
      let nd = Domain.remove ~ex c d2 in
      tighten_domain r2 nd env
    | Some _ | None ->
      (* If `d1` is a singleton domain but its constructor has a payload,
         we cannot tighten the domain of `r2` because they could have
         distinct payloads. *)
      env
  in fun ~ex r1 r2 env ->
    aux ~ex r1 r2 env |> aux ~ex r2 r1

[bclement-ocp]

Nit: It might be simpler to keep a match on extract r1 and extract r2 here as previously and tighten when seeing a Constr { c_args = []; _ } values. It should have the same effect (propagation ensures that singleton domain become Constr semantic values already) while being more readable (no need for is_tightenable).

[bclement-ocp]

Ideally the call to X.make should be called at the same point that the term is created (otherwise we might change the code in build_constr_eq and break this property accidentally). Could build_constr_eq call X.make and return Some (r, cons, r')?

[bclement-ocp]

Please keep the comment about doing this globally in CCX which is still relevant.

[bclement-ocp]

Is there a reason to add the existing assumptions before the new ones? It was done the other way before, and usually we can expect assume to be empty (any assumption not involving ADTs) even when result.assume is not.

[bclement-ocp]

The older was: List.rev_append assume result.assume. I am OK with using rev_append here; my point is that we should recurse on assume — not on result.assume.

(But I was confused and forgot that result.assume just came from Rel_utils.delayed and so the order does not actually matter)

[bclement-ocp]

Suggested change

	) ([], SE.empty) env.domains
	) ([], env.new_terms) env.domains

[bclement-ocp]

It would be more efficient to have propagate_domains accumulate over the existing env.new_terms since it has access to the env already (and then the new_terms returned by propagate_domains already contains env.new_terms).