Only use Expr.t to store model values

As arrays can occur into model values, we need to use `Expr.t` to
represent them.

We cannot produce the appropriate model term with `Arrays.to_model_term`
because we haven't semantic values for arrays. Instead we perform two
passes on a pre-model generating with `X.to_model_term`.
- The first pass collects all the values of arrays and generates a model
  term for each array. If the array was declared by the user, we add
  it to the model.
- The second pass substitutes all the array identifiers in the pre-model
  by model terms we have generated in the first pass.

src/lib/reasoners/records.ml

@@ -439,7 +439,8 @@ module Shostak (X : ALIEN) = struct
         Option.bind l @@ fun l ->
         Some (E.mk_term Sy.(Op Record) l ty)
 
-      | Other (a, _) -> X.to_model_term a
+      | Other (a, _) ->
+        X.to_model_term a
       | Access _ -> None
     in fun r -> to_model_term (embed r)
 end

src/lib/reasoners/uf.ml

@@ -1065,8 +1065,7 @@ let terms env =
 
 (* Helper functions used by the caches during the computation of the model. *)
 module Cache = struct
-  let store_array_get arrays_cache (t : Expr.t) (i : ModelMap.Value.t)
-      (v : ModelMap.Value.t) =
+  let store_array_get arrays_cache (t : Expr.t) (i : Expr.t) (v : Expr.t) =
     match Hashtbl.find_opt arrays_cache t with
     | Some values ->
       Hashtbl.replace values i v
@@ -1080,17 +1079,17 @@ module Cache = struct
     match Hashtbl.find_opt abstracts_cache r with
     | Some abstract -> abstract
     | None ->
-      let abstract = Id.Namespace.Abstract.fresh () |> Hstring.make in
+      let abstract = Expr.mk_abstract (Expr.type_info t) in
       Hashtbl.add abstracts_cache r abstract;
       abstract
 end
 
 type cache = {
-  array_selects: (Expr.t, (ModelMap.Value.t, ModelMap.Value.t) Hashtbl.t)
+  array_selects: (Expr.t, (Expr.t, Expr.t) Hashtbl.t)
       Hashtbl.t;
   (** Stores all the get accesses to arrays. *)
 
-  abstracts: (r, Id.t) Hashtbl.t;
+  abstracts: (r, Expr.t) Hashtbl.t;
   (** Stores all the abstract values generated. This cache is necessary
       to ensure we don't generate twice an abstract value for a given symbol. *)
 }
@@ -1131,7 +1130,7 @@ let compute_concrete_model_of_val cache =
           List.fold_left
             (fun (arg_vals, arg_tys, mrepr) arg ->
                let rep_arg, mrepr = model_repr_of_term arg env mrepr in
-               ModelMap.Value.Constant rep_arg :: arg_vals,
+               rep_arg :: arg_vals,
                (Expr.type_info arg) :: arg_tys,
                mrepr
             )
@@ -1152,9 +1151,9 @@ let compute_concrete_model_of_val cache =
 
         | Sy.Op Sy.Set, _, _ -> acc
 
-        | Sy.Op Sy.Get, [Constant a; i], _ ->
+        | Sy.Op Sy.Get, [a; i], _ ->
           begin
-            store_array_select a i (Constant ret_rep);
+            store_array_select a i ret_rep;
             acc
           end
 
@@ -1165,9 +1164,8 @@ let compute_concrete_model_of_val cache =
               (* We cannot produce a concrete value as the type is abstract.
                  In this case, we produce an abstract value with the appropriate
                  type. *)
-              let abstract = get_abstract_for env t in
-              ModelMap.Value.Abstract (abstract, ty)
-            | _ -> ModelMap.Value.Constant ret_rep
+              get_abstract_for env t
+            | _ -> ret_rep
           in
           ModelMap.(add (id, arg_tys, ty) arg_vals value mdl), mrepr
 
@@ -1188,16 +1186,15 @@ let extract_concrete_model cache =
         terms (ModelMap.empty ~suspicious, ME.empty)
     in
     let model =
-      let open ModelMap.Value in
       Hashtbl.fold (fun t vals mdl ->
           (* We produce a fresh identifiant for abstract value in order to
              prevent any capture. *)
           let abstract = get_abstract_for env t in
           let ty = Expr.type_info t in
           let arr_val =
             Hashtbl.fold (fun i v arr_val ->
-                Store (arr_val, i, v)
-              ) vals (Abstract (abstract, ty))
+                Expr.ArraysEx.store arr_val i v
+              ) vals abstract
           in
           let id =
             let Expr.{ f; _ } = Expr.term_view t in
@@ -1208,7 +1205,21 @@ let extract_concrete_model cache =
                  [array_selects]. *)
               assert false
           in
-          ModelMap.add (id, [], ty) [] arr_val mdl
+          let mdl =
+            if not @@ Id.Namespace.Internal.is_id (Hstring.view id) then
+              ModelMap.add (id, [], ty) [] arr_val mdl
+            else
+              (* Internal identifiers can occur here if we need to generate
+                 a model term for an embedded array but this array isn't itself
+                 declared by the user. *)
+              mdl
+          in
+          (* We need to update the model [mdl] in order to substitute all the
+             occurrences of the array identifier [id] by an appropriate model
+             term. This cannot be performed while computing the model with
+             `compute_concrete_model_of_val` because we need to first iterate
+             on all the union-find environment to collect array values. *)
+          ModelMap.subst id arr_val mdl
         ) cache.array_selects model
     in
     { Models.propositional = prop_model; model; term_values = mrepr }

src/lib/structures/errors.ml

@@ -89,6 +89,10 @@ type mode_error =
   | Invalid_set_option of string
   | Forbidden_command of string
 
+type model_error =
+  | Subst_type_clash of Id.t * Ty.t * Ty.t
+  | Subst_not_model_term of Expr.t
+
 type error =
   | Parser_error of string
   | Lexical_error of Loc.t * string
@@ -98,6 +102,7 @@ type error =
   | Warning_as_error
   | Dolmen_error of (int * string)
   | Mode_error of Util.mode * mode_error
+  | Model_error of model_error
 
 exception Error of error
 
@@ -252,6 +257,18 @@ let report_mode_error fmt = function
   | Forbidden_command s ->
     fprintf fmt "Command %s" s
 
+let report_model_error ppf = function
+  | Subst_type_clash (id, ty1, ty2) ->
+    Fmt.pf ppf
+      "Cannot substitute the identifier %a of type %a by an expression of \
+       type %a"
+      Id.pp id
+      Ty.pp_smtlib ty1
+      Ty.pp_smtlib ty2
+
+  | Subst_not_model_term e ->
+    Fmt.pf ppf "The expression %a is not a model term" Expr.print e
+
 let report fmt = function
   | Parser_error s ->
     Format.fprintf fmt "Parser Error: %s" s;
@@ -277,3 +294,4 @@ let report fmt = function
       "Invalid action during %a mode: %a"
       Util.pp_mode mode
       report_mode_error merr;
+  | Model_error err -> report_model_error fmt err

src/lib/structures/errors.mli

@@ -97,6 +97,11 @@ type mode_error =
   | Invalid_set_option of string
   | Forbidden_command of string
 
+(** Errors raised while using models. *)
+type model_error =
+  | Subst_type_clash of Id.t * Ty.t * Ty.t
+  | Subst_not_model_term of Expr.t
+
 (** All types of error that can be raised *)
 type error =
   | Parser_error of string (** Error used at parser loading *)
@@ -107,9 +112,13 @@ type error =
   | Warning_as_error
   | Dolmen_error of (int * string)
   (** Error code + description raised by dolmen. *)
+
   | Mode_error of Util.mode * mode_error
   (** Error used when performing actions forbidden in some modes. *)
 
+  | Model_error of model_error
+  (** Error raised while using models. *)
+
 (** {2 Exceptions } *)
 
 exception Error of error

src/lib/structures/expr.ml

@@ -440,6 +440,10 @@ module SmtPrinter = struct
 
     | Sy.False, [] -> Fmt.pf ppf "false"
 
+    | Sy.Name { hs = n; _ }, []
+      when Id.Namespace.Abstract.is_id (Hstring.view n) ->
+      Fmt.pf ppf "(as %a %a)" Id.pp n Ty.pp_smtlib ty
+
     | Sy.Name { hs = n; _ }, [] -> Symbols.pp_name ppf (Hstring.view n)
 
     | Sy.Name { hs = n; _ }, _ :: _ ->
@@ -903,6 +907,10 @@ let void = mk_term (Sy.Void) [] Ty.Tunit
 
 let fresh_name ty = mk_term (Sy.fresh_internal_name ()) [] ty
 
+let mk_abstract ty =
+  let id = Id.Namespace.Abstract.fresh () |> Hstring.make in
+  mk_term (Sy.Name { hs = id; defined = false; kind = Other }) [] ty
+
 let is_internal_name t =
   match t with
   | { f; xs = []; _ } -> Sy.is_fresh_internal_name f
@@ -1025,7 +1033,7 @@ let mk_ite cond th el =
 
 let rec is_model_term e =
   match e.f, e.xs with
-  | (Op Constr _ | Op Record), xs -> List.for_all is_model_term xs
+  | (Op Constr _ | Op Record | Op Set), xs -> List.for_all is_model_term xs
   | Op Div, [{ f = Real _; _ }; { f = Real _; _ }] -> true
   | Op Minus, [{ f = Real q; _ }; { f = Real _; _ }] -> Q.equal q Q.zero
   | Op Minus, [{ f = Int i; _ }; { f = Int _; _ }] -> Z.equal i Z.zero

src/lib/structures/expr.mli

@@ -202,6 +202,11 @@ val int : string -> t
 val real : string -> t
 val bitv : string -> Ty.t -> t
 val fresh_name : Ty.t -> t
+
+val mk_abstract : Ty.t -> t
+(** [mk_abstract ty] creates an abstract model term of type [ty].
+    This function is intended to be used only in models. *)
+
 val pred : t -> t
 
 (** smart constructors for literals *)

src/lib/structures/id.ml

@@ -30,6 +30,8 @@
 
 type t = Hstring.t [@@deriving ord]
 
+let equal = Hstring.equal
+
 let pp ppf id =
   Dolmen.Smtlib2.Script.Poly.Print.id ppf
     (Dolmen.Std.Name.simple (Hstring.view id))

src/lib/structures/id.mli

@@ -30,6 +30,7 @@
 
 type t = Hstring.t [@@deriving ord]
 
+val equal : t -> t -> bool
 val show : t -> string
 val pp : t Fmt.t
 

src/lib/structures/modelMap.ml

@@ -33,40 +33,17 @@ module Sy = Symbols
 
 type sy = Id.t * Ty.t list * Ty.t [@@deriving ord]
 
-module Value = struct
-  type t =
-    | Abstract of Id.t * Ty.t
-    | Store of t * t * t
-    | Constant of Expr.t
-  [@@deriving ord]
-
-  let rec pp ppf v =
-    match v with
-    | Abstract (id, ty) ->
-      Fmt.pf ppf "(as %a %a)" Id.pp id Ty.pp_smtlib ty
-    | Store (arr, i, v) ->
-      Fmt.pf ppf "(@[<hv>store@ %a@ %a %a)@]"
-        pp arr pp i pp v
-    | Constant e ->
-      Expr.pp_smtlib ppf e
-
-  module Map = Map.Make (struct
-      type nonrec t = t
-
-      let compare = compare
-    end)
-end
-
 module Graph = struct
   module M = Map.Make
       (struct
-        type t = Value.t list [@@deriving ord]
+        type t = Expr.t list [@@deriving ord]
       end)
 
-  type t = Value.t M.t
+  type t = Expr.t M.t
 
   let empty = M.empty
   let add = M.add
+  let map = M.map
 
   (* A fiber of the function [f] over a value [v] is the set of all the values
      in the domain of [f] whose the image by [f] is [v].
@@ -75,11 +52,11 @@ module Graph = struct
      non-empty fibers of the function represented by its graph. *)
   module Fiber = struct
     include Set.Make (struct
-        type t = Value.t list [@@deriving ord]
+        type t = Expr.t list [@@deriving ord]
       end)
 
     let pp_arg ppf (ctr, arg) =
-      Fmt.pf ppf "(= arg_%i %a)" ctr Value.pp arg
+      Fmt.pf ppf "(= arg_%i %a)" ctr Expr.pp_smtlib arg
 
     (* For an argument (x_1, ..., x_n) of the function represented by the graph,
        prints the SMT-LIB formula:
@@ -112,26 +89,26 @@ module Graph = struct
   (* Compute all the fibers of the function represented by the graph. *)
   let inverse graph =
     M.fold (fun arg_vals ret_val acc ->
-        match Value.Map.find_opt ret_val acc with
+        match Expr.Map.find_opt ret_val acc with
         | Some fib ->
-          Value.Map.add ret_val (Fiber.add arg_vals fib) acc
+          Expr.Map.add ret_val (Fiber.add arg_vals fib) acc
         | None ->
-          Value.Map.add ret_val (Fiber.of_list [arg_vals]) acc
-      ) graph Value.Map.empty
+          Expr.Map.add ret_val (Fiber.of_list [arg_vals]) acc
+      ) graph Expr.Map.empty
 
   let pp_inverse ppf rel =
     let rec aux ppf seq =
       match seq () with
       | Seq.Nil -> ()
       | Cons ((ret_val, _), seq) when Stdcompat.Seq.is_empty seq ->
-        Fmt.pf ppf "%a" Value.pp ret_val
+        Fmt.pf ppf "%a" Expr.pp_smtlib ret_val
       | Cons ((ret_val, fiber), seq) ->
         Fmt.pf ppf "(@[<hv>ite %a@ %a@ %a)@]"
           Fiber.pp fiber
-          Value.pp ret_val
+          Expr.pp_smtlib ret_val
           aux seq
     in
-    aux ppf (Value.Map.to_seq rel)
+    aux ppf (Expr.Map.to_seq rel)
 end
 
 module P = Map.Make
@@ -157,13 +134,33 @@ let add ((id, arg_tys, _) as sy) arg_vals ret_val { values; suspicious } =
 
 let empty ~suspicious = { values = P.empty; suspicious }
 
+let rec subst_in_term id e c =
+  let Expr.{ f; xs; ty = ty'; _ } = Expr.term_view c in
+  match f, xs with
+  | Sy.Name { hs = id'; _ }, [] when Id.equal id id' ->
+    let ty = Expr.type_info e in
+    if not @@ Ty.equal ty ty' then
+      raise (Errors.Error (Model_error (Subst_type_clash (id, ty', ty))));
+    e
+  | _ ->
+    begin
+      let xs = List.map (subst_in_term id e) xs in
+      Expr.mk_term f xs ty'
+    end
+
+let subst id e { values; suspicious } =
+  if not @@ Expr.is_model_term e then
+    raise (Errors.Error (Model_error (Subst_not_model_term e)));
+  let values = P.map (Graph.map (subst_in_term id e)) values in
+  { values; suspicious }
+
 let pp_named_arg_ty ~unused ppf (arg_name, arg_ty) =
   let pp_unused ppf unused = if unused then Fmt.pf ppf "_" else () in
   Fmt.pf ppf "(%aarg_%i %a)" pp_unused unused arg_name Ty.pp_smtlib arg_ty
 
 let pp_define_fun ppf ((id, arg_tys, ret_ty), graph) =
   let inverse_rel = Graph.inverse graph in
-  let is_constant = Value.Map.cardinal inverse_rel = 1 in
+  let is_constant = Expr.Map.cardinal inverse_rel = 1 in
   let named_arg_tys = List.mapi (fun i arg_ty -> (i, arg_ty)) arg_tys in
   Fmt.pf ppf "(@[define-fun %a (%a) %a@ %a)@]"
     Id.pp id