Use term_cst as identifiers of names

The goal of this PR is mainly to improve our API for models. Currently,
we use AE symbols as identifiers of declared constants in models.

Fix partially #1214

src/bin/common/solving_loop.ml

@@ -107,14 +107,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 Uid.Term_map.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 _ -> Uid.Term_map.add (Uid.of_term_cst id) t acc
     end
   | _ -> (* Named terms are expected to be definitions with simple
             names. *)
@@ -347,7 +347,7 @@ let main () =
     State.create_key ~pipe:"" "sat_state"
   in
 
-  let named_terms: DStd.Expr.term Util.MS.t State.key =
+  let named_terms: DStd.Expr.term Uid.Term_map.t State.key =
     State.create_key ~pipe:"" "named_terms"
   in
 
@@ -501,7 +501,7 @@ let main () =
     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 Uid.Term_map.empty
     |> DO.init
     |> State.init ~debug ~report_style ~reports ~max_warn ~time_limit
       ~size_limit ~response_file
@@ -793,15 +793,9 @@ let main () =
     | None -> "unknown"
   in
 
-  let print_terms_assignments =
-    Fmt.list
-      ~sep:Fmt.cut
-      (fun fmt (name, v) -> Fmt.pf fmt "(%s %s)" name v)
-  in
-
   let handle_get_assignment ~get_value st =
     let assignments =
-      Util.MS.fold
+      Uid.Term_map.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
@@ -813,7 +807,7 @@ let main () =
     in
     Printer.print_std
       "(@[<v 0>%a@])@,"
-      print_terms_assignments
+      Fmt.(list ~sep:cut @@ parens @@ pair ~sep:sp Uid.pp string)
       assignments
   in
 
@@ -933,7 +927,7 @@ let main () =
         |> DO.StrictMode.clear
         |> DO.ProduceAssignment.clear
         |> DO.init
