cleanup: Use proper namespacing for names (#1028)

This introduces proper namespacing for variable names instead of relying
on string prefixes. In order to disturb the ordering as little as
possible, names are pre-mangled using their namespace (e.g. "x" in the
`Internal` namespace is stored as ".!x") and further operations
(hashing, comparison, etc.) are performed on the mangled names.

src/lib/reasoners/ac.ml

@@ -169,12 +169,12 @@ module Make (X : Sig.X) = struct
     | None -> r, acc
     | Some _ -> match Expr.term_view t with
       | { Expr.f = Sy.Name { hs; kind = Sy.Ac; _ }; xs; ty; _ } ->
-        let aro_sy = Sy.name ("@" ^ (HS.view hs)) in
+        let aro_sy = Sy.name ~ns:Internal ("@" ^ (HS.view hs)) in
         let aro_t = Expr.mk_term aro_sy xs ty  in
         let eq = Expr.mk_eq ~iff:false aro_t t in
         X.term_embed aro_t, eq::acc
       | { Expr.f = Sy.Op Sy.Mult; xs; ty; _ } ->
-        let aro_sy = Sy.name "@*" in
+        let aro_sy = Sy.name ~ns:Internal "@*" in
         let aro_t = Expr.mk_term aro_sy xs ty  in
         let eq = Expr.mk_eq ~iff:false aro_t t in
         X.term_embed aro_t, eq::acc

src/lib/reasoners/arith.ml

@@ -36,7 +36,7 @@ module Z = Numbers.Z
 module Q = Numbers.Q
 
 let is_mult h = Sy.equal (Sy.Op Sy.Mult) h
-let mod_symb = Sy.name "@mod"
+let mod_symb = Sy.name ~ns:Internal "@mod"
 
 let calc_power (c : Q.t) (d : Q.t) (ty : Ty.t) =
   (* d must be integral and if we work on integer exponentation,
@@ -243,7 +243,9 @@ module Shostak
       if Options.get_no_nla() && P.is_const p1 == None && P.is_const p2 == None
       then
         (* becomes uninterpreted *)
-        let tau = E.mk_term (Sy.name ~kind:Sy.Ac "@*") [t1; t2] ty in
+        let tau =
+          E.mk_term (Sy.name ~kind:Sy.Ac ~ns:Internal "@*") [t1; t2] ty
+        in
         let xtau, ctx' = X.make tau in
         P.add p (P.create [coef, xtau] Q.zero ty), List.rev_append ctx' ctx
       else
@@ -256,7 +258,7 @@ module Shostak
          (P.is_const p2 == None ||
           (ty == Ty.Tint && P.is_const p1 == None)) then
         (* becomes uninterpreted *)
-        let tau = E.mk_term (Sy.name "@/") [t1; t2] ty in
+        let tau = E.mk_term (Sy.name ~ns:Internal "@/") [t1; t2] ty in
         let xtau, ctx' = X.make tau in
         P.add p (P.create [coef, xtau] Q.zero ty), List.rev_append ctx' ctx
       else
@@ -283,7 +285,7 @@ module Shostak
          (P.is_const p1 == None || P.is_const p2 == None)
       then
         (* becomes uninterpreted *)
-        let tau = E.mk_term (Sy.name "@%") [t1; t2] ty in
+        let tau = E.mk_term (Sy.name ~ns:Internal "@%") [t1; t2] ty in
         let xtau, ctx' = X.make tau in
         P.add p (P.create [coef, xtau] Q.zero ty), List.rev_append ctx' ctx
       else

src/lib/reasoners/ccx.ml

@@ -245,7 +245,7 @@ module Main : S = struct
   end
   (*BISECT-IGNORE-END*)
 
-  let one, _ = X.make (Expr.mk_term (Sy.name "@bottom") [] Ty.Tint)
+  let one, _ = X.make (Expr.mk_term (Sy.name ~ns:Internal "@bottom") [] Ty.Tint)
 
   let concat_leaves uf l =
     let concat_rec acc t =

src/lib/reasoners/theory.ml

@@ -125,6 +125,8 @@ module Main_Default : S = struct
       | _ -> Ty.fresh_tvar ()
 
     let logics_of_assumed st =
+      (* NB: using an [Hstring.Map] here depends on the fact that name mangling
+         is done pre-emptively in [Symbols.name] *)
       SE.fold
         (fun t mp ->
            match E.term_view t with

src/lib/reasoners/uf.ml

@@ -1184,22 +1184,23 @@ let extract_concrete_model cache =
                 Expr.ArraysEx.store arr_val i v
               ) vals abstract
           in
-          let id =
+          let id, is_user =
             let Expr.{ f; _ } = Expr.term_view t in
             match f with
-            | Sy.Name { hs; _ } -> hs
+            | Sy.Name { hs; ns = User; _ } -> hs, true
+            | Sy.Name { hs; _ } -> hs, false
             | _ ->
               (* We only store array declarations as keys in the cache
                  [array_selects]. *)
               assert false
           in
           let mdl =
-            if not @@ Id.Namespace.Internal.is_id (Hstring.view id) then
+            if is_user 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. *)
+                 declared by the user -- see the [embedded-array] test . *)
               mdl
           in
           (* We need to update the model [mdl] in order to substitute all the

src/lib/reasoners/use.ml

@@ -53,7 +53,7 @@ let union_tpl (x1,y1) (x2,y2) =
   Options.exec_thread_yield ();
   SE.union x1 x2, SA.union y1 y2
 
-let one, _ = X.make (E.mk_term (Symbols.name "@bottom") [] Ty.Tint)
+let one, _ = X.make (E.mk_term (Symbols.name ~ns:Internal "@bottom") [] Ty.Tint)
 let leaves r =
   match X.leaves r with [] -> [one] | l -> l
 

src/lib/structures/expr.ml

@@ -440,15 +440,14 @@ module SmtPrinter = struct
 
     | Sy.False, [] -> Fmt.pf ppf "false"
 
-    | Sy.Name { hs = n; _ }, []
-      when Id.Namespace.Abstract.is_id (Hstring.view n) ->
+    | Sy.Name { ns = Abstract; hs = 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; _ }, [] -> Id.pp ppf n
 
     | Sy.Name { hs = n; _ }, _ :: _ ->
       Fmt.pf ppf "@[<2>(%a %a@])"
-        Symbols.pp_name (Hstring.view n)
+        Id.pp n
         Fmt.(list ~sep:sp pp |> box) xs
 
     | Sy.Var v, [] -> Var.print ppf v
@@ -905,15 +904,15 @@ let vrai =
 let faux = neg (vrai)
 let void = mk_term (Sy.Void) [] Ty.Tunit
 
-let fresh_name ty = mk_term (Sy.fresh_internal_name ()) [] ty
+let fresh_name ty =
+  mk_term (Sy.name ~ns:Fresh @@ Id.Namespace.Internal.fresh ()) [] 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
+  mk_term (Sy.name ~ns:Abstract @@ Id.Namespace.Abstract.fresh ()) [] ty
 
 let is_internal_name t =
   match t with
-  | { f; xs = []; _ } -> Sy.is_fresh_internal_name f
+  | { f = Name { ns = Fresh; _ }; xs = []; _ } -> true
   | _ -> false
 
 let is_internal_skolem t = Sy.is_fresh_skolem t.f
@@ -1722,7 +1721,7 @@ let skolemize { main = f; binders; sko_v; sko_vty; _ } =
 
   let mk_sym cpt s =
     Fmt.kstr
-      (fun str -> Sy.name (Id.Namespace.make_as_fresh_skolem str))
+      (fun str -> Sy.name ~ns:Skolem str)
       "%s%s!%d"
       s
       tyvars
@@ -2594,13 +2593,13 @@ module Purification = struct
         in_e, add_let let_v let_e lets
 
       | (Sy.Lit _ | Sy.Form _), _ ->
-        let fresh_var = Var.of_string @@ Sy.fresh_skolem_string "Pur-F" in
+        let fresh_var = Sy.fresh_skolem_var "Pur-F" in
         mk_term (Sy.Var fresh_var) [] t.ty , add_let fresh_var t lets
 
       | _ -> (* detect ITEs *)
         match t.xs with
         | [_;_;_] when is_ite t.f ->
-          let fresh_var = Var.of_string @@ Sy.fresh_skolem_string "Pur-Ite" in
+          let fresh_var = Sy.fresh_skolem_var "Pur-Ite" in
           mk_term (Sy.Var fresh_var) [] t.ty , add_let fresh_var t lets
 
         | _ ->

src/lib/structures/id.ml

@@ -43,45 +43,30 @@ let show id = Fmt.str "%a" pp id
 module Namespace = struct
   module type S = sig
     val fresh : ?base:string -> unit -> string
-    val is_id : string -> bool
   end
 
-  module Make (S : sig val prefix : string end) = struct
-    let make_as_fresh = (^) S.prefix
-
+  module Make () = struct
     let fresh, reset_fresh_cpt =
       let cpt = ref 0 in
       let fresh_string ?(base = "") () =
-        let res = make_as_fresh (base ^ (string_of_int !cpt)) in
+        let res = base ^ (string_of_int !cpt) in
         incr cpt;
         res
       in
       let reset_fresh_string_cpt () =
         cpt := 0
       in
       fresh_string, reset_fresh_string_cpt
-
-    let is_id = Stdcompat.String.starts_with ~prefix:S.prefix
   end
 
-  module Internal = Make (struct let prefix = ".k" end)
+  module Internal = Make ()
 
-  module Skolem = Make
-      (struct
-        (* garder le suffixe "__" car cela influence l'ordre *)
-        let prefix = ".?__"
-      end)
+  module Skolem = Make ()
 
-  let make_as_fresh_skolem = Skolem.make_as_fresh
-
-  module Abstract = Make (struct let prefix = "@a" end)
+  module Abstract = Make ()
 
   let reinit () =
     Internal.reset_fresh_cpt ();
     Skolem.reset_fresh_cpt ();
     Abstract.reset_fresh_cpt ()
 end
-
-let dummy_typed =
-  let id = Namespace.Internal.fresh () |> Hstring.make in
-  (id, [], Ty.Tunit)

src/lib/structures/id.mli

@@ -36,8 +36,6 @@ type typed = t * Ty.t list * Ty.t
     - Types of its arguments.
     - The returned type. *)
 
-val dummy_typed : typed
-
 val compare_typed : typed -> typed -> int
 val equal : t -> t -> bool
 val show : t -> string
@@ -46,15 +44,12 @@ val pp : t Fmt.t
 module Namespace : sig
   module type S = sig
     val fresh : ?base:string -> unit -> string
-    val is_id : string -> bool
   end
 
   module Internal : S
   module Skolem : S
   module Abstract : S
 
-  val make_as_fresh_skolem : string -> string
-
   val reinit : unit -> unit
   (** Resets the [fresh_internal_name], [fresh_skolem] and [fresh_abstract]
       counters. *)

src/lib/structures/satml_types.ml

@@ -921,9 +921,7 @@ module Flat_Formula : FLAT_FORMULA = struct
     if is_neg then a.Atom.neg,l else a,l
 
   let mk_new_proxy n =
-    let hs = Hs.make (".PROXY__" ^ (string_of_int n)) in
-    (* TODO: we should use a smart constructor here. *)
-    let sy = Symbols.Name { hs; kind = Symbols.Other; defined = false } in
+    let sy = Symbols.name ~ns:Internal @@ "PROXY__" ^ string_of_int n in
     E.mk_term sy [] Ty.Tbool
 
   let get_proxy_of f proxies_mp =
@@ -991,7 +989,7 @@ module Proxy_formula = struct
     if is_neg then a.Atom.neg,l else a,l
 
   let mk_new_proxy n =
-    let sy = Symbols.name @@ ".PROXY__" ^ (string_of_int n) in
+    let sy = Symbols.name ~ns:Internal @@ "PROXY__" ^ (string_of_int n) in
     E.mk_term sy [] Ty.Tbool
 
   let rec mk_cnf hcons f ((proxies, inv_proxies, new_vars, cnf) as accu) =