Wrong destructor for mutually recursive ADT

[Halbaroth]

The new Dolmen frontend didn't create the correct destructor in presence of mutually recursive ADT. For instance the input:

(set-logic ALL)
(declare-datatypes ((Data1 0) (Data2 0))
  (
    ((cons1 (d1 Int) (d2 Data2)))
    (
      (cons2 (d3 Data1))
      (cons3)
    )
  )
)
(declare-const a Data1)
(declare-const b Data2)
(declare-const x Int)
(assert ((_ is cons1) a))
(assert ((_ is cons3) b))
(assert (= (d1 a) x))
(check-sat)

raised an assertion in the record theory.
The presence of a flaw in a test of d_cnf to discriminate between records and ADT produced Sy.Access destructors intead of Sy.Destructor destructors on some terms whose the type is a mutually recursive ADT. For instance d1 a was translated into mk_term Sy.Access [a] ....

The fix consists in using the cache of AE types in d_cnf to discriminate between records and ADT.

Notice that the legacy frontend parses the previous file correctly.

[bclement-ocp]

I thought we were using the record flag to determine whether to create an ADT or a record. I guess we don't do it if they are in a mutually recursive nest because the legacy typechecker didn't either, and so the record flag is no longer correct there:

alt-ergo/src/lib/frontend/d_cnf.ml

Lines 766 to 768 in f7ae6f7

	(* If there are adts in the list of type declarations then records are
	converted to adts, because that's how it's done in the legacy typechecker.
	But it might be more efficient not to do that. *)

I think the fix is sound but we might want to revisit this choice — it doesn't make much sense to ever use the ADT theory for types that are records (or enums, for that matter), even if they are mutually recursive with ADTs. Probably should wait until we remove the legacy frontend (#556) to avoid parity issues.

[Halbaroth]

I noticed this comment. I agree it will be simpler to modify this after removing the legacy frontend.