Use constant terms as identifiers in names and variables

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/bin/js/worker_js.ml

@@ -107,12 +107,13 @@ let main worker_id filename filecontent =
                 let used =
                   if Options.get_unsat_core () then Worker_interface.Unused
                   else Worker_interface.Unknown in
-                (name,b.Lexing.pos_lnum,e.Lexing.pos_lnum,!nb,used) :: acc
+                (Id.show name,b.Lexing.pos_lnum,e.Lexing.pos_lnum,
+                 !nb,used) :: acc
               | _ -> acc
             end
           | Some r ->
             let b,e = r.loc in
-            (r.name,b.Lexing.pos_lnum,e.Lexing.pos_lnum,
+            (Id.show r.name,b.Lexing.pos_lnum,e.Lexing.pos_lnum,
              !nb,Worker_interface.Used)
             :: acc
         ) tbl []

src/lib/frontend/frontend.ml

@@ -32,12 +32,12 @@ open Options
 module E = Expr
 module Ex = Explanation
 
-type used_context = Util.SS.t option
+type used_context = Id.Set.t option
 
 let unused_context name context =
   match context with
   | None -> false
-  | Some s -> not (Util.SS.mem name s)
+  | Some s -> not (Id.Set.mem name s)
 
 type status =
   | Unsat of Commands.sat_tdecl * Ex.t
@@ -147,11 +147,11 @@ module type S = sig
 
   val pop : int process
 
-  val assume : (string * E.t * bool) process
+  val assume : (Id.t * E.t * bool) process
 
-  val pred_def : (string * E.t) process
+  val pred_def : (Id.t * E.t) process
 
-  val query : (string * E.t * Ty.goal_sort) process
+  val query : (Id.t * E.t * Ty.goal_sort) process
 
   val th_assume : E.th_elt process
 
@@ -169,9 +169,12 @@ end
 let init_with_replay_used acc f =
   assert (Sys.file_exists f);
   let cin = open_in f in
-  let acc = ref (match acc with None -> Util.SS.empty | Some ss -> ss) in
+  let acc = ref (match acc with None -> Id.Set.empty | Some ss -> ss) in
   try
-    while true do acc := Util.SS.add (input_line cin) !acc done;
+    while true do
+      (* TODO: check this line? *)
+      acc := Id.Set.add (Id.of_string ~ns:Internal (input_line cin)) !acc
+    done;
     assert false
   with End_of_file ->
     Some !acc
@@ -238,7 +241,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
 
   let output_used_context g_name dep =
     let f = Options.get_used_context_file () in
-    let cout = open_out (sprintf "%s.%s.used" f g_name) in
+    let cout = open_out (asprintf "%s.%a.used" f Id.pp g_name) in
     let cfmt = Format.formatter_of_out_channel cout in
     Ex.print_unsat_core cfmt dep;
     close_out cout
@@ -258,7 +261,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
           (fun f ->
              SAT.assume satenv
                {E.ff=f;
-                origin_name = "";
+                origin_name = Id.of_string ~ns:Internal "";
                 gdist = -1;
                 hdist = -1;
                 trigger_depth = max_int;
@@ -276,7 +279,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
       ignore (SAT.unsat
                 satenv
                 {E.ff=E.vrai;
-                 origin_name = "";
+                 origin_name = Id.of_string ~ns:Internal "";
                  gdist = -1;
                  hdist = -1;
                  trigger_depth = max_int;
@@ -297,7 +300,8 @@ 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.typed)
+      (env : env) : unit =
     ignore loc;
     match env.res with
     | `Sat | `Unknown ->
@@ -322,9 +326,12 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
 
   let internal_assume
       ?(loc = Loc.dummy)
-      ((name, f, mf) : string * E.t * bool)
+      ((name, f, mf) : Id.t * E.t * bool)
       (env : env) =
-    let is_hyp = try (Char.equal '@' name.[0]) with _ -> false in
+    let is_hyp =
+      (* TODO: check this code! *)
+      Compat.String.starts_with ~prefix:"@" (Id.show name)
+    in
     if is_hyp || not (unused_context name env.used_context) then
       let expl =
         if is_hyp then

src/lib/frontend/frontend.mli

@@ -71,11 +71,11 @@ module type S = sig
 
   val pop : int process
 
-  val assume : (string * Expr.t * bool) process
+  val assume : (Id.t * Expr.t * bool) process
 
-  val pred_def : (string * Expr.t) process
+  val pred_def : (Id.t * Expr.t) process
 
-  val query : (string * Expr.t * Ty.goal_sort) process
+  val query : (Id.t * Expr.t * Ty.goal_sort) process
 
   val th_assume : Expr.th_elt process
 

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