Cleanup and a bit of documentation

src/lib/frontend/models.ml

@@ -38,7 +38,7 @@ type t = {
   propositional : Expr.Set.t;
   model : ModelMap.t;
   objectives: (Expr.t * objective_value) Util.MI.t;
-  terms_values : (Shostak.Combine.r * string) Expr.Map.t
+  terms_values : (Shostak.Combine.r * Hstring.t) Expr.Map.t
 }
 
 module MS = Map.Make(String)

src/lib/frontend/models.mli

@@ -40,7 +40,7 @@ type t = {
   propositional : Expr.Set.t;
   model : ModelMap.t;
   objectives: (Expr.t * objective_value) Util.MI.t;
-  terms_values : (Shostak.Combine.r * string) Expr.Map.t
+  terms_values : (Shostak.Combine.r * Hstring.t) Expr.Map.t
   (** A map from terms to their values in the model (as a
       representative of type X.r and as a string. *)
 }

src/lib/reasoners/uf.ml

@@ -999,6 +999,12 @@ let assign_next env =
   Debug.check_invariants "assign_next" env;
   res, env
 
+let save_cache () =
+  LX.save_cache ()
+
+let reinit_cache () =
+  LX.reinit_cache ()
+
 (**** Counter examples functions ****)
 let is_a_good_model_value r =
   match X.leaves r with
@@ -1022,7 +1028,7 @@ let model_repr_of_term t env mrepr unbounded =
     match unbounded with
     | Some string_repr ->
       assert (is_a_good_model_value rep && is_const_term rep);
-      (rep, string_repr), mrepr
+      (rep, Hstring.make string_repr), mrepr
     | None ->
       let cls =
         try SE.elements (MapX.find rep env.classes)
@@ -1034,7 +1040,8 @@ let model_repr_of_term t env mrepr unbounded =
       in
       let rep, string_repr = X.choose_adequate_model t rep cls in
       assert (is_a_good_model_value rep && is_const_term rep);
-      (rep, string_repr), ME.add t (rep, string_repr) mrepr
+      let hs = Hstring.make string_repr in
+      (rep, hs), ME.add t (rep, hs) mrepr
 
 let is_optimization_op = function
   | Sy.Op Sy.Optimize _ -> true
@@ -1045,7 +1052,7 @@ module Cache = struct
   let records_cache = Hashtbl.create 17
   let abstracts_cache = Hashtbl.create 17
 
-  let store_array_get t (i : string) v =
+  let store_array_get t i v =
     match Hashtbl.find_opt arrays_cache t with
     | Some values ->
       Hashtbl.replace values i v
@@ -1061,7 +1068,7 @@ module Cache = struct
       let values = Hashtbl.create 17 in
       Hashtbl.add records_cache (id, ty) values
 
-  let store_record_access id ty (field : string) (v : string) =
+  let store_record_access id ty field v =
     match Hashtbl.find_opt records_cache (id, ty) with
     | Some values ->
       Hashtbl.replace values field v
@@ -1083,12 +1090,6 @@ module Cache = struct
     Hashtbl.clear abstracts_cache
 end
 
-let save_cache () =
-  LX.save_cache ()
-
-let reinit_cache () =
-  LX.reinit_cache ()
-
 let is_forbidden_symbol f ty =
   (X.is_solvable_theory_symbol f ty
    && not (Shostak.Records.is_mine_symb f ty))
@@ -1143,11 +1144,14 @@ let compute_concrete_model_of_val env t ((mdl, mrepr) as acc) unbounded =
             assert (xs_ta == []);
             Cache.store_array_get ta i (ret_rep |> snd);
             acc
-          | _ -> assert false
+          | _ ->
+            (* There is no semantic values for arrays, which means an array
+               is directly represented as a term. *)
+            assert false
         end
 
       | Sy.Name (id, _, _), [], Ty.Trecord trecord ->
-        Cache.store_record_sig (Hstring.view id) trecord;
+        Cache.store_record_sig id trecord;
         acc
 
       | Sy.Name (id, _, _), _, _ ->
@@ -1173,10 +1177,12 @@ let compute_concrete_model_of_val env t ((mdl, mrepr) as acc) unbounded =
         begin
           match X.type_info record with
           | Ty.Trecord trecord ->
-            Cache.store_record_access name trecord (Hstring.view field)
+            Cache.store_record_access name trecord field
               (ret_rep |> snd);
             mdl, mrepr
-          | _ -> assert false
+          | _ ->
+            (* This case is excluded by the parser. *)
+            assert false
         end
 
       | _ ->
@@ -1294,16 +1300,16 @@ let compute_concrete_model ?(optimized_splits=Util.MI.empty) env =
         let record_def =
           List.fold_left
             (fun record_def (field, field_ty) ->
-               match Hashtbl.find_opt vals (Hstring.view field) with
+               match Hashtbl.find_opt vals field with
                | Some v -> `Constant v :: record_def
                | None ->
                  let id = Id.Namespace.Abstract.fresh () |> Hstring.make in
                  `Abstract (id, [], field_ty) :: record_def
             ) [] trecord.Ty.lbs
           |> List.rev
         in
-        ModelMap.add (Hstring.make id, [], Ty.Trecord trecord) []
-          (`Record (Hstring.view trecord.Ty.record_constr, record_def)) mdl
+        ModelMap.add (id, [], Ty.Trecord trecord) []
+          (`Record (trecord.Ty.record_constr, record_def)) mdl
       ) Cache.records_cache mdl
   in
   (mdl, mrepr)
