Simple ADTs with a single constructor are records (OCamlPro#1146)

* Simple ADTs with a single constructor are records

This PR fixes a bug in `D_cnf` that have been exposed by OCamlPro#1130.
Before merging `Enum` into `ADT` the situation was as follows:
- simple ADT with several constructors and with at least one payload
  was sent to the `Adt` theory
- simple ADT with several constructors but no payload was sent to `Enum` theory
- simple ADT with a single constructor was sent to the `Record` theory.

The last corner case includes a corner corner case:
An ADT with a single constructor without payload (so basically the unit type
with an extra step...)

The `D_cnf` included a bug. It produced single constructors without
payload of type ADT instead of type record but the check done in
`is_mine_symb` prevented from sending it to `Adt`. As I removed this
check, we got an assert on the following input:
```smt2
(set-logic ALL)
(declare-datatype t ((Record)))
(define-fun a () t Record)
(check-sat)
```

After this patch, the situation is as follows:
- simple ADT with several constructors is sent to the `Adt` theory
- simple ADT with only one constructor is sent to the `Record` theory
- mutually recursive ADT whose all the types are record is sent to the
  `Record` theory

src/lib/frontend/cnf.ml

@@ -115,7 +115,7 @@ let rec make_term quant_basename t =
 
     | TTrecord lbs ->
       let lbs = List.map (fun (_, t) -> mk_term t) lbs in
-      E.mk_term (Sy.Op Sy.Record) lbs ty
+      E.mk_record lbs ty
 
     | TTlet (binders, t2) ->
       let binders =

src/lib/frontend/d_cnf.ml

@@ -970,8 +970,16 @@ let rec mk_expr
             E.mk_term sy [] ty
 
           | B.Constructor _ ->
-            let ty = dty_to_ty term_ty in
-            E.mk_constr (Uid.of_dolmen tcst) [] ty
+            begin match dty_to_ty term_ty with
+              | Trecord _ as ty ->
+                E.mk_record [] ty
+              | Tadt _ as ty ->
+                E.mk_constr (Uid.of_dolmen tcst) [] ty
+              | Tunit ->
+                E.void
+              | ty ->
+                Fmt.failwith "unexpected type %a@." Ty.print ty
+            end
 
           | _ -> unsupported "Constant term %a" DE.Term.print term
         end
@@ -1343,7 +1351,7 @@ let rec mk_expr
                 E.mk_term sy l ty
               | Ty.Trecord _ ->
                 let l = List.map (fun t -> aux_mk_expr t) args in
-                E.mk_term (Sy.Op Sy.Record) l ty
+                E.mk_record l ty
               | _ ->
                 Fmt.failwith
                   "Constructor error: %a does not belong to a record nor an\

src/lib/reasoners/adt.ml

@@ -193,8 +193,11 @@ module Shostak (X : ALIEN) = struct
          if equal sel (embed sel_x) then X.term_embed t, ctx
          else sel_x, ctx (* canonization OK *)
     *)
-    | _ ->
-      assert false
+
+    | Sy.Op Sy.Constr _, _, Ty.Trecord _ ->
+      Fmt.failwith "unexpected record constructor %a@." E.print t
+
+    | _ -> assert false
 
   let hash x =
     abs @@ match x with

src/lib/structures/expr.ml

@@ -1264,6 +1264,8 @@ let mk_constr cons xs ty = mk_term (Sy.Op (Constr cons)) xs ty
 let mk_tester cons t =
   mk_builtin ~is_pos:true (Sy.IsConstr cons) [t]
 
+let mk_record xs ty = mk_term (Sy.Op Record) xs ty
+
 (** Substitutions *)
 
 let is_skolem_cst v =

src/lib/structures/expr.mli

@@ -282,6 +282,7 @@ val mk_ite : t -> t -> t -> t
 
 val mk_constr : Uid.t -> t list -> Ty.t -> t
 val mk_tester : Uid.t -> t -> t
+val mk_record : t list -> Ty.t -> t
 
 (** Substitutions *)