Uniformization of internal identifiers generation (#905)

This PR centralizes how internal identifiers are created. This work is a first step before a simpler task, which is to replace the '!' by '.' in name identifiers.

src/lib/frontend/typechecker.ml

@@ -2152,7 +2152,11 @@ let axioms_of_rules loc name lf acc env =
   let acc =
     List.fold_left
       (fun acc f ->
-         let name = (Hstring.fresh_string ()) ^ "_" ^ name in
+         let name =
+           Fmt.str "%s_%s"
+             (Symbols.fresh_internal_string ())
+             name
+         in
          let td = {c = TAxiom(loc,name,Util.Default, f); annot = new_id () } in
          (td, env)::acc
       ) acc lf

src/lib/reasoners/arith.ml

@@ -458,7 +458,7 @@ module Shostak
     List.exists
       (fun x ->
          match X.term_extract x with
-         | Some t, _ -> E.is_fresh t
+         | Some t, _ -> E.is_internal_name t
          | _ -> false
       ) (X.leaves xp)
 

src/lib/reasoners/fun_sat.ml

@@ -1854,8 +1854,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     Steps.reinit_steps ();
     clear_instances_cache ();
     Th.reinit_cpt ();
-    Symbols.reinit_fresh_sy_cpt ();
     Symbols.clear_labels ();
+    Symbols.reset_id_builders ();
     Var.reinit_cnt ();
     Satml_types.Flat_Formula.reinit_cpt ();
     Ty.reinit_decls ();

src/lib/reasoners/satml_frontend.ml

@@ -1252,7 +1252,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
   let reinit_ctx () =
     Steps.reinit_steps ();
     Th.reinit_cpt ();
-    Symbols.reinit_fresh_sy_cpt ();
+    Symbols.reset_id_builders ();
     Symbols.clear_labels ();
     Var.reinit_cnt ();
     Satml_types.Flat_Formula.reinit_cpt ();

src/lib/reasoners/uf.ml

@@ -1029,7 +1029,7 @@ let compute_concrete_model ({ make; _ } as env) =
        (* Keep record constructors because models.ml expects them to be there *)
        if (X.is_solvable_theory_symbol f ty
            && not (Shostak.Records.is_mine_symb f ty))
-       || E.is_fresh t || E.is_fresh_skolem t
+       || E.is_internal_name t || E.is_internal_skolem t
        || E.equal t E.vrai || E.equal t E.faux
        || Sy.is_internal f
        then

src/lib/structures/expr.ml

@@ -811,17 +811,6 @@ let neg t =
 let is_int t = t.ty == Ty.Tint
 let is_real t = t.ty == Ty.Treal
 
-let is_fresh t =
-  match t with
-  | { f = Sy.Name (hs, _, _); xs = []; _ } ->
-    Hstring.is_fresh_string (Hstring.view hs)
-  | _ -> false
-
-let is_fresh_skolem t =
-  match t with
-  | { f = Sy.Name (hs, _, _); _ } -> Hstring.is_fresh_skolem (Hstring.view hs)
-  | _ -> false
-
 let name_of_lemma f =
   match form_view f with
   | Lemma { name; _ } -> name
@@ -938,7 +927,14 @@ let vrai =
 let faux = neg (vrai)
 let void = mk_term (Sy.Void) [] Ty.Tunit
 
-let fresh_name ty = mk_term (Sy.name (Hstring.fresh_string())) [] ty
+let fresh_name ty = mk_term (Sy.fresh_internal_name ()) [] ty
+
+let is_internal_name t =
+  match t with
+  | { f; xs = []; _ } -> Sy.is_fresh_internal_name f
+  | _ -> false
+
+let is_internal_skolem t = Sy.is_fresh_skolem t.f
 
 let positive_int i = mk_term (Sy.int i) [] Ty.Tint
 
@@ -1230,7 +1226,7 @@ let is_skolem_cst v =
 
 let get_skolem =
   let hsko = Hsko.create 17 in
-  let gen_sko ty = mk_term (Sy.fresh "@sko") [] ty in
+  let gen_sko ty = mk_term (Sy.fresh_skolem "@sko") [] ty in
   fun v ty ->
     try Hsko.find hsko v
     with Not_found ->
@@ -1701,7 +1697,7 @@ let mk_let let_v let_e in_e =
   let free_v_as_terms =
     SMap.fold (fun sy (ty ,_) acc -> (mk_term sy [] ty)::acc) free_vars []
   in
-  let let_sko = mk_term (Sy.fresh "_let") free_v_as_terms let_e_ty in
+  let let_sko = mk_term (Sy.fresh_skolem "_let") free_v_as_terms let_e_ty in
   let is_bool = type_info in_e == Ty.Tbool in
   mk_let_aux {let_v; let_e; in_e; let_sko; is_bool}
 
@@ -1716,8 +1712,12 @@ let skolemize { main = f; binders; sko_v; sko_vty; _ } =
   let tyvars = Format.asprintf "[%a]" pp_list sko_vty in
 
   let mk_sym cpt s =
-    (* garder le suffixe "__" car cela influence l'ordre *)
-    Sy.name (Format.sprintf "!?__%s%s!%d" s tyvars cpt)
+    Fmt.kstr
+      (fun str -> Sy.make_as_fresh_skolem str)
+      "%s%s!%d"
+      s
+      tyvars
+      cpt
   in
   let grounding_sbt =
     List.fold_left
@@ -2577,13 +2577,13 @@ module Purification = struct
         in_e, add_let let_v let_e lets
 
       | (Sy.Lit _ | Sy.Form _), _ ->
-        let fresh_sy = Sy.fresh ~is_var:true "Pur-F" in
+        let fresh_sy = Sy.fresh_skolem ~is_var:true "Pur-F" in
         mk_term fresh_sy [] t.ty , add_let fresh_sy t lets
 
       | _ -> (* detect ITEs *)
         match t.xs with
         | [_;_;_] when is_ite t.f ->
-          let fresh_sy = Sy.fresh ~is_var:true "Pur-Ite" in
+          let fresh_sy = Sy.fresh_skolem ~is_var:true "Pur-Ite" in
           mk_term fresh_sy [] t.ty , add_let fresh_sy t lets
 
         | _ ->

src/lib/structures/expr.mli

@@ -172,8 +172,8 @@ val size : t -> int
 val depth : t -> int
 val is_positive : t -> bool
 val neg : t -> t
-val is_fresh : t -> bool
-val is_fresh_skolem : t -> bool
+val is_internal_name : t -> bool
+val is_internal_skolem : t -> bool
 val is_int : t -> bool
 val is_real : t -> bool
 val type_info : t -> Ty.t

src/lib/structures/symbols.ml

@@ -386,19 +386,54 @@ let to_string s = to_string ~show_vars:true s
 let print_clean fmt s = Format.fprintf fmt "%s" (to_string_clean s)
 let print fmt s = Format.fprintf fmt "%s" (to_string s)
 
+module type Id = sig
+  val fresh : ?base:string -> unit -> string
+  val reset_fresh_cpt : unit -> unit
+  val is_id : string -> bool
+  val make_as_fresh : string -> string
+end
 
-let fresh, reinit_fresh_sy_cpt =
-  let cpt = ref 0 in
-  let fresh ?(is_var=false) s =
-    incr cpt;
-    (* garder le suffixe "__" car cela influence l'ordre *)
-    let s = (Format.sprintf "!?__%s%i" s (!cpt)) in
-    if is_var then var @@ Var.of_string s else name s
-  in
-  let reinit_fresh_sy_cpt () =
-    cpt := 0
-  in
-  fresh, reinit_fresh_sy_cpt
+module MakeId(S : sig val prefix : string end) : Id = struct
+
+  let make_as_fresh = (^) S.prefix
+
+  let fresh, reset_fresh_cpt =
+    let cpt = ref 0 in
+    let fresh_string ?(base = "") () =
+      incr cpt;
+      make_as_fresh (base ^ (string_of_int !cpt))
+    in
+    let reset_fresh_string_cpt () =
+      cpt := 0
+    in
+    fresh_string, reset_fresh_string_cpt
+
+  let is_id = Compat.String.starts_with ~prefix:S.prefix
+end
+
+module InternalId = MakeId(struct let prefix = "!k" end)
+module SkolemId = MakeId(struct let prefix = "!?__" end)
+(* garder le suffixe "__" car cela influence l'ordre *)
+
+let fresh_internal_string () = InternalId.fresh ()
+let fresh_internal_name () = name (fresh_internal_string ())
+
+let fresh_skolem ?(is_var=false) base =
+  let fresh = SkolemId.fresh ~base () in
+  if is_var then
+    var @@ Var.of_string fresh
+  else
+    name fresh
+
+let make_as_fresh_skolem str = name (SkolemId.make_as_fresh str)
+
+let is_fresh_internal_name = function
+  | Name (hd, _, _) -> InternalId.is_id (Hstring.view hd)
+  | _ -> false
+
+let is_fresh_skolem = function
+  | Name (hd, _, _) -> SkolemId.is_id (Hstring.view hd)
+  | _ -> false
 
 let is_get f = equal f (Op Get)
 let is_set f = equal f (Op Set)
@@ -425,6 +460,10 @@ let label t = try Labels.find labels t with Not_found -> Hstring.empty
 
 let clear_labels () = Labels.clear labels
 
+let reset_id_builders () =
+  InternalId.reset_fresh_cpt ();
+  SkolemId.reset_fresh_cpt ()
+
 module Set : Set.S with type elt = t =
   Set.Make (struct type t=s let compare=compare end)
 

src/lib/structures/symbols.mli

@@ -128,9 +128,13 @@ val print_clean : Format.formatter -> t -> unit
 
 (*val dummy : t*)
 
-val fresh : ?is_var:bool -> string -> t
+val fresh_internal_string : unit -> string
+val fresh_internal_name : unit -> t
+val is_fresh_internal_name : t -> bool
 
-val reinit_fresh_sy_cpt : unit -> unit
+val fresh_skolem : ?is_var:bool -> string -> t
+val make_as_fresh_skolem : string -> t
+val is_fresh_skolem : t -> bool
 (** Resets to 0 the fresh symbol counter *)
 
 val is_get : t -> bool
@@ -151,6 +155,9 @@ val string_of_bound : bound -> string
 val clear_labels : unit -> unit
 (** Empties the labels Hashtable *)
 
+val reset_id_builders : unit -> unit
+(** Resets the `fresh_internal_name` and `fresh_skolem` counters. *)
+
 module Set : Set.S with type elt = t
 
 module Map : sig

src/lib/util/hstring.ml

@@ -58,35 +58,11 @@ let rec list_assoc x = function
   | [] -> raise Not_found
   | (y, v) :: l -> if equal x y then v else list_assoc x l
 
-let fresh_string, reset_fresh_string_cpt =
-  let cpt = ref 0 in
-  let fresh_string () =
-    incr cpt;
-    "!k" ^ (string_of_int !cpt)
-  in
-  let reset_fresh_string_cpt () =
-    cpt := 0
-  in
-  fresh_string, reset_fresh_string_cpt
-
-let is_fresh_string s =
-  try s.[0] == '!' && s.[1] == 'k'
-  with Invalid_argument s ->
-    assert (String.compare s "index out of bounds" = 0);
-    false
-
-let is_fresh_skolem s =
-  try s.[0] == '!' && s.[1] == '?'
-  with Invalid_argument s ->
-    assert (String.compare s "index out of bounds" = 0);
-    false
-
 let save_cache () =
   HC.save_cache ()
 
 let reinit_cache () =
-  HC.reinit_cache ();
-  reset_fresh_string_cpt ()
+  HC.reinit_cache ()
 
 module Arg = struct type t'= t type t = t' let compare = compare end
 module Set : Set.S with type elt = t = Set.Make(Arg)

src/lib/util/hstring.mli

@@ -46,12 +46,6 @@ val empty : t
 
 val list_assoc : t -> (t * 'a) list -> 'a
 
-val fresh_string : unit -> string
-
-val is_fresh_string : string -> bool
-
-val is_fresh_skolem : string -> bool
-
 val save_cache : unit -> unit
 (** Saves the module's cache *)