@@ -1320,7 +1326,7 @@ let compute_objectives ~optimized_splits env mrepr =
           | Minfinity -> seen_infinity := true; Obj_minfty
           | Value _ | Limit _ ->
             let (_r_x, r_s), _mrepr = model_repr_of_term e env mrepr None in
-            Obj_val r_s
+            Obj_val (Hstring.view r_s)
           | Unknown ->
             (* in this case, we should have !seen_infinity == true.
                Which is handled in the if branch. Moreover, we

src/lib/structures/modelMap.ml

@@ -30,21 +30,21 @@
 
 module X = Shostak.Combine
 
-type type_ = Id.t * Ty.t list * Ty.t [@@deriving ord]
+type sig_ = Id.t * Ty.t list * Ty.t [@@deriving ord]
 
 module Value = struct
   type simple = [
-    | `Abstract of type_
-    | `Constant of string
+    | `Abstract of sig_
+    | `Constant of Hstring.t
   ]
   [@@deriving ord]
 
-  type record = string * simple list
+  type record = Hstring.t * simple list
   [@@deriving ord]
 
   type array = [
-    | `Abstract of type_
-    | `Store of array * string * string
+    | `Abstract of sig_
+    | `Store of array * Hstring.t * Hstring.t
   ]
   [@@deriving ord]
 
@@ -60,22 +60,22 @@ module Value = struct
     | `Abstract (id, _, ty) ->
       Fmt.pf ppf "(as %a %a)" Id.pp id Ty.pp_smtlib ty
     | `Constant s ->
-      Fmt.pf ppf "%s" s
+      Fmt.pf ppf "%a" Hstring.print s
 
   let rec pp_array ppf arr =
     match arr 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@ %s %s)@]"
-        pp_array arr i v
+      Fmt.pf ppf "(@[<hv>store@ %a@ %a %a)@]"
+        pp_array arr Hstring.print i Hstring.print v
 
   let pp ppf v =
     match v with
     | `Array arr -> pp_array ppf arr
     | `Record (id, fields) ->
       Fmt.pf ppf "(@[<hv>%s %a)@]"
-        (Util.quoted_string id)
+        (Util.quoted_string (Hstring.view id))
         Fmt.(list ~sep:sp pp_simple) fields
     | #simple as w -> pp_simple ppf w
 
@@ -102,6 +102,12 @@ module Graph = struct
         type t = Value.t list [@@deriving ord]
       end)
 
+    (* For an argument (x_1, ..., x_n) of the function represented by the graph,
+       prints the SMT-LIB formula:
+        (and (= arg_0 x_1)
+          (and (= arg_1 x2)
+            ... (= arg_n x_n).
+    *)
     let rec pp_args ctr ppf = function
       | [] -> ()
       | [arg] ->
@@ -112,6 +118,12 @@ module Graph = struct
           Value.pp arg
           (pp_args (ctr + 1)) args
 
+    (* For a fiber [x; y; z; ...] of the function represented by the graph,
+       prints the SMT-LIB formula:
+        (or (and (= arg_0 x_0) (and (= arg_1 x_1) ...))
+          (or (and (= arg_0 y_0) (and (= arg_1 y_1) ...))
+            ...
+    *)
     let pp ppf fiber =
       let rec aux ppf seq =
         match seq () with
@@ -126,7 +138,7 @@ module Graph = struct
       aux ppf (to_seq fiber)
   end
 
-  (* Compute the inverse relation of the graph. *)
+  (* 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
@@ -153,7 +165,7 @@ end
 
 module P = Map.Make
     (struct
-      type t = type_ [@@deriving ord]
+      type t = sig_ [@@deriving ord]
     end)
 
 type t = {

src/lib/structures/modelMap.mli

@@ -28,25 +28,25 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type type_ = Id.t * Ty.t list * Ty.t
+type sig_ = Id.t * Ty.t list * Ty.t
 (** Type of a model value. *)
 
 module Value : sig
   type simple = [
-    | `Abstract of type_
+    | `Abstract of sig_
     (** An unique abstract value. *)
 
-    | `Constant of string
+    | `Constant of Hstring.t
     (** A string representation of a semantic value. *)
   ]
 
-  type record = string * simple list
+  type record = Hstring.t * simple list
 
   type array = [
-    | `Abstract of type_
+    | `Abstract of sig_
     (** An unique abstract array value. *)
 
-    | `Store of array * string * string
+    | `Store of array * Hstring.t * Hstring.t
     (** An array store: [(store array key value)]. *)
   ]
 
@@ -67,9 +67,9 @@ end
 type t
 (** Type of model. *)
 
-val add : type_ -> Value.t list -> Value.t -> t -> t
-(** [add type_ args ret mdl] adds the binding [args -> ret] to the partial graph
-    associated with the signature [type_]. *)
+val add : sig_ -> Value.t list -> Value.t -> t -> t
+(** [add sig_ args ret mdl] adds the binding [args -> ret] to the partial graph
+    associated with the signature [sig_]. *)
 
 val empty : suspicious:bool -> t
 (** An empty model. *)