Use constant terms as identifiers in names and variables

This PR changes the way we construct identifiers for names (in Symbols) and
variables (in Var).

We plan to completely replace the AE identifiers with identifiers from Dolmen.
This PR serves as an intermediate step from string-based identifiers to Dolmen
identifiers.

- All the identifiers are now managed in the Id module.
- Constant terms are used for declared or defined identifiers in the input file.
- Internal identifiers are still pre-mangled strings. Replacing them with
  Dolmen identifiers requires careful investigation, particularly in the AC(X)
  implementation.
- I haven't removed Id.typed yet. After this PR, the user identifiers will be
  typed, so we do not need to store them separately. If we use the internal
  type of the identifier, we will need to implement a conversion function from
  Dolmen type to Alt-Ergo type, which is not trivial. I prefer keeping this
  type and remove it after transitioning from Alt-Ergo types to Dolmen types.
- The new API of Id prevents us from creating duplicate fresh/fresh_ac/abstract
  identifiers.
- I still check that user identifiers do not start with . or @. In Before this
  PR, we mangled the identifier if it happened. In this PR, we crash. I don't
  have a strong opinion on this behavior, it was just simpler to implement
  this way.
- I use identifiers for term variables too. I preserved the internal
  representation because:
  1. The notion of local variables is AE-specific, whereas the local name in
     Dolmen identifiers is a distinct concept.
  2. After this PR, variables are typed but what is the type of Underscore?
     May be forall a. a?

This PR have been tested on ae-format (+2-2).

src/bin/common/solving_loop.ml

@@ -32,6 +32,8 @@ module DO = D_state_option
 module Sy = Symbols
 module O = Options
 
+module ConstSet = Map.Make (Dolmen.Std.Expr.Term.Const)
+
 exception Exit_with_code of int
 
 type solver_ctx = {
@@ -103,14 +105,14 @@ let cmd_on_modes st modes cmd =
 
 (** Adds the named terms of the statement [stmt] to the map accumulator [acc] *)
 let add_if_named
-    ~(acc : DStd.Expr.term Util.MS.t)
+    ~(acc : DStd.Expr.term ConstSet.t)
     (stmt : Typer_Pipe.typechecked D_loop.Typer_Pipe.stmt) =
   match stmt.contents with
-  | `Defs [`Term_def ({name = Simple n; _}, id, _, _, t)] ->
+  | `Defs [`Term_def (_, id, _, _, t)] ->
     begin
       match DStd.Expr.Id.get_tag id DStd.Expr.Tags.named with
       | None -> acc
-      | Some _ -> Util.MS.add n t acc
+      | Some _ -> ConstSet.add id t acc
     end
   | _ -> (* Named terms are expected to be definitions with simple
             names. *)
@@ -212,7 +214,7 @@ let process_source ?selector_inst ~print_status src =
     State.create_key ~pipe:"" "sat_state"
   in
 
-  let named_terms: DStd.Expr.term Util.MS.t State.key =
+  let named_terms: DStd.Expr.term ConstSet.t State.key =
     State.create_key ~pipe:"" "named_terms"
   in
 
@@ -357,7 +359,7 @@ let process_source ?selector_inst ~print_status src =
     State.empty
     |> State.set solver_ctx_key solver_ctx
     |> State.set partial_model_key None
-    |> State.set named_terms Util.MS.empty
+    |> State.set named_terms ConstSet.empty
     |> DO.init
     |> State.init ~debug ~report_style ~reports ~max_warn ~time_limit
       ~size_limit ~response_file
@@ -633,14 +635,14 @@ let process_source ?selector_inst ~print_status src =
   in
 
   (* Fetches the term value in the current model. *)
-  let evaluate_term get_value name term =
+  let evaluate_term get_value tcst term =
     (* There are two ways to evaluate a term:
        - if its name is registered in the environment, get its value;
        - if not, check if the formula is in the environment.
     *)
     let simple_form =
       Expr.mk_term
-        (Sy.name name)
+        (Sy.name @@ Id.of_term_cst ~defined:true tcst)
         []
         (Translate.dty_to_ty term.DStd.Expr.term_ty)
     in
@@ -652,12 +654,12 @@ let process_source ?selector_inst ~print_status src =
   let print_terms_assignments =
     Fmt.list
       ~sep:Fmt.cut
-      (fun fmt (name, v) -> Fmt.pf fmt "(%s %s)" name v)
+      (fun fmt (name, v) -> Fmt.pf fmt "(%a %s)" Util.pp_term_cst name v)
   in
 
   let handle_get_assignment ~get_value st =
     let assignments =
-      Util.MS.fold
+      ConstSet.fold
         (fun name term acc ->
            if DStd.Expr.Ty.equal term.DStd.Expr.term_ty DStd.Expr.Ty.bool then
              (name, evaluate_term get_value name term) :: acc
@@ -789,7 +791,7 @@ let process_source ?selector_inst ~print_status src =
         |> DO.StrictMode.clear
         |> DO.ProduceAssignment.clear
         |> DO.init
-        |> State.set named_terms Util.MS.empty
+        |> State.set named_terms ConstSet.empty
 
       | {contents = `Exit; _} -> raise Exit
 

src/lib/frontend/models.ml

@@ -194,14 +194,15 @@ module Pp_smtlib_term = struct
     | Sy.In(lb, rb), [t] ->
       fprintf fmt "(%a in %a, %a)" print t Sy.print_bound lb Sy.print_bound rb
 
-    | Sy.Name { hs = n; _ }, l -> begin
+    | Sy.Name { id; _ }, l -> begin
         let constraint_name =
+          let s = Id.show id in
           try let constraint_name,_,_ =
-                (MS.find (Hstring.view n) !constraints) in
+                (MS.find s !constraints) in
             constraint_name
           with _ ->
-            let constraint_name = "c_"^(Hstring.view n)  in
-            constraints := MS.add (Hstring.view n)
+            let constraint_name = "c_" ^ s  in
+            constraints := MS.add s
                 (constraint_name,
                  to_string_type (E.type_info t),
                  List.map (fun e -> to_string_type (E.type_info e)) l

src/lib/frontend/translate.ml

@@ -45,23 +45,6 @@ module HT =
     let hash (Id i)= DE.Id.hash i
   end)
 
-(** Helper function: returns the basename of a dolmen path, since in AE
-    the problems are contained in one-file (for now at least), the path is
-    irrelevant and only the basename matters *)
-let get_basename = function
-  | DStd.Path.Local { name; }
-  | Absolute { name; path = []; } -> name
-  | Absolute { name; path; } ->
-    Fmt.failwith
-      "Expected an empty path to the basename: \"%s\" but got: [%a]."
-      name (fun fmt l ->
-          match l with
-          | h :: t ->
-            Format.fprintf fmt "%s" h;
-            List.iter (Format.fprintf fmt "; %s") t
-          | _ -> ()
-        ) path
-
 module Cache = struct
 
   let ae_sy_ht: Sy.t HT.t = HT.create 100
@@ -124,8 +107,9 @@ module Cache = struct
   let store_sy_vl_names (tvl: DE.term_var list) =
     List.iter (
       fun ({ DE.path; _ } as tv) ->
-        let name = get_basename path in
-        store_sy tv (Sy.name name)
+        let name = Util.get_basename path in
+        (* TODO : Check this line! *)
+        store_sy tv (Sy.name @@ Id.of_string ~ns:Internal name)
     ) tvl
 
   let store_ty_vars ?(is_var = true) ty =
@@ -176,7 +160,7 @@ let builtin_term t = Dl.Typer.T.builtin_term t
 let builtin_ty t = Dl.Typer.T.builtin_ty t
 
 let ty (ty_cst : DE.ty_cst) ty =
-  let name = get_basename ty_cst.path in
+  let name = Util.get_basename ty_cst.path in
   DStd.Id.Map.add { name = DStd.Name.simple name; ns = Sort } @@
   fun env s ->
   builtin_ty @@
@@ -188,7 +172,7 @@ let fpa_rounding_mode, rounding_modes, add_rounding_modes =
     let constrs = Fpa_rounding.d_constrs in
     let add_constrs map =
       List.fold_left (fun map (c : DE.term_cst) ->
-          let name = get_basename c.path in
+          let name = Util.get_basename c.path in
           DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term }
             (fun env _ ->
                builtin_term @@
@@ -629,12 +613,12 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
 
 (** Handles term declaration by storing the eventual present type variables
     in the cache as well as the symbol associated to the term. *)
-let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) =
-  let name = get_basename path in
+let mk_term_decl ({ id_ty; tags; _ } as tcst: DE.term_cst) =
   let sy =
+    let id = Id.of_term_cst tcst in
     begin match DStd.Tag.get tags DE.Tags.ac with
-      | Some () -> Sy.name ~kind:Sy.Ac name
-      | _ -> Sy.name name
+      | Some () -> Sy.name ~kind:Sy.Ac id
+      | _ -> Sy.name id
     end
   in
   Cache.store_sy tcst sy;
@@ -646,7 +630,7 @@ let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) =
       List.map dty_to_ty arg_tys, dty_to_ty ret_ty
     | _ -> [], dty_to_ty id_ty
   in
-  (Hstring.make name, arg_tys, ret_ty)
+  (tcst, arg_tys, ret_ty)
 
 (** Handles the definitions of a list of mutually recursive types.
     - If one of the types is an ADT, the ADTs that have only one case are
@@ -744,15 +728,15 @@ let handle_patt_var id (DE.{ term_descr; _ } as term)  =
   match term_descr with
   | Cst ({ builtin = B.Base; id_ty; _ } as ty_c) ->
     let ty = dty_to_ty id_ty in
-    let v = Var.of_string @@ Fmt.to_to_string DE.Term.Const.print id in
-    let sy = Sy.Var v in
+    let v = Var.of_id @@ Id.of_term_cst ty_c in
+    let sy = Sy.var v in
     Cache.store_sy ty_c sy;
     v, id, ty
 
   | Var ({ builtin = B.Base; id_ty; _ } as ty_v) ->
     let ty = dty_to_ty id_ty in
-    let v = Var.of_string @@ Fmt.to_to_string DE.Term.Const.print id in
-    let sy = Sy.Var v in
+    let v = Var.of_id @@ Id.of_term_cst ty_v in
+    let sy = Sy.var v in
     Cache.store_sy ty_v sy;
     v, id, ty
 
@@ -815,10 +799,10 @@ end = struct
     | Cst ({ builtin = B.Constructor _; _ } as cst) ->
       Constr (cst, [])
 
-    | Var ({ builtin = B.Base; path; _ } as t_v) ->
+    | Var ({ builtin = B.Base; _ } as t_v) ->
       (* Should the type be passed as an argument
          instead of re-evaluating it here? *)
-      let v = Var.of_string (get_basename path) in
+      let v = Var.of_id @@ Id.of_term_cst t_v in
       let sy = Sy.var v in
       Cache.store_sy t_v sy;
       (* Adding the matched variable to the store *)
@@ -1439,9 +1423,8 @@ let rec mk_expr
       | Binder ((Let_par ls | Let_seq ls) as let_binder, body) ->
         let lsbis =
           List.map (
-            fun ({ DE.path; _ } as tv, t) ->
-              let name = get_basename path in
-              let v = Var.of_string name in
+            fun (tv, t) ->
+              let v = Var.of_id @@ Id.of_term_cst tv in
               Cache.store_sy tv (Sy.var v);
               v, t
           ) ls
@@ -1485,9 +1468,9 @@ let rec mk_expr
           (* the following is done in two iterations to preserve the order *)
           (* quantified variables *)
           let ntvl = List.rev_map (
-              fun (DE.{ path; id_ty; _ } as t_v) ->
+              fun (DE.{ id_ty; _ } as t_v) ->
                 dty_to_ty id_ty,
-                Var.of_string (get_basename path),
+                Var.of_id @@ Id.of_term_cst t_v,
                 t_v
             ) tvl
           in
@@ -1631,11 +1614,7 @@ and make_trigger ?(loc = Loc.dummy) ~name_base ~decl_kind
     | { DE.term_descr = Binder (Exists (_, qm_vars), e); _ } ->
       List.iter
         (fun (v : DE.term_var) ->
-           let var =
-             match v.path with
-             | Local { name } -> Var.local name
-             | _ -> assert false
-           in
+           let var = Var.local @@ Id.of_term_cst v in
            Cache.store_var v var)
         qm_vars;
       e
@@ -1950,9 +1929,8 @@ let make dloc_file acc stmt =
          names in a row. *)
       List.iter (fun (def : Typer_Pipe.def) ->
           match def with
-          | `Term_def (_, ({ path; _ } as tcst), _, _, _) ->
-            let name_base = get_basename path in
-            let sy = Sy.name ~defined:true name_base in
+          | `Term_def (_, tcst, _, _, _) ->
+            let sy = Sy.name @@ Id.of_term_cst ~defined:true tcst in
             Cache.store_sy tcst sy
           | `Type_alias _ -> ()
           | `Instanceof _ ->
@@ -1968,15 +1946,15 @@ let make dloc_file acc stmt =
           | `Term_def ( _, ({ path; tags; _ } as tcst), tyvars, terml, body) ->
             Cache.store_tyvl tyvars;
             let st_loc = dl_to_ael dloc_file loc in
-            let name_base = get_basename path in
+            let name_base = Util.get_basename path in
 
             let binders, defn =
               let rty = dty_to_ty body.term_ty in
               let binders, rev_args =
                 List.fold_left (
-                  fun (binders, acc) (DE.{ path; id_ty; _ } as tv) ->
+                  fun (binders, acc) (DE.{ id_ty; _ } as tv) ->
                     let ty = dty_to_ty id_ty in
-                    let v = Var.of_string (get_basename path) in
+                    let v = Var.of_id @@ Id.of_term_cst tv in
                     let sy = Sy.var v in
                     Cache.store_sy tv sy;
                     let e = E.mk_term sy [] ty in

src/lib/reasoners/ac.ml

@@ -202,17 +202,19 @@ module Make (X : Sig.X) = struct
   let abstract2 sy t r acc =
     if List.exists (is_other_ac_symbol sy) (X.leaves r) then
       match X.ac_extract r, Expr.term_view t with
-      | Some ac, { f = Name { hs; kind = Ac; _ } ; xs; ty; _ } ->
+      | Some ac, { f = Name { id; kind = Ac; _ } ; xs; ty; _ } ->
         (* It should have been abstracted when building [r] *)
         assert (not (Sy.equal sy ac.h));
-        let aro_sy = Sy.name ~ns:Internal ("@" ^ (HS.view hs)) in
+        let aro_sy =
+          Sy.name @@ Id.of_string ~ns:Internal ("@" ^ (Id.show id))
+        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
       | Some ac, { f = Op Mult; xs; ty; _ } ->
         (* It should have been abstracted when building [r] *)
         assert (not (Sy.equal sy ac.h));
-        let aro_sy = Sy.name ~ns:Internal "@*" in
+        let aro_sy = Sy.name @@ Id.of_string ~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 @@ let src = Logs.Src.create ~doc:"Arith" __MODULE__
 module Log = (val Logs.src_log src : Logs.LOG)
 
 let is_mult h = Sy.equal (Sy.Op Sy.Mult) h
-let mod_symb = Sy.name ~ns:Internal "@mod"
+let mod_symb = Sy.name @@ Id.of_string ~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,
@@ -246,7 +246,8 @@ module Shostak
       then
         (* becomes uninterpreted *)
         let tau =
-          E.mk_term (Sy.name ~kind:Sy.Ac ~ns:Internal "@*") [t1; t2] ty
+          let sy = Sy.name ~kind:Sy.Ac @@ Id.of_string ~ns:Internal "@*" in
+          E.mk_term sy [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
@@ -260,7 +261,10 @@ 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 ~ns:Internal "@/") [t1; t2] ty in
+        let tau =
+          let sy = Sy.name @@ Id.of_string ~ns:Internal "@/" in
+          E.mk_term sy [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
@@ -287,7 +291,10 @@ module Shostak
          (P.is_const p1 == None || P.is_const p2 == None)
       then
         (* becomes uninterpreted *)
-        let tau = E.mk_term (Sy.name ~ns:Internal "@%") [t1; t2] ty in
+        let tau =
+          let sy = Sy.name @@ Id.of_string ~ns:Internal "@%" in
+          E.mk_term sy [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

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

src/lib/reasoners/fun_sat.ml

@@ -1875,8 +1875,7 @@ module Make (Th : Theory.S) = struct
     clear_instances_cache ();
     Th.reinit_cpt ();
     Symbols.clear_labels ();
-    Id.Namespace.reinit ();
-    Var.reinit_cnt ();
+    Id.reinit ();
     Satml_types.Flat_Formula.reinit_cpt ();
     Ty.reinit_decls ();
     IntervalCalculus.reinit_cache ();
@@ -1888,7 +1887,6 @@ module Make (Th : Theory.S) = struct
 
   let () =
     Steps.save_steps ();
-    Var.save_cnt ();
     Expr.save_cache ();
     Hstring.save_cache ();
     Shostak.Combine.save_cache ();