feat(ADT): model generation (#1093)

* Model generation for ADT theory

This PR implements the model generation for ADT. The model generation is
done by the casesplit mechanism in `Adt_rel`.

To ensure the termination of the model generation, we sorts the constructors of nests during 
the parsing pass.

Author: Halbaroth

src/lib/dune

@@ -61,7 +61,7 @@
     Emap Gc_debug Hconsing Hstring Heap Lists Loc
     MyUnix Numbers Uqueue
     Options Timers Util Vec Version Steps Printer My_zip
-    Theories
+    Theories Nest
   )
 
  (js_of_ocaml

src/lib/frontend/d_cnf.ml

@@ -586,10 +586,11 @@ and handle_ty_app ?(update = false) ty_c l =
 let mk_ty_decl (ty_c: DE.ty_cst) =
   match DT.definition ty_c with
   | Some (
-      Adt { cases = [| { cstr = { id_ty; _ } as cstr; dstrs; _ } |]; _ }
+      Adt { cases = [| { cstr = { id_ty; _ } as cstr; dstrs; _ } |]; _ } as adt
     ) ->
     (* Records and adts that only have one case are treated in the same way,
        and considered as records. *)
+    Nest.add_nest [adt];
     let tyvl = Cache.store_ty_vars_ret id_ty in
     let rev_lbs =
       Array.fold_left (
@@ -610,9 +611,8 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
     let ty = Ty.trecord ~record_constr tyvl (Uid.of_dolmen ty_c) lbs in
     Cache.store_ty ty_c ty
 
-  | Some (
-      (Adt { cases; _ } as _adt)
-    ) ->
+  | Some ((Adt { cases; _ } as adt)) ->
+    Nest.add_nest [adt];
     let uid = Uid.of_dolmen ty_c in
     let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in
     let rev_cs, is_enum =
@@ -624,7 +624,7 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
               if Array.length dstrs = 0
               then true
               else (
-                let ty = Ty.t_adt (Uid.of_dolmen ty_c) tyvl in
+                let ty = Ty.t_adt uid tyvl in
                 Cache.store_ty ty_c ty;
                 false
               )
@@ -711,10 +711,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
       in
       Cache.store_ty ty_c ty
 
-    | Tadt (hs, tyl),
-      Some (
-        Adt { cases; ty = ty_c; _ }
-      ) ->
+    | Tadt (hs, tyl), Some (Adt { cases; ty = ty_c; _ }) ->
       let rev_cs =
         Array.fold_left (
           fun accl DE.{ cstr; dstrs; _ } ->
@@ -744,19 +741,21 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
     List.fold_left (
       fun (acc, ca) ty_c ->
         match DT.definition ty_c with
-        | Some (Adt { record; cases; _ }) as df
+        | Some (Adt { record; cases; _ } as df)
           when not record && Array.length cases > 1 ->
           df :: acc, true
-        | df -> df :: acc, ca
+        | Some (Adt _ as df) ->
+          df :: acc, ca
+        | Some Abstract | None ->
+          assert false
     ) ([], false) tdl
   in
+  Nest.add_nest rev_tdefs;
   let rev_l =
     List.fold_left (
       fun acc tdef ->
         match tdef with
-        | Some (
-            (DE.Adt { cases; record; ty = ty_c; }) as adt
-          ) ->
+        | DE.Adt { cases; record; ty = ty_c; } as adt ->
           let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in
 
           let cns, is_enum =
@@ -784,8 +783,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
             Cache.store_ty ty_c ty;
             (ty, Some adt) :: acc
           )
-        | None
-        | Some Abstract ->
+        | Abstract ->
           assert false (* unreachable in the second iteration *)
     ) [] (List.rev rev_tdefs)
   in
@@ -1009,8 +1007,7 @@ let rec mk_expr
 
           | B.Constructor _ ->
             let ty = dty_to_ty term_ty in
-            let sy = Sy.Op (Sy.Constr (Uid.of_dolmen tcst)) in
-            E.mk_term sy [] ty
+            E.mk_constr (Uid.of_dolmen tcst) [] ty
 
           | _ -> unsupported "Constant term %a" DE.Term.print term
         end
@@ -1379,7 +1376,7 @@ let rec mk_expr
             let ty = dty_to_ty term_ty in
             begin match ty with
               | Ty.Tadt (_, _) ->
-                let sy = Sy.Op (Sy.Constr (Uid.of_dolmen tcst)) in
+                let sy = Sy.constr @@ Uid.of_dolmen tcst in
                 let l = List.map (fun t -> aux_mk_expr t) args in
                 E.mk_term sy l ty
               | Ty.Trecord _ ->

src/lib/reasoners/adt.ml

@@ -401,12 +401,17 @@ module Shostak (X : ALIEN) = struct
 
 
   let assign_value _ _ _ =
-    Printer.print_err
-      "[ADTs.models] assign_value currently not implemented";
-    raise (Util.Not_implemented "Models for ADTs")
-
-  let to_model_term _r =
-    Printer.print_err
-      "[ADTs.models] to_model_term currently not implemented";
-    raise (Util.Not_implemented "Models for ADTs")
+    (* Model generation is performed by the case-split mechanism
+       in [Adt_rel]. *)
+    None
+
+  let to_model_term r =
+    match embed r with
+    | Constr { c_name; c_ty; c_args } ->
+      let args = Lists.try_map (fun (_, arg) -> X.to_model_term arg) c_args in
+      Option.bind args @@ fun args ->
+      Some (E.mk_constr c_name args c_ty)
+
+    | Select _ -> None
+    | Alien a -> X.to_model_term a
 end

src/lib/reasoners/adt_rel.ml

@@ -36,34 +36,50 @@ module LR = Uf.LX
 module Th = Shostak.Adt
 module SLR = Set.Make(LR)
 
+module TSet = Set.Make
+    (struct
+      type t = Uid.t
+
+      (* We use a dedicated total order on the constructors to ensure
+         the termination of the model generation. *)
+      let compare = Nest.compare
+    end)
+
 let timer = Timers.M_Adt
 
 module Domain = struct
   (* Set of possible constructors. The explanation justifies that any value
      assigned to the semantic value has to use a constructor lying in the
      domain. *)
   type t = {
-    constrs : Uid.Set.t;
+    constrs : TSet.t;
     ex : Ex.t;
   }
 
   exception Inconsistent of Ex.t
 
+  let[@inline always] cardinal { constrs; _ } = TSet.cardinal constrs
+
+  let[@inline always] choose { constrs; _ } =
+    (* We choose the minimal element to ensure the termination of
+       model generation. *)
+    TSet.min_elt constrs
+
   let[@inline always] as_singleton { constrs; ex } =
-    if Uid.Set.cardinal constrs = 1 then
-      Some (Uid.Set.choose constrs, ex)
+    if TSet.cardinal constrs = 1 then
+      Some (TSet.choose constrs, ex)
     else
       None
 
   let domain ~constrs ex =
-    if Uid.Set.is_empty constrs then
+    if TSet.is_empty constrs then
       raise @@ Inconsistent ex
     else
       { constrs; ex }
 
-  let[@inline always] singleton ~ex c = { constrs = Uid.Set.singleton c; ex }
+  let[@inline always] singleton ~ex c = { constrs = TSet.singleton c; ex }
 
-  let[@inline always] subset d1 d2 = Uid.Set.subset d1.constrs d2.constrs
+  let[@inline always] subset d1 d2 = TSet.subset d1.constrs d2.constrs
 
   let unknown ty =
     match ty with
@@ -73,31 +89,31 @@ module Domain = struct
       let constrs =
         List.fold_left
           (fun acc Ty.{ constr; _ } ->
-             Uid.Set.add constr acc
-          ) Uid.Set.empty body
+             TSet.add constr acc
+          ) TSet.empty body
       in
-      assert (not @@ Uid.Set.is_empty constrs);
+      assert (not @@ TSet.is_empty constrs);
       { constrs; ex = Ex.empty }
     | _ ->
       (* Only ADT values can have a domain. This case shouldn't happen since
          we check the type of semantic values in both [add] and [assume]. *)
       assert false
 
-  let equal d1 d2 = Uid.Set.equal d1.constrs d2.constrs
+  let equal d1 d2 = TSet.equal d1.constrs d2.constrs
 
   let pp ppf d =
     Fmt.(braces @@
-         iter ~sep:comma Uid.Set.iter Uid.pp) ppf d.constrs;
+         iter ~sep:comma TSet.iter Uid.pp) ppf d.constrs;
     if Options.(get_verbose () || get_unsat_core ()) then
       Fmt.pf ppf " %a" (Fmt.box Ex.print) d.ex
 
   let intersect ~ex d1 d2 =
