From 49f0318da31a1594d135be428e12774eea9f1f6b Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 29 Aug 2024 22:42:04 +0200 Subject: [PATCH] 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 | 22 ++---- src/lib/dune | 2 +- src/lib/frontend/d_cnf.ml | 23 +++--- src/lib/frontend/frontend.ml | 3 +- src/lib/frontend/models.ml | 12 +-- src/lib/frontend/typechecker.ml | 16 ++-- src/lib/reasoners/ac.ml | 6 +- src/lib/reasoners/arith.ml | 14 +++- src/lib/reasoners/ccx.ml | 6 +- src/lib/reasoners/ccx.mli | 2 +- src/lib/reasoners/fun_sat.ml | 6 +- src/lib/reasoners/fun_sat.mli | 2 +- src/lib/reasoners/instances.ml | 4 +- src/lib/reasoners/sat_solver_sig.ml | 4 +- src/lib/reasoners/sat_solver_sig.mli | 4 +- src/lib/reasoners/satml.ml | 2 +- src/lib/reasoners/satml.mli | 2 +- src/lib/reasoners/satml_frontend.ml | 8 +- src/lib/reasoners/theory.ml | 14 ++-- src/lib/reasoners/theory.mli | 2 +- src/lib/reasoners/uf.ml | 14 ++-- src/lib/reasoners/uf.mli | 2 +- src/lib/reasoners/use.ml | 5 +- src/lib/structures/commands.ml | 8 +- src/lib/structures/commands.mli | 2 +- src/lib/structures/errors.ml | 4 +- src/lib/structures/errors.mli | 2 +- src/lib/structures/expr.ml | 23 ++++-- src/lib/structures/id.ml | 60 --------------- src/lib/structures/id.mli | 44 ----------- src/lib/structures/modelMap.ml | 24 +++--- src/lib/structures/modelMap.mli | 12 ++- src/lib/structures/satml_types.ml | 10 ++- src/lib/structures/symbols.ml | 76 ++++++++++++++----- src/lib/structures/symbols.mli | 21 ++++- src/lib/structures/ty.ml | 2 + src/lib/structures/ty.mli | 4 +- src/lib/structures/uid.ml | 52 +++++++++++-- src/lib/structures/uid.mli | 3 + tests/issues/854/function.models.expected | 2 +- tests/issues/854/original.models.expected | 2 +- tests/issues/854/twice_eq.models.expected | 2 +- tests/models/adt/arith.models.expected | 4 +- tests/models/arith/arith11.dolmen.expected | 4 +- .../array/embedded-array.models.expected | 6 +- tests/models/bool/bool1.models.expected | 8 +- tests/models/bool/bool3.models.expected | 4 +- tests/models/complete_3.models.expected | 2 +- tests/models/records/record3.models.expected | 2 +- tests/models/uf/uf1.models.expected | 2 +- tests/models/uf/uf2.models.expected | 2 +- 51 files changed, 293 insertions(+), 269 deletions(-) delete mode 100644 src/lib/structures/id.ml delete mode 100644 src/lib/structures/id.mli 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)) )