diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 2f0a5d038..13dd9d39d 100644 --- a/src/bin/common/solving_loop.ml +++ b/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 "(@[%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 diff --git a/src/lib/dune b/src/lib/dune index c67fb0a69..ec9ef74bb 100644 --- a/src/lib/dune +++ b/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 diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index 7c417b946..ad1bbcb86 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/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 _ -> diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index d2d437024..d1c3af487 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -299,7 +299,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.profile) (env : env) + : unit = ignore loc; match env.res with | `Sat | `Unknown -> diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml index 8c885caac..499b7e5fa 100644 --- a/src/lib/frontend/models.ml +++ b/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)@ " diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml index 569b4f85d..bb6783070 100644 --- a/src/lib/frontend/typechecker.ml +++ b/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 diff --git a/src/lib/reasoners/ac.ml b/src/lib/reasoners/ac.ml index bedf31684..838e2634b 100644 --- a/src/lib/reasoners/ac.ml +++ b/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 diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml index afc1b7ae9..3fb428eb7 100644 --- a/src/lib/reasoners/arith.ml +++ b/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 diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml index 5d9f56787..9a8c152e7 100644 --- a/src/lib/reasoners/ccx.ml +++ b/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 = diff --git a/src/lib/reasoners/ccx.mli b/src/lib/reasoners/ccx.mli index 83c09ed50..0e6f60d11 100644 --- a/src/lib/reasoners/ccx.mli +++ b/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 diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 347ef6cc4..74e61b7e9 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/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 (); diff --git a/src/lib/reasoners/fun_sat.mli b/src/lib/reasoners/fun_sat.mli index 6e018f04e..27e058177 100644 --- a/src/lib/reasoners/fun_sat.mli +++ b/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 diff --git a/src/lib/reasoners/instances.ml b/src/lib/reasoners/instances.ml index 6f9f7af11..384452ce5 100644 --- a/src/lib/reasoners/instances.ml +++ b/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 diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml index c8450e6d3..41712a65f 100644 --- a/src/lib/reasoners/sat_solver_sig.ml +++ b/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]. *) diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli index 9380bbbbc..218a6c0f3 100644 --- a/src/lib/reasoners/sat_solver_sig.mli +++ b/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]. *) diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index 59248fffa..7fec61350 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -92,7 +92,7 @@ module type SAT_ML = sig val solve : t -> unit val compute_concrete_model : - declared_ids:Id.typed list -> + declared_ids:ModelMap.profile list -> t -> Models.t Lazy.t * Objective.Model.t diff --git a/src/lib/reasoners/satml.mli b/src/lib/reasoners/satml.mli index 166b2ff5a..3dbb0705f 100644 --- a/src/lib/reasoners/satml.mli +++ b/src/lib/reasoners/satml.mli @@ -46,7 +46,7 @@ module type SAT_ML = sig val solve : t -> unit val compute_concrete_model : - declared_ids:Id.typed list -> + declared_ids:ModelMap.profile list -> t -> Models.t Lazy.t * Objective.Model.t diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 2200a8e0a..566ac533b 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -68,9 +68,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct (** The reason why satml raised [I_dont_know] if it does; [None] by default. *) - mutable declare_top : Id.typed list; - declare_tail : Id.typed list Stack.t; - (** Stack of the declared symbols by the user. The field [declare_top] + mutable declare_top : ModelMap.profile list; + declare_tail : ModelMap.profile list Stack.t; + (** Stack of the identifiers declared 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. *) } @@ -1411,8 +1411,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let reinit_ctx () = Steps.reinit_steps (); Th.reinit_cpt (); - Id.Namespace.reinit (); Symbols.clear_labels (); + Symbols.Namespace.reinit (); Var.reinit_cnt (); Objective.Function.reinit_cnt (); Satml_types.Flat_Formula.reinit_cpt (); diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index 31973c37d..36db54954 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -65,7 +65,7 @@ module type S = sig val compute_concrete_model : acts:Shostak.Literal.t Th_util.acts -> t -> unit val extract_concrete_model : - declared_ids:Id.typed list -> + declared_ids:ModelMap.profile list -> t -> Models.t Lazy.t * Objective.Model.t @@ -137,7 +137,7 @@ module Main_Default : S = struct let xs = List.map E.type_info xs in let xs, ty = try - let xs', ty', is_ac' = Hstring.Map.find hs mp in + let xs', ty', is_ac' = Uid.Term_map.find hs mp in assert (is_ac == is_ac'); let ty = generalize_types ty ty' in let xs = @@ -146,10 +146,10 @@ module Main_Default : S = struct xs, ty with Not_found -> xs, ty in - Hstring.Map.add hs (xs, ty, is_ac) mp + Uid.Term_map.add hs (xs, ty, is_ac) mp | _ -> mp - ) st Hstring.Map.empty + ) st Uid.Term_map.empty let types_of_assumed sty = let open Ty in @@ -213,12 +213,12 @@ module Main_Default : S = struct let print_logics ?(header=true) logics = print_dbg ~header "@[(* logics: *)@ "; - Hstring.Map.iter + Uid.Term_map.iter (fun hs (xs, ty, is_ac) -> print_dbg ~flushed:false ~header:false - "logic %s%s : %a%a@ " + "logic %s%a : %a%a@ " (if is_ac == Sy.Ac then "ac " else "") - (Hstring.view hs) + Uid.pp hs print_arrow_type xs Ty.print ty )logics; diff --git a/src/lib/reasoners/theory.mli b/src/lib/reasoners/theory.mli index 8a2387e53..9b4f21ba9 100644 --- a/src/lib/reasoners/theory.mli +++ b/src/lib/reasoners/theory.mli @@ -57,7 +57,7 @@ module type S = sig val compute_concrete_model : acts:Shostak.Literal.t Th_util.acts -> t -> unit val extract_concrete_model : - declared_ids:Id.typed list -> + declared_ids:ModelMap.profile list -> t -> Models.t Lazy.t * Objective.Model.t diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index 4049634cf..dfa66b707 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -1112,14 +1112,14 @@ module MED = Map.Make else Expr.compare a b end) -let is_suspicious_name hs = - match Hstring.view hs with +let is_suspicious_id id = + match Uid.show id with | "@/" | "@%" | "@*" -> true | _ -> false (* The model generation is known to be imcomplete for FPA theory. *) let is_suspicious_symbol = function - | Symbols.Name { hs; _ } when is_suspicious_name hs -> true + | Symbols.Name { hs; _ } when is_suspicious_id hs -> true | _ -> false let terms env = @@ -1238,7 +1238,7 @@ let compute_concrete_model_of_val cache = get_abstract_for env t | _ -> ret_rep in - ModelMap.(add (id, arg_tys, ty) arg_vals value mdl), mrepr + ModelMap.add (id, arg_tys, ty) arg_vals value mdl, mrepr | _ -> Printer.print_err @@ -1261,7 +1261,6 @@ let extract_concrete_model cache = (* We produce a fresh identifiant for abstract value in order to prevent any capture. *) let abstract = get_abstract_for env t in - let ty = Expr.type_info t in let arr_val = E.Table.fold (fun i v arr_val -> Expr.ArraysEx.store arr_val i v @@ -1277,9 +1276,10 @@ let extract_concrete_model cache = [array_selects]. *) assert false in + let p = id, [], Expr.type_info t in let mdl = if is_user then - ModelMap.add (id, [], ty) [] arr_val mdl + ModelMap.add p [] 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 @@ -1291,7 +1291,7 @@ let extract_concrete_model cache = term. This cannot be performed while computing the model with `compute_concrete_model_of_val` because we need to first iterate on all the union-find environment to collect array values. *) - ModelMap.subst id arr_val mdl + ModelMap.subst p arr_val mdl ) cache.array_selects model in { Models.propositional = prop_model; model; term_values = mrepr } diff --git a/src/lib/reasoners/uf.mli b/src/lib/reasoners/uf.mli index f73f3f794..ca722b533 100644 --- a/src/lib/reasoners/uf.mli +++ b/src/lib/reasoners/uf.mli @@ -160,7 +160,7 @@ val assign_next : t -> (r Xliteral.view * bool * Th_util.lit_origin) list * t (** Compute a counterexample using the Uf environment *) val extract_concrete_model : prop_model:Expr.Set.t -> - declared_ids:Id.typed list -> + declared_ids:ModelMap.profile list -> t -> Models.t diff --git a/src/lib/reasoners/use.ml b/src/lib/reasoners/use.ml index 1d6670acd..1d0404377 100644 --- a/src/lib/reasoners/use.ml +++ b/src/lib/reasoners/use.ml @@ -53,7 +53,10 @@ 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 ~ns:Internal "@bottom") [] Ty.Tint) +let one, _ = + let name = Symbols.name ~ns:Internal @@ Uid.of_string "@bottom" in + X.make (E.mk_term name [] Ty.Tint) + let leaves r = match X.leaves r with [] -> [one] | l -> l diff --git a/src/lib/structures/commands.ml b/src/lib/structures/commands.ml index 47856b2a4..5b03a9967 100644 --- a/src/lib/structures/commands.ml +++ b/src/lib/structures/commands.ml @@ -31,7 +31,7 @@ let src = Logs.Src.create ~doc:"Commands" __MODULE__ module Log = (val Logs.src_log src : Logs.LOG) type sat_decl_aux = - | Decl of Id.typed + | Decl of ModelMap.profile | Assume of string * Expr.t * bool | PredDef of Expr.t * string (*name of the predicate*) | RwtDef of (Expr.t Typed.rwt_rule) list @@ -48,9 +48,9 @@ type sat_tdecl = { let print_aux fmt = function | Decl (id, arg_tys, ret_ty) -> - Fmt.pf fmt "declare %a with type (%a) -> %a" - Id.pp id - Fmt.(list ~sep:comma Ty.print) arg_tys + Fmt.pf fmt "declare %a with type %a -> %a" + Uid.pp id + Fmt.(parens @@ list ~sep:comma Ty.print) arg_tys Ty.print ret_ty | Assume (name, e, b) -> diff --git a/src/lib/structures/commands.mli b/src/lib/structures/commands.mli index 152f1ca0b..0c9871f90 100644 --- a/src/lib/structures/commands.mli +++ b/src/lib/structures/commands.mli @@ -28,7 +28,7 @@ (* Sat entry *) type sat_decl_aux = - | Decl of Id.typed + | Decl of ModelMap.profile | Assume of string * Expr.t * bool | PredDef of Expr.t * string (*name of the predicate*) | RwtDef of (Expr.t Typed.rwt_rule) list diff --git a/src/lib/structures/errors.ml b/src/lib/structures/errors.ml index e5bc26035..597e54be4 100644 --- a/src/lib/structures/errors.ml +++ b/src/lib/structures/errors.ml @@ -88,7 +88,7 @@ type mode_error = | Forbidden_command of string type model_error = - | Subst_type_clash of Id.t * Ty.t * Ty.t + | Subst_type_clash of Uid.term_cst * Ty.t * Ty.t | Subst_not_model_term of Expr.t type error = @@ -262,7 +262,7 @@ let report_model_error ppf = function Fmt.pf ppf "Cannot substitute the identifier %a of type %a by an expression of \ type %a" - Id.pp id + Uid.pp id Ty.pp_smtlib ty1 Ty.pp_smtlib ty2 diff --git a/src/lib/structures/errors.mli b/src/lib/structures/errors.mli index 7f1794c17..992967f0e 100644 --- a/src/lib/structures/errors.mli +++ b/src/lib/structures/errors.mli @@ -97,7 +97,7 @@ type mode_error = (** Errors raised while using models. *) type model_error = - | Subst_type_clash of Id.t * Ty.t * Ty.t + | Subst_type_clash of Uid.term_cst * Ty.t * Ty.t | Subst_not_model_term of Expr.t (** All types of error that can be raised *) diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 7fec2a89e..20a80f610 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -475,13 +475,13 @@ module SmtPrinter = struct | Sy.False, [] -> Fmt.pf ppf "false" | Sy.Name { ns = Abstract; hs = n; _ }, [] -> - Fmt.pf ppf "(as %a %a)" Id.pp n Ty.pp_smtlib ty + Fmt.pf ppf "(as %a %a)" Uid.pp n Ty.pp_smtlib ty - | Sy.Name { hs = n; _ }, [] -> Id.pp ppf n + | Sy.Name { hs = n; _ }, [] -> Uid.pp ppf n | Sy.Name { hs = n; _ }, _ :: _ -> Fmt.pf ppf "@[<2>(%a %a@])" - Id.pp n + Uid.pp n Fmt.(list ~sep:sp pp |> box) xs | Sy.Var v, [] -> Var.print ppf v @@ -982,13 +982,22 @@ let vrai = let faux = neg (vrai) let fresh_name ty = - mk_term (Sy.name ~ns:Fresh @@ Id.Namespace.Internal.fresh ()) [] ty + let name = + Sy.name ~ns:Fresh @@ Uid.of_string @@ Sy.Namespace.Internal.fresh () + in + mk_term name [] ty let mk_abstract ty = - mk_term (Sy.name ~ns:Abstract @@ Id.Namespace.Abstract.fresh ()) [] ty + let name = + Sy.name ~ns:Abstract @@ Uid.of_string @@ Sy.Namespace.Internal.fresh () + in + mk_term name [] ty let fresh_ac_name ty = - mk_term (Sy.name ~ns:Fresh_ac @@ Id.Namespace.Internal.fresh ()) [] ty + let name = + Sy.name ~ns:Fresh_ac @@ Uid.of_string @@ Sy.Namespace.Internal.fresh () + in + mk_term name [] ty let is_fresh_ac_name t = match t with @@ -1800,7 +1809,7 @@ let skolemize { main = f; binders; sko_v; sko_vty; _ } = let mk_sym cpt s = Fmt.kstr - (fun str -> Sy.name ~ns:Skolem str) + (fun str -> Sy.name ~ns:Skolem @@ Uid.of_string str) "%s%s!%d" s tyvars diff --git a/src/lib/structures/id.ml b/src/lib/structures/id.ml deleted file mode 100644 index b8666d20a..000000000 --- a/src/lib/structures/id.ml +++ /dev/null @@ -1,60 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of OCamlPro *) -(* Non-Commercial Purpose License, version 1. *) -(* *) -(* As an exception, Alt-Ergo Club members at the Gold level can *) -(* use this file under the terms of the Apache Software License *) -(* version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* More details can be found in the directory licenses/ *) -(* *) -(**************************************************************************) - -type t = Hstring.t [@@deriving ord] - -type typed = t * Ty.t list * Ty.t [@@deriving ord] - -let equal = Hstring.equal - -let pp ppf id = - Dolmen.Smtlib2.Script.Poly.Print.id ppf - (Dolmen.Std.Name.simple (Hstring.view id)) - -let show id = Fmt.str "%a" pp id - -module Namespace = struct - module type S = sig - val fresh : ?base:string -> unit -> string - end - - module Make () = struct - let fresh, reset_fresh_cpt = - let cpt = ref 0 in - let fresh_string ?(base = "") () = - 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 - end - - module Internal = Make () - - module Skolem = Make () - - module Abstract = Make () - - let reinit () = - Internal.reset_fresh_cpt (); - Skolem.reset_fresh_cpt (); - Abstract.reset_fresh_cpt () -end diff --git a/src/lib/structures/id.mli b/src/lib/structures/id.mli deleted file mode 100644 index 5666a0a8a..000000000 --- a/src/lib/structures/id.mli +++ /dev/null @@ -1,44 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of OCamlPro *) -(* Non-Commercial Purpose License, version 1. *) -(* *) -(* As an exception, Alt-Ergo Club members at the Gold level can *) -(* use this file under the terms of the Apache Software License *) -(* version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* More details can be found in the directory licenses/ *) -(* *) -(**************************************************************************) - -type t = Hstring.t [@@deriving ord] - -type typed = t * Ty.t list * Ty.t -(** Typed identifier of function. In order: - - The identifier. - - Types of its arguments. - - The returned type. *) - -val compare_typed : typed -> typed -> int -val equal : t -> t -> bool -val show : t -> string -val pp : t Fmt.t - -module Namespace : sig - module type S = sig - val fresh : ?base:string -> unit -> string - end - - module Internal : S - module Skolem : S - module Abstract : S - - val reinit : unit -> unit - (** Resets the [fresh_internal_name], [fresh_skolem] and [fresh_abstract] - counters. *) -end diff --git a/src/lib/structures/modelMap.ml b/src/lib/structures/modelMap.ml index e8fee0f14..9ba0c3d2f 100644 --- a/src/lib/structures/modelMap.ml +++ b/src/lib/structures/modelMap.ml @@ -104,11 +104,13 @@ module Constraints = struct aux ppf (Expr.Map.to_seq c) end +type profile = Uid.term_cst * Ty.t list * Ty.t + module P = Map.Make (struct - type t = Id.typed + type t = profile - let compare = Id.compare_typed + let compare (id1, _, _) (id2, _, _) = Uid.compare id1 id2 end) type graph = @@ -123,25 +125,25 @@ type t = { suspicious : bool; } -let add ((id, arg_tys, _) as sy) arg_vals ret_val { values; suspicious } = +let add ((id, arg_tys, _) as p) arg_vals ret_val { values; suspicious } = if List.compare_lengths arg_tys arg_vals <> 0 then Fmt.invalid_arg "The arity of the symbol %a doesn't agree the number of \ - arguments" Id.pp id; + arguments" Uid.pp id; let constraints = - match P.find sy values with + match P.find p values with | C g -> g | Free _ | exception Not_found -> Constraints.empty in let values = - P.add sy (C (Constraints.add arg_vals ret_val constraints)) values + P.add p (C (Constraints.add arg_vals ret_val constraints)) values in { values; suspicious } let empty ~suspicious declared_ids = let values = List.fold_left - (fun values ((_, _, ret_ty) as sy) -> - P.add sy (Free (Expr.mk_abstract ret_ty)) values + (fun values ((_, _, ret_ty) as p) -> + P.add p (Free (Expr.mk_abstract ret_ty)) values ) P.empty declared_ids in @@ -150,7 +152,7 @@ let empty ~suspicious declared_ids = let rec subst_in_term id e c = let Expr.{ f; xs; ty = ty'; _ } = Expr.term_view c in match f, xs with - | Sy.Name { hs = id'; _ }, [] when Id.equal id id' -> + | Sy.Name { hs = id'; _ }, [] when Uid.equal id id' -> let ty = Expr.type_info e in if not @@ Ty.equal ty ty' then Errors.error (Model_error (Subst_type_clash (id, ty', ty))); @@ -161,7 +163,7 @@ let rec subst_in_term id e c = Expr.mk_term f xs ty' end -let subst id e { values; suspicious } = +let subst (id, _, _) e { values; suspicious } = if not @@ Expr.is_model_term e then Errors.error (Model_error (Subst_not_model_term e)); @@ -181,7 +183,7 @@ let pp_named_arg_ty ~unused ppf (arg_name, arg_ty) = let pp_define_fun ~is_constant pp ppf ((id, arg_tys, ret_ty), a) = let named_arg_tys = List.mapi (fun i arg_ty -> (i, arg_ty)) arg_tys in Fmt.pf ppf "(@[define-fun %a (%a) %a@ %a)@]" - Id.pp id + Uid.pp id Fmt.(list ~sep:sp (pp_named_arg_ty ~unused:is_constant)) named_arg_tys Ty.pp_smtlib ret_ty pp a diff --git a/src/lib/structures/modelMap.mli b/src/lib/structures/modelMap.mli index aa823bca1..de5a54ed4 100644 --- a/src/lib/structures/modelMap.mli +++ b/src/lib/structures/modelMap.mli @@ -19,16 +19,22 @@ type t (** Type of model. *) -val add : Id.typed -> Expr.t list -> Expr.t -> t -> t +type profile = Uid.term_cst * Ty.t list * Ty.t +(** Typed identifier of function. In order: + - The identifier. + - Types of its arguments. + - The returned type. *) + +val add : profile -> Expr.t list -> Expr.t -> t -> t (** [add sy args ret mdl] adds the binding [args -> ret] to the partial graph associated with the symbol [sy]. *) -val empty : suspicious:bool -> Id.typed list -> t +val empty : suspicious:bool -> profile list -> t (** An empty model. The [suspicious] flag is used to remember that this model may be wrong as it involves symbols from theories for which the model generation is known to be incomplete. *) -val subst : Id.t -> Expr.t -> t -> t +val subst : profile -> Expr.t -> t -> t (** [subst id e mdl] substitutes all the occurrences of the identifier [id] in the model [mdl] by the model term [e]. diff --git a/src/lib/structures/satml_types.ml b/src/lib/structures/satml_types.ml index be109c2de..418b48fa4 100644 --- a/src/lib/structures/satml_types.ml +++ b/src/lib/structures/satml_types.ml @@ -953,7 +953,10 @@ module Flat_Formula : FLAT_FORMULA = struct if is_neg then a.Atom.neg,l else a,l let mk_new_proxy n = - let sy = Symbols.name ~ns:Internal @@ "PROXY__" ^ string_of_int n in + let sy = + Symbols.name ~ns:Internal @@ Uid.of_string + @@ "PROXY__" ^ string_of_int n + in E.mk_term sy [] Ty.Tbool let get_proxy_of f proxies_mp = @@ -1020,7 +1023,10 @@ module Proxy_formula = struct if is_neg then a.Atom.neg,l else a,l let mk_new_proxy n = - let sy = Symbols.name ~ns:Internal @@ "PROXY__" ^ (string_of_int n) in + let sy = + Symbols.name ~ns:Internal @@ Uid.of_string + @@ "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) = diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index 902d33f94..fe610701f 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -25,6 +25,9 @@ (* *) (**************************************************************************) +module DE = Dolmen.Std.Expr +module DStd = Dolmen.Std + type builtin = LE | LT (* arithmetic *) | IsConstr of Uid.term_cst (* ADT tester *) @@ -77,6 +80,37 @@ type form = type name_kind = Ac | Other +module Namespace = struct + module type S = sig + val fresh : ?base:string -> unit -> string + end + + module Make () = struct + let fresh, reset_fresh_cpt = + let cpt = ref 0 in + let fresh_string ?(base = "") () = + 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 + end + + module Internal = Make () + + module Skolem = Make () + + module Abstract = Make () + + let reinit () = + Internal.reset_fresh_cpt (); + Skolem.reset_fresh_cpt (); + Abstract.reset_fresh_cpt () +end + type name_space = User | Internal | Fresh | Fresh_ac | Skolem | Abstract let compare_name_space ns1 ns2 = @@ -112,7 +146,7 @@ type t = | True | False | Name of - { hs : Id.t + { hs : Uid.term_cst ; kind : name_kind ; defined : bool ; ns : name_space } @@ -129,19 +163,21 @@ type t = let mangle ns s = match ns with - | User when String.length s > 0 && Char.equal '.' s.[0] -> ".." ^ s - | User when String.length s > 0 && Char.equal '@' s.[0] -> ".@" ^ s - | User -> s - | Internal -> ".!" ^ s - | Fresh -> ".k" ^ s - | Fresh_ac -> ".K" ^ s - | Skolem -> ".?__" ^ s - | Abstract -> "@a" ^ s + (* These two cases should not occur because Dolmen refuses these + identifiers since the version 0.10. *) + | User when String.length s > 0 && Char.equal '.' s.[0] -> Some (".." ^ s) + | User when String.length s > 0 && Char.equal '@' s.[0] -> Some (".@" ^ s) + | User -> None + | Internal -> Some (".!" ^ s) + | Fresh -> Some (".k" ^ s) + | Fresh_ac -> Some (".K" ^ s) + | Skolem -> Some (".?__" ^ s) + | Abstract -> Some ("@a" ^ s) (* NB: names are pre-mangled, which means that we don't need to take the namespace into consideration when hashing or comparing. *) -let name ?(kind=Other) ?(defined=false) ?(ns = User) s = - Name { hs = Hstring.make (mangle ns s) ; kind ; defined ; ns } +let name ?(kind=Other) ?(defined=false) ?(ns = User) id = + Name { hs = Uid.do_mangle (mangle ns) id ; kind ; defined ; ns } let var s = Var s let int i = Int (Z.of_string i) @@ -263,7 +299,7 @@ let compare s1 s2 = | Var v1, Var v2 | MapsTo v1, MapsTo v2 -> Var.compare v1 v2 | Name { ns = ns1; hs = h1; kind = k1; _ }, Name { ns = ns2; hs = h2; kind = k2; _ } -> - let c = Hstring.compare h1 h2 in + let c = Uid.compare h1 h2 in if c <> 0 then c else let c = compare_kinds k1 k2 in if c <> 0 then c else compare_name_space ns1 ns2 @@ -293,8 +329,8 @@ let hash x = | Bitv (n, s) -> 19 * (Hashtbl.hash n + Hashtbl.hash s) + 3 | In (b1, b2) -> 19 * (Hashtbl.hash b1 + Hashtbl.hash b2) + 4 (* NB: No need to hash the namespace because names are pre-mangled *) - | Name { hs = n; kind = Ac; _ } -> 19 * Hstring.hash n + 5 - | Name { hs = n; kind = Other; _ } -> 19 * Hstring.hash n + 6 + | Name { hs = n; kind = Ac; _ } -> 19 * Uid.hash n + 5 + | Name { hs = n; kind = Other; _ } -> 19 * Uid.hash n + 6 | Int z -> 19 * Z.hash z + 7 | Real n -> 19 * Hashtbl.hash n + 7 | Var v -> 19 * Var.hash v + 8 @@ -317,10 +353,6 @@ let string_of_bound b = let print_bound fmt b = Format.fprintf fmt "%s" (string_of_bound b) -let pp_name ppf (_ns, s) = - (* Names are pre-mangled *) - Dolmen.Smtlib2.Script.Poly.Print.id ppf (Dolmen.Std.Name.simple s) - module AEPrinter = struct let pp_operator ppf op = match op with @@ -425,7 +457,7 @@ module AEPrinter = struct (* Core theory *) | True -> Fmt.pf ppf "true" | False -> Fmt.pf ppf "false" - | Name { ns; hs; _ } -> pp_name ppf (ns, Hstring.view hs) + | Name { hs; _ } -> Uid.pp ppf hs | Var v when show_vars -> Fmt.pf ppf "'%s'" (Var.to_string v) | Var v -> Fmt.string ppf (Var.to_string v) @@ -524,8 +556,10 @@ let to_string_clean sy = let to_string sy = Fmt.str "%a" (AEPrinter.pp ~show_vars:true) sy -let fresh_skolem_string base = Id.Namespace.Skolem.fresh ~base () -let fresh_skolem_name base = name ~ns:Skolem (fresh_skolem_string base) +let fresh_skolem_string base = Namespace.Skolem.fresh ~base () +let fresh_skolem_name base = + name ~ns:Skolem @@ Uid.of_string @@ fresh_skolem_string base + let fresh_skolem_var base = Var.of_string (fresh_skolem_string base) let is_get f = equal f (Op Get) diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli index 145e72bc1..44b4599fd 100644 --- a/src/lib/structures/symbols.mli +++ b/src/lib/structures/symbols.mli @@ -150,7 +150,7 @@ type t = | True | False | Name of - { hs : Id.t + { hs : Uid.term_cst (** Note: [hs] is prefixed according to [ns]. *) ; kind : name_kind ; defined : bool @@ -166,6 +166,20 @@ type t = | MapsTo of Var.t | Let +module Namespace : sig + module type S = sig + val fresh : ?base:string -> unit -> string + end + + module Internal : S + module Skolem : S + module Abstract : S + + val reinit : unit -> unit + (** Resets the [fresh_internal_name], [fresh_skolem] and [fresh_abstract] + counters. *) +end + (** Create a new symbol with the given name. By default, names are created in the [User] name space. @@ -174,7 +188,8 @@ type t = not be exactly the name that was passed to this function (however, calling `name` with the same string but two different name spaces is guaranteed to return two [Name]s with distinct [hs] fields). *) -val name : ?kind:name_kind -> ?defined:bool -> ?ns:name_space -> string -> t +val name : + ?kind:name_kind -> ?defined:bool -> ?ns:name_space -> Uid.term_cst -> t val var : Var.t -> t val int : string -> t @@ -205,8 +220,6 @@ val print : t Fmt.t val to_string_clean : t -> string val print_clean : t Fmt.t -val pp_name : (name_space * string) Fmt.t - val pp_ae_operator : operator Fmt.t (* [pp_ae_operator ppf op] prints the operator symbol [op] on the formatter [ppf] using the Alt-Ergo native format. *) diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml index 8daf7a735..e7ddc4d61 100644 --- a/src/lib/structures/ty.ml +++ b/src/lib/structures/ty.ml @@ -729,3 +729,5 @@ let is_global_hyp s = (* Context reinitialization *) let reinit_decls () = Decls.reinit () + +let id = Compat.Type.Id.make () diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli index 688662695..f4bed817c 100644 --- a/src/lib/structures/ty.mli +++ b/src/lib/structures/ty.mli @@ -88,6 +88,8 @@ and trecord = { } (** Record types. *) +val id : t Compat.Type.Id.t + type adt_constr = { constr : Uid.term_cst ; (** constructor of an ADT type *) @@ -272,7 +274,7 @@ val monomorphize: t -> t type goal_sort = | Cut (** Introduce a cut in a goal. Once the cut proved, - it's added as a hypothesis. *) + it is added as a hypothesis. *) | Check (** Check if some intermediate assertion is prouvable *) | Thm diff --git a/src/lib/structures/uid.ml b/src/lib/structures/uid.ml index 66d877467..28a6aa3c0 100644 --- a/src/lib/structures/uid.ml +++ b/src/lib/structures/uid.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2022-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -27,6 +27,8 @@ module DStd = Dolmen.Std module DE = Dolmen.Std.Expr +module DT = DE.Ty +module B = DStd.Builtin type _ t = | Hstring : Hstring.t -> 'a t @@ -38,6 +40,29 @@ type term_cst = DE.term_cst t type ty_cst = DE.ty_cst t type ty_var = DE.ty_var t +let (let*) = Option.bind + +let rename_path f (path : DStd.Path.t) = + match path with + | Local { name; } -> + let* n = f name in + Some (DStd.Path.local n) + | Absolute { path; name; } -> + let* n = f name in + Some (DStd.Path.absolute path n) + +let do_mangle mangler (id : term_cst) = + match id with + | Hstring hs -> + let* s = mangler @@ Hstring.view hs in + Some (Hstring (Hstring.make s)) + | Term_cst { id_ty; path; builtin; tags; _ } -> + let* p = rename_path mangler path in + Some (Term_cst (DE.Id.mk ~builtin ~tags p id_ty)) + +let do_mangle mangler id = + Option.value (do_mangle mangler id) ~default:id + let order_tag : int DStd.Tag.t = DStd.Tag.create () let has_order_if_constr id = @@ -71,10 +96,21 @@ let hash (type a) (u : a t) = | Ty_cst id -> DE.Id.hash id | Ty_var id -> DE.Id.hash id +let pp_name ppf (_ns, s) = + (* Names are pre-mangled *) + Dolmen.Smtlib2.Script.Poly.Print.id ppf (Dolmen.Std.Name.simple s) + +let pp_quoted_id ppf DE.{ path; _ } = + let (Absolute { name; _ } | Local { name }) = path in + Dolmen.Smtlib2.Script.Poly.Print.id ppf @@ DStd.Name.simple name + +let pp_quoted_hstring ppf hs = + Dolmen.Smtlib2.Script.Poly.Print.id ppf @@ DStd.Name.simple @@ Hstring.view hs + let pp (type a) ppf (u : a t) = match u with - | Hstring hs -> Hstring.print ppf hs - | Term_cst id -> DE.Id.print ppf id + | Hstring hs -> pp_quoted_hstring ppf hs + | Term_cst id -> pp_quoted_id ppf id | Ty_cst id -> DE.Id.print ppf id | Ty_var id -> DE.Id.print ppf id @@ -98,12 +134,18 @@ let compare (type a b) (u1 : a t) (u2 : b t) = module Term_set = Set.Make (struct - type nonrec t = term_cst + type t = term_cst + let compare = compare + end) + +module Term_map = Map.Make + (struct + type t = term_cst let compare = compare end) module Ty_map = Map.Make (struct - type nonrec t = ty_cst + type t = ty_cst let compare = compare end) diff --git a/src/lib/structures/uid.mli b/src/lib/structures/uid.mli index 866357b3a..7ff4b3e66 100644 --- a/src/lib/structures/uid.mli +++ b/src/lib/structures/uid.mli @@ -49,8 +49,11 @@ val show : 'a t -> string val equal : 'a t -> 'a t -> bool val compare : 'a t -> 'a t -> int +val do_mangle : (string -> string option) -> term_cst -> term_cst + val order_tag : int Dolmen.Std.Tag.t (** Tag used to attach the order of constructor. *) module Term_set : Set.S with type elt = term_cst +module Term_map : Map.S with type key = term_cst module Ty_map : Map.S with type key = ty_cst diff --git a/tests/issues/854/function.models.expected b/tests/issues/854/function.models.expected index 63577badc..4969adb77 100644 --- a/tests/issues/854/function.models.expected +++ b/tests/issues/854/function.models.expected @@ -1,8 +1,8 @@ unknown ( + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a5 intref)) (define-fun a () Int 0) - (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref)) (define-fun f ((_arg_0 Int)) Int 0) (define-fun a1 () Int 0) ) diff --git a/tests/issues/854/original.models.expected b/tests/issues/854/original.models.expected index a0ce9f571..7d40ab42e 100644 --- a/tests/issues/854/original.models.expected +++ b/tests/issues/854/original.models.expected @@ -1,7 +1,7 @@ unknown ( - (define-fun a () Int 0) (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a3 intref)) + (define-fun a () Int 0) (define-fun a1 () Int 0) ) diff --git a/tests/issues/854/twice_eq.models.expected b/tests/issues/854/twice_eq.models.expected index 3488c940f..ee4c1de0d 100644 --- a/tests/issues/854/twice_eq.models.expected +++ b/tests/issues/854/twice_eq.models.expected @@ -1,8 +1,8 @@ unknown ( - (define-fun a () Int 0) (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref)) (define-fun another_mk ((_arg_0 Int)) intref (as @a4 intref)) + (define-fun a () Int 0) (define-fun a1 () Int 0) ) diff --git a/tests/models/adt/arith.models.expected b/tests/models/adt/arith.models.expected index 18e539f31..7da79872d 100644 --- a/tests/models/adt/arith.models.expected +++ b/tests/models/adt/arith.models.expected @@ -1,8 +1,8 @@ unknown ( - (define-fun x () Real 2.0) - (define-fun y () Real 0.0) (define-fun a () Data (cons1 2.0 0.0)) (define-fun b () Data (cons3 0.0)) + (define-fun x () Real 2.0) + (define-fun y () Real 0.0) ) diff --git a/tests/models/arith/arith11.dolmen.expected b/tests/models/arith/arith11.dolmen.expected index 216672887..35ae71285 100644 --- a/tests/models/arith/arith11.dolmen.expected +++ b/tests/models/arith/arith11.dolmen.expected @@ -1,10 +1,10 @@ unknown ( - (define-fun x () Real 2.0) - (define-fun y () Real (as @a0 Real)) (define-fun p1 () Bool false) (define-fun p2 () Bool true) + (define-fun x () Real 2.0) + (define-fun y () Real (as @a0 Real)) ) (objectives (x 2.0) diff --git a/tests/models/array/embedded-array.models.expected b/tests/models/array/embedded-array.models.expected index 0cb5c3d3e..9ce0ca17d 100644 --- a/tests/models/array/embedded-array.models.expected +++ b/tests/models/array/embedded-array.models.expected @@ -1,8 +1,8 @@ unknown ( + (define-fun s () S (as @a9 S)) (define-fun x () Pair - (pair (store (as @a3 (Array Int S)) 0 s) - (store (as @a3 (Array Int S)) 0 s))) - (define-fun s () S (as @a2 S)) + (pair (store (as @a10 (Array Int S)) 0 s) + (store (as @a10 (Array Int S)) 0 s))) ) diff --git a/tests/models/bool/bool1.models.expected b/tests/models/bool/bool1.models.expected index 1eb3e25e7..3a2ce307f 100644 --- a/tests/models/bool/bool1.models.expected +++ b/tests/models/bool/bool1.models.expected @@ -4,8 +4,8 @@ unknown (define-fun p () Bool true) (define-fun q () Bool true) ) -((notp false) - (notnq false)) +((notnq false) + (notp false)) unknown @@ -13,6 +13,6 @@ unknown (define-fun p () Bool true) (define-fun q () Bool true) ) -((notp false) - (notnq false)) +((notnq false) + (notp false)) diff --git a/tests/models/bool/bool3.models.expected b/tests/models/bool/bool3.models.expected index 341a2df7e..ed7a9b1e2 100644 --- a/tests/models/bool/bool3.models.expected +++ b/tests/models/bool/bool3.models.expected @@ -4,6 +4,6 @@ unknown (define-fun x () Bool true) (define-fun y () Bool true) ) -((foo true) - (bar false)) +((bar false) + (foo true)) diff --git a/tests/models/complete_3.models.expected b/tests/models/complete_3.models.expected index d507e21ca..30de4692b 100644 --- a/tests/models/complete_3.models.expected +++ b/tests/models/complete_3.models.expected @@ -1,5 +1,5 @@ unknown ( - (define-fun x () Int (as @a0 Int)) + (define-fun x () Int (as @a1 Int)) ) diff --git a/tests/models/records/record3.models.expected b/tests/models/records/record3.models.expected index 8b2d9f83a..b478bf755 100644 --- a/tests/models/records/record3.models.expected +++ b/tests/models/records/record3.models.expected @@ -1,7 +1,7 @@ unknown ( + (define-fun f ((_arg_0 Int)) Pair (pair 5 0)) (define-fun x () Int 0) (define-fun y () Int 5) - (define-fun f ((_arg_0 Int)) Pair (pair 5 0)) ) diff --git a/tests/models/uf/uf1.models.expected b/tests/models/uf/uf1.models.expected index d3b170c21..2891baf56 100644 --- a/tests/models/uf/uf1.models.expected +++ b/tests/models/uf/uf1.models.expected @@ -1,7 +1,7 @@ unknown ( + (define-fun f ((_arg_0 Int)) Int 0) (define-fun a () Int 0) (define-fun b () Int 0) - (define-fun f ((_arg_0 Int)) Int 0) ) diff --git a/tests/models/uf/uf2.models.expected b/tests/models/uf/uf2.models.expected index 232c59a45..faa7fb056 100644 --- a/tests/models/uf/uf2.models.expected +++ b/tests/models/uf/uf2.models.expected @@ -1,7 +1,7 @@ unknown ( + (define-fun f ((arg_0 Int)) Int (ite (= arg_0 0) 1 0)) (define-fun a () Int 0) (define-fun b () Int (- 1)) - (define-fun f ((arg_0 Int)) Int (ite (= arg_0 0) 1 0)) )