-    let constrs = Uid.Set.inter d1.constrs d2.constrs in
+    let constrs = TSet.inter d1.constrs d2.constrs in
     let ex = ex |> Ex.union d1.ex |> Ex.union d2.ex in
     domain ~constrs ex
 
   let remove ~ex c d =
-    let constrs = Uid.Set.remove c d.constrs in
+    let constrs = TSet.remove c d.constrs in
     let ex = Ex.union ex d.ex in
     domain ~constrs ex
 end
@@ -209,6 +225,8 @@ module Domains = struct
         ) t.changed acc
     in
     acc, { t with changed = SX.empty }
+
+  let fold f t = MX.fold f t.domains
 end
 
 let calc_destructor d e uf =
@@ -327,7 +345,7 @@ let assume_th_elt t th_elt _ =
    This function alone isn't sufficient to produce a complete decision
    procedure for the ADT theory. For instance, let's assume we have three
    semantic values [r1], [r2] and [r3] whose the domain is `{C1, C2}`. It's
-   clear that `(distinct r1 r2 r3)` is unsatisfiable but we haven't enough
+   clear that `(distinct r1 r2 r3)` is unsatisfiable but we have not enough
    information to discover this contradiction.
 
    We plan to support model generation for ADT. As a by-product, we will got
@@ -566,45 +584,81 @@ let constr_of_destr ty d =
 
 exception Found of X.r * Uid.t
 
-(* Pick a delayed destructor application in [env.delayed]. Returns [None]
-   if there is no delayed destructor. *)
-let pick_delayed_destructor env =
-  try
-    Rel_utils.Delayed.iter_delayed
-      (fun r sy _e ->
-         match sy with
-         | Sy.Destruct d ->
-           raise_notrace @@ Found (r, d)
-         | _ ->
-           ()
-      ) env.delayed;
-    None
-  with Found (r, d) -> Some (r, d)
+let (let*) = Option.bind
 
-(* Do a case-split by choosing a semantic value [r] and constructor [c]
+(* Do a cases-plit by choosing a semantic value [r] and constructor [c]
    for which there are delayed destructor applications and propagate the
    literal [(not (_ is c) r)]. *)
+let split_delayed_destructor env =
+  if not @@ Options.get_enable_adts_cs () then
+    None
+  else
+    try
+      Rel_utils.Delayed.iter_delayed
+        (fun r sy _e ->
+           match sy with
+           | Sy.Destruct destr -> raise_notrace @@ Found (r, destr)
+           | _ -> ()
+        ) env.delayed;
+      None
+    with Found (r, d) ->
+      let c = constr_of_destr (X.type_info r) d in
+      Some (LR.mkv_builtin false (Sy.IsConstr c) [r])
+
+(* Pick a constructor in a tracked domain with minimal cardinal.
+   Returns [None] if there is no such constructor. *)
+let pick_best ds =
+  let* _, r, c =
+    Domains.fold
+      (fun r d best ->
+         let cd = Domain.cardinal d in
+         match Th.embed r, best with
+         | Constr _, _ -> best
+         | _, Some (n, _, _) when n <= cd -> best
+         | _ ->
+           let c = Domain.choose d in
+           Some (cd, r, c)
+      ) ds None
+  in
+  Some (r, c)
+
+let split_best_domain ~for_model uf =
+  if not for_model then
+    None
+  else
+    let ds = Uf.(GlobalDomains.find (module Domains) @@ domains uf) in
+    let* r, c = pick_best ds in
+    let _, cons = Option.get @@ build_constr_eq r c in
+    (* In the current implementation of `X.make`, we produce
+       a nonempty context only for interpreted semantic values
+       of the `Arith` and `Records` theories. The semantic
+       values `cons` never involves such values. *)
+    let nr, ctx = X.make cons in
+    assert (Lists.is_empty ctx);
+    Some (LR.mkv_eq r nr)
+
+let next_case_split ~for_model env uf =
+  match split_delayed_destructor env with
+  | Some _ as r -> r
+  | None -> split_best_domain ~for_model uf
+
 let case_split env uf ~for_model =
-  if Options.get_disable_adts () || not (Options.get_enable_adts_cs())
-  then
+  if Options.get_disable_adts () then
     []
   else begin
-    assert (not for_model);
-    if Options.get_debug_adt () then
-      Debug.pp_domains "before cs"
-        (Uf.GlobalDomains.find (module Domains) (Uf.domains uf));
-    match pick_delayed_destructor env with
-    | Some (r, d) ->
-      if Options.get_debug_adt () then
+    match next_case_split ~for_model env uf with
+    | Some cs ->
+      if Options.get_debug_adt () then begin
+        Debug.pp_domains "before cs"
+          (Uf.GlobalDomains.find (module Domains) (Uf.domains uf));
         Printer.print_dbg ~flushed:false
           ~module_name:"Adt_rel" ~function_name:"case_split"
-          "found r = %a and d = %a@ " X.print r Uid.pp d;
-      (* CS on negative version would be better in general. *)
-      let c = constr_of_destr (X.type_info r) d in
-      let cs =  LR.mkv_builtin false (Sy.IsConstr c) [r] in
-      [ cs, true, Th_util.CS (Th_util.Th_adt, two) ]
+          "Assume %a" (Xliteral.print_view X.print) cs;
+      end;
+      [ cs, true, Th_util.CS (Th_util.Th_adt, two)]
     | None ->
-      Debug.no_case_split ();
+      if Options.get_debug_adt () then
+        Debug.no_case_split ();
       []
   end
 

src/lib/reasoners/enum_rel.ml

@@ -268,7 +268,7 @@ let tighten_domain rr nd domains =
    This function alone isn't sufficient to produce a complete decision
    procedure for the Enum theory. For instance, let's assume we have three
    semantic values [r1], [r2] and [r3] whose the domain is `{C1, C2}`. It's
-   clear that `(distinct r1 r2 r3)` is unsatisfiable but we haven't enough
+   clear that `(distinct r1 r2 r3)` is unsatisfiable but we have not enough
    information to discover this contradiction.
 
    Now, if we produce a case-split for one of these semantic values,

src/lib/reasoners/fun_sat.ml

@@ -1275,10 +1275,6 @@ module Make (Th : Theory.S) = struct
     match Options.get_instantiation_heuristic () with
     | INormal ->
       (* TODO: check if this test still produces a wrong model. *)
-      (* S: This seems spurious!
-         On example UFDT/20170428-Barrett/cdt-cade2015/data/gandl/cotree/
-         x2015_09_10_16_49_52_978_1009894.smt_in.smt2,
-         this returns a wrong model. *)
       update_model_and_return_unknown
         env (Options.get_last_interpretation ())
         ~unknown_reason:Incomplete (* may becomes ModelGen *)
@@ -1885,7 +1881,8 @@ module Make (Th : Theory.S) = struct
     Expr.reinit_cache ();
     Hstring.reinit_cache ();
     Shostak.Combine.reinit_cache ();
-    Uf.reinit_cache ()
+    Uf.reinit_cache ();
+    Nest.reinit ()
 
   let () =
     Steps.save_steps ();