-        |> State.set named_terms Util.MS.empty
+        |> State.set named_terms Uid.Term_map.empty
 
       | {contents = `Exit; _} -> raise Exit
 

src/lib/dune

@@ -58,7 +58,7 @@
     ; structures
     Commands Errors Explanation Fpa_rounding
     Parsed Profiling Satml_types Symbols
-    Expr Var Ty Typed Xliteral ModelMap Id Uid Objective Literal
+    Expr Var Ty Typed Xliteral ModelMap Uid Objective Literal
     ; util
     Emap Gc_debug Hconsing Hstring Heap Loc Numbers Uqueue
     Options Timers Util Vec Version Steps Printer

src/lib/frontend/d_cnf.ml

@@ -122,11 +122,10 @@ module Cache = struct
     List.map (store_tyv_ret ~is_var) tyvl
 
   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)
-    ) tvl
+    List.iter
+      (fun tv ->
+         store_sy tv @@ Sy.name @@ Uid.of_term_cst tv
+      ) tvl
 
   let store_ty_vars ?(is_var = true) ty =
     match DT.view ty with
@@ -628,12 +627,11 @@ 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 =
     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 @@ Uid.of_term_cst tcst
+      | _ -> Sy.name @@ Uid.of_term_cst tcst
     end
   in
   Cache.store_sy tcst sy;
@@ -645,7 +643,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)
+  Uid.of_term_cst 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
@@ -1889,9 +1887,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 ~defined:true @@ Uid.of_term_cst tcst in
             Cache.store_sy tcst sy
           | `Type_alias _ -> ()
           | `Instanceof _ ->

src/lib/frontend/frontend.ml

@@ -299,7 +299,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
     if Options.get_unsat_core () then Ex.singleton (Ex.RootDep {name;f;loc})
     else Ex.empty
 
-  let internal_decl ?(loc = Loc.dummy) (id : Id.typed) (env : env) : unit =
+  let internal_decl ?(loc = Loc.dummy) (id : ModelMap.profile) (env : env) : unit =
     ignore loc;
     match env.res with
     | `Sat | `Unknown ->

src/lib/frontend/models.ml

@@ -21,7 +21,7 @@ module X = Shostak.Combine
 module E = Expr
 module MS = Map.Make(String)
 
-let constraints = ref MS.empty
+let constraints = ref Uid.Term_map.empty
 
 type t = {
   propositional : Expr.Set.t;
@@ -195,12 +195,12 @@ module Pp_smtlib_term = struct
 
     | Sy.Name { hs = n; _ }, l -> begin
         let constraint_name =
-          try let constraint_name,_,_ =
-                (MS.find (Hstring.view n) !constraints) in
+          try
+            let constraint_name, _, _ = Uid.Term_map.find n !constraints in
             constraint_name
           with _ ->
-            let constraint_name = "c_"^(Hstring.view n)  in
-            constraints := MS.add (Hstring.view n)
+            let constraint_name = "c_" ^ Uid.show n  in
+            constraints := Uid.Term_map.add n
                 (constraint_name,
                  to_string_type (E.type_info t),
                  List.map (fun e -> to_string_type (E.type_info e)) l
@@ -243,7 +243,7 @@ module Why3CounterExample = struct
         (Format.dprintf "%t(assert %a)@ " acc pp_term e)
       ) prop_model (Format.dprintf "") in
     Format.fprintf fmt "@ ; constraints@ ";
-    MS.iter (fun _ (name,ty,args_ty) ->
+    Uid.Term_map.iter (fun _ (name,ty,args_ty) ->
         match args_ty with
         | [] ->
           Format.fprintf fmt "(declare-const %s %s)@ "

src/lib/frontend/typechecker.ml

@@ -451,20 +451,22 @@ module Env = struct
   let add_names env lv pp_ty loc =
     Types.monomorphized pp_ty;
     let ty = Types.ty_of_pp loc env.types None pp_ty in
-    add env lv Symbols.name ty
+    let fvar s = Symbols.name @@ Uid.of_string s in
+    add env lv fvar ty
 
   let add_names_lbl env lv pp_ty loc =
     Types.monomorphized pp_ty;
     let ty = Types.ty_of_pp loc env.types None pp_ty in
+    let fvar s = Symbols.name @@ Uid.of_string s in
     let rlv =
       List.fold_left (fun acc (x, lbl) ->
           let lbl = Hstring.make lbl in
           if not (Hstring.equal lbl Hstring.empty) then
-            Symbols.add_label lbl (Symbols.name x);
+            Symbols.add_label lbl (fvar x);
           x::acc
         ) [] lv in
     let lv = List.rev rlv in
-    add env lv Symbols.name ty
+    add env lv fvar ty
 
   let add_logics ?(kind=Other) env mk_symb names pp_profile loc =
     let decl, profile =
@@ -2185,7 +2187,7 @@ let axioms_of_rules loc name lf acc env =
       (fun acc f ->
          let name =
            Fmt.str "%s_%s"
-             (Id.Namespace.Internal.fresh ())
+             (Symbols.Namespace.Internal.fresh ())
              name
          in
          let td = {c = TAxiom(loc,name,Util.Default, f); annot = new_id () } in
@@ -2414,7 +2416,9 @@ let declare_fun env loc n ?(defined=false) ?ret_ty l  =
     | Some ty ->
       PPeq, PFunction(l,ty)
   in
-  let mk_symb hs = Symbols.name hs ~defined ~kind:Symbols.Other in
+  let mk_symb s =
+    Symbols.name (Uid.of_string s) ~defined ~kind:Symbols.Other
+  in
   let tlogic, env = Env.add_logics env mk_symb [n] ty loc in (* TODO *)
   env, infix, tlogic
 
@@ -2488,7 +2492,7 @@ let rec type_decl (acc, env) d assertion_stack =
 
   | Logic (loc, ac, lp, pp_ty) ->
     Options.tool_req 1 "TR-Typing-LogicFun$_F$";
-    let mk_symb hs = Symbols.name hs ~kind:ac in
+    let mk_symb s = Symbols.name (Uid.of_string s) ~kind:ac in
     let tlogic, env' = Env.add_logics env mk_symb lp pp_ty loc in
     let lp = List.map fst lp in
     let td = {c = TLogic(loc,lp,tlogic); annot = new_id () } in

src/lib/reasoners/ac.ml

@@ -205,14 +205,16 @@ module Make (X : Sig.X) = struct
       | Some ac, { f = Name { hs; 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 ~ns:Internal @@ Uid.do_mangle (fun s -> Some ("@" ^ s)) 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
       | 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 ~ns:Internal @@ Uid.of_string "@*" 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 ~ns:Internal @@ Uid.of_string "@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 ~ns:Internal @@ Uid.of_string "@*" 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 ~ns:Internal @@ Uid.of_string "@/" 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,9 @@ 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 =
+          E.mk_term (Sy.name ~ns:Internal @@ Uid.of_string "@%") [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

@@ -88,7 +88,7 @@ module type S = sig
 
   val extract_concrete_model :
     prop_model:Expr.Set.t ->
-    declared_ids:Id.typed list ->
+    declared_ids:ModelMap.profile list ->
     t -> Models.t
 
 end
@@ -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 ~ns:Internal @@ Uid.of_string "@bottom" in
+    X.make (Expr.mk_term sy [] Ty.Tint)
 
   let concat_leaves uf l =
     let concat_rec acc t =

src/lib/reasoners/ccx.mli

@@ -78,7 +78,7 @@ module type S = sig
 
   val extract_concrete_model :
     prop_model:Expr.Set.t ->
-    declared_ids:Id.typed list ->
+    declared_ids:ModelMap.profile list ->
     t -> Models.t
 
 end

src/lib/reasoners/fun_sat.ml

@@ -178,8 +178,8 @@ module Make (Th : Theory.S) = struct
     last_saved_model : Models.t Lazy.t option ref;
     unknown_reason : Sat_solver_sig.unknown_reason option;
 
-    declare_top : Id.typed list ref;
-    declare_tail : Id.typed list Stack.t;
+    declare_top : ModelMap.profile list ref;
+    declare_tail : ModelMap.profile list Stack.t;
     (** Stack of the declared symbols by the user. The field [declare_top]
         is the top of the stack and [declare_tail] is tail. In particular, this
         stack is never empty. *)
@@ -1875,7 +1875,7 @@ module Make (Th : Theory.S) = struct
     clear_instances_cache ();
     Th.reinit_cpt ();
     Symbols.clear_labels ();
-    Id.Namespace.reinit ();
+    Symbols.Namespace.reinit ();
     Var.reinit_cnt ();
     Satml_types.Flat_Formula.reinit_cpt ();
     Ty.reinit_decls ();

src/lib/reasoners/fun_sat.mli

@@ -37,7 +37,7 @@ module Make (_ : Theory.S) : sig
 
   val empty : ?selector:(Expr.t -> bool) -> unit -> t
 
-  val declare : t -> Id.typed -> t
+  val declare : t -> ModelMap.profile -> t
 
   val push : t -> int -> t
 

src/lib/reasoners/instances.ml

@@ -169,7 +169,7 @@ module Make(X : Theory.S) : S with type tbox = X.t = struct
                 matching = EM.max_term_depth env.matching (E.depth f) } in
     match E.form_view f with
     | E.Iff(f1, f2) ->
-      let p = E.mk_term (Symbols.name name) [] Ty.Tbool in
+      let p = E.mk_term (Symbols.name @@ Uid.of_string name) [] Ty.Tbool in
       let np = E.neg p in
       let defn =
         if E.equal f1 p then f2
@@ -179,7 +179,7 @@ module Make(X : Theory.S) : S with type tbox = X.t = struct
       add_ground_pred env ~guard p np defn ex
 
     | E.Literal _ ->
-      let p = E.mk_term (Symbols.name name) [] Ty.Tbool in
+      let p = E.mk_term (Symbols.name @@ Uid.of_string name) [] Ty.Tbool in
       let np = E.neg p in
       let defn =
         if E.equal p f then E.vrai

src/lib/reasoners/sat_solver_sig.ml

@@ -75,10 +75,10 @@ module type S = sig
       The optional argument [selector] is used to filter ground facts
       discovered by the instantiation engine. *)
 
-  val declare : t -> Id.typed -> unit
+  val declare : t -> ModelMap.profile -> unit
   (** [declare env id] declares a new identifier [id].
 
-      If the environment [env] isn't unsatisfiable and the model generation
+      If the environment [env] is not unsatisfiable and the model generation
       is enabled, the solver produces a model term for [id] which can be
       retrieved with [get_model]. *)
 

src/lib/reasoners/sat_solver_sig.mli

@@ -55,10 +55,10 @@ module type S = sig
       The optional argument [selector] is used to filter ground facts
       discovered by the instantiation engine. *)
 
-  val declare : t -> Id.typed -> unit
+  val declare : t -> ModelMap.profile -> unit
   (** [declare env id] declares a new identifier [id].
 
-      If the environment [env] isn't unsatisfiable and the model generation
+      If the environment [env] is not unsatisfiable and the model generation
       is enabled, the solver produces a model term for [id] which can be
       retrieved with [get_model]. *)