From 8150259a463561ad1e49d0d4eabd5464bf85bafd Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 29 Jan 2025 15:13:57 +0100 Subject: [PATCH 1/2] Use constant terms as identifiers in names and variables This PR changes the way we construct identifiers for names (in Symbols) and variables (in Var). We plan to completely replace the AE identifiers with identifiers from Dolmen. This PR serves as an intermediate step from string-based identifiers to Dolmen identifiers. - All the identifiers are now managed in the Id module. - Constant terms are used for declared or defined identifiers in the input file. - Internal identifiers are still pre-mangled strings. Replacing them with Dolmen identifiers requires careful investigation, particularly in the AC(X) implementation. - I haven't removed Id.typed yet. After this PR, the user identifiers will be typed, so we do not need to store them separately. If we use the internal type of the identifier, we will need to implement a conversion function from Dolmen type to Alt-Ergo type, which is not trivial. I prefer keeping this type and remove it after transitioning from Alt-Ergo types to Dolmen types. - The new API of Id prevents us from creating duplicate fresh/fresh_ac/abstract identifiers. - I still check that user identifiers do not start with . or @. In Before this PR, we mangled the identifier if it happened. In this PR, we crash. I don't have a strong opinion on this behavior, it was just simpler to implement this way. - I use identifiers for term variables too. I preserved the internal representation because: 1. The notion of local variables is AE-specific, whereas the local name in Dolmen identifiers is a distinct concept. 2. After this PR, variables are typed but what is the type of Underscore? May be forall a. a? This PR have been tested on ae-format (+2-2). --- src/bin/common/solving_loop.ml | 22 +-- src/lib/frontend/models.ml | 9 +- src/lib/frontend/translate.ml | 74 +++------ src/lib/reasoners/ac.ml | 8 +- src/lib/reasoners/arith.ml | 15 +- src/lib/reasoners/ccx.ml | 4 +- src/lib/reasoners/fun_sat.ml | 4 +- src/lib/reasoners/instances.ml | 10 +- src/lib/reasoners/intervalCalculus.ml | 4 +- src/lib/reasoners/satml_frontend.ml | 6 +- src/lib/reasoners/theory.ml | 18 +- src/lib/reasoners/uf.ml | 43 +++-- src/lib/reasoners/use.ml | 5 +- src/lib/structures/commands.ml | 4 +- src/lib/structures/expr.ml | 35 ++-- src/lib/structures/id.ml | 154 ++++++++++++++---- src/lib/structures/id.mli | 122 ++++++++++++-- src/lib/structures/modelMap.ml | 6 +- src/lib/structures/modelMap.mli | 10 +- src/lib/structures/satml_types.ml | 10 +- src/lib/structures/symbols.ml | 86 +++------- src/lib/structures/symbols.mli | 93 +---------- src/lib/structures/var.ml | 83 +++++----- src/lib/structures/var.mli | 36 ++-- src/lib/util/util.ml | 26 +++ src/lib/util/util.mli | 9 + tests/issues/854/function.default.expected | 2 +- tests/issues/854/original.default.expected | 2 +- tests/issues/854/twice_eq.default.expected | 2 +- tests/models/adt/arith.default.expected | 4 +- tests/models/arith/arith11.default.expected | 4 +- .../array/embedded-array.default.expected | 2 +- tests/models/bool/bool1.default.expected | 8 +- tests/models/bool/bool3.default.expected | 4 +- tests/models/records/record3.default.expected | 2 +- tests/models/uf/uf1.default.expected | 2 +- tests/models/uf/uf2.default.expected | 2 +- 37 files changed, 503 insertions(+), 427 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index a35411d7bd..1dd0fb46ed 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -32,6 +32,8 @@ module DO = D_state_option module Sy = Symbols module O = Options +module ConstSet = Map.Make (Dolmen.Std.Expr.Term.Const) + exception Exit_with_code of int type solver_ctx = { @@ -103,14 +105,14 @@ let cmd_on_modes st modes cmd = (** Adds the named terms of the statement [stmt] to the map accumulator [acc] *) let add_if_named - ~(acc : DStd.Expr.term Util.MS.t) + ~(acc : DStd.Expr.term ConstSet.t) (stmt : Typer_Pipe.typechecked D_loop.Typer_Pipe.stmt) = match stmt.contents with - | `Defs [`Term_def ({name = Simple n; _}, id, _, _, t)] -> + | `Defs [`Term_def (_, id, _, _, t)] -> begin match DStd.Expr.Id.get_tag id DStd.Expr.Tags.named with | None -> acc - | Some _ -> Util.MS.add n t acc + | Some _ -> ConstSet.add id t acc end | _ -> (* Named terms are expected to be definitions with simple names. *) @@ -212,7 +214,7 @@ let process_source ?selector_inst ~print_status src = State.create_key ~pipe:"" "sat_state" in - let named_terms: DStd.Expr.term Util.MS.t State.key = + let named_terms: DStd.Expr.term ConstSet.t State.key = State.create_key ~pipe:"" "named_terms" in @@ -357,7 +359,7 @@ let process_source ?selector_inst ~print_status src = State.empty |> State.set solver_ctx_key solver_ctx |> State.set partial_model_key None - |> State.set named_terms Util.MS.empty + |> State.set named_terms ConstSet.empty |> DO.init |> State.init ~debug ~report_style ~reports ~max_warn ~time_limit ~size_limit ~response_file @@ -633,14 +635,14 @@ let process_source ?selector_inst ~print_status src = in (* Fetches the term value in the current model. *) - let evaluate_term get_value name term = + let evaluate_term get_value tcst term = (* There are two ways to evaluate a term: - if its name is registered in the environment, get its value; - if not, check if the formula is in the environment. *) let simple_form = Expr.mk_term - (Sy.name name) + (Sy.name @@ Id.of_term_cst ~defined:true tcst) [] (Translate.dty_to_ty term.DStd.Expr.term_ty) in @@ -652,12 +654,12 @@ let process_source ?selector_inst ~print_status src = let print_terms_assignments = Fmt.list ~sep:Fmt.cut - (fun fmt (name, v) -> Fmt.pf fmt "(%s %s)" name v) + (fun fmt (name, v) -> Fmt.pf fmt "(%a %s)" Util.pp_term_cst name v) in let handle_get_assignment ~get_value st = let assignments = - Util.MS.fold + ConstSet.fold (fun name term acc -> if DStd.Expr.Ty.equal term.DStd.Expr.term_ty DStd.Expr.Ty.bool then (name, evaluate_term get_value name term) :: acc @@ -789,7 +791,7 @@ let process_source ?selector_inst ~print_status src = |> DO.StrictMode.clear |> DO.ProduceAssignment.clear |> DO.init - |> State.set named_terms Util.MS.empty + |> State.set named_terms ConstSet.empty | {contents = `Exit; _} -> raise Exit diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml index afa71e83d2..fc2be74b56 100644 --- a/src/lib/frontend/models.ml +++ b/src/lib/frontend/models.ml @@ -194,14 +194,15 @@ module Pp_smtlib_term = struct | Sy.In(lb, rb), [t] -> fprintf fmt "(%a in %a, %a)" print t Sy.print_bound lb Sy.print_bound rb - | Sy.Name { hs = n; _ }, l -> begin + | Sy.Name { id; _ }, l -> begin let constraint_name = + let s = Id.show id in try let constraint_name,_,_ = - (MS.find (Hstring.view n) !constraints) in + (MS.find s !constraints) in constraint_name with _ -> - let constraint_name = "c_"^(Hstring.view n) in - constraints := MS.add (Hstring.view n) + let constraint_name = "c_" ^ s in + constraints := MS.add s (constraint_name, to_string_type (E.type_info t), List.map (fun e -> to_string_type (E.type_info e)) l diff --git a/src/lib/frontend/translate.ml b/src/lib/frontend/translate.ml index 0b3f5c8038..71fc7787a8 100644 --- a/src/lib/frontend/translate.ml +++ b/src/lib/frontend/translate.ml @@ -45,23 +45,6 @@ module HT = let hash (Id i)= DE.Id.hash i end) -(** Helper function: returns the basename of a dolmen path, since in AE - the problems are contained in one-file (for now at least), the path is - irrelevant and only the basename matters *) -let get_basename = function - | DStd.Path.Local { name; } - | Absolute { name; path = []; } -> name - | Absolute { name; path; } -> - Fmt.failwith - "Expected an empty path to the basename: \"%s\" but got: [%a]." - name (fun fmt l -> - match l with - | h :: t -> - Format.fprintf fmt "%s" h; - List.iter (Format.fprintf fmt "; %s") t - | _ -> () - ) path - module Cache = struct let ae_sy_ht: Sy.t HT.t = HT.create 100 @@ -124,8 +107,9 @@ module Cache = struct let store_sy_vl_names (tvl: DE.term_var list) = List.iter ( fun ({ DE.path; _ } as tv) -> - let name = get_basename path in - store_sy tv (Sy.name name) + let name = Util.get_basename path in + (* TODO : Check this line! *) + store_sy tv (Sy.name @@ Id.of_string ~ns:Internal name) ) tvl let store_ty_vars ?(is_var = true) ty = @@ -176,7 +160,7 @@ let builtin_term t = Dl.Typer.T.builtin_term t let builtin_ty t = Dl.Typer.T.builtin_ty t let ty (ty_cst : DE.ty_cst) ty = - let name = get_basename ty_cst.path in + let name = Util.get_basename ty_cst.path in DStd.Id.Map.add { name = DStd.Name.simple name; ns = Sort } @@ fun env s -> builtin_ty @@ @@ -188,7 +172,7 @@ let fpa_rounding_mode, rounding_modes, add_rounding_modes = let constrs = Fpa_rounding.d_constrs in let add_constrs map = List.fold_left (fun map (c : DE.term_cst) -> - let name = get_basename c.path in + let name = Util.get_basename c.path in DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term } (fun env _ -> builtin_term @@ @@ -629,12 +613,12 @@ let mk_ty_decl (ty_c: DE.ty_cst) = (** Handles term declaration by storing the eventual present type variables in the cache as well as the symbol associated to the term. *) -let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) = - let name = get_basename path in +let mk_term_decl ({ id_ty; tags; _ } as tcst: DE.term_cst) = let sy = + let id = Id.of_term_cst tcst in begin match DStd.Tag.get tags DE.Tags.ac with - | Some () -> Sy.name ~kind:Sy.Ac name - | _ -> Sy.name name + | Some () -> Sy.name ~kind:Sy.Ac id + | _ -> Sy.name id end in Cache.store_sy tcst sy; @@ -646,7 +630,7 @@ let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) = List.map dty_to_ty arg_tys, dty_to_ty ret_ty | _ -> [], dty_to_ty id_ty in - (Hstring.make name, arg_tys, ret_ty) + (tcst, arg_tys, ret_ty) (** Handles the definitions of a list of mutually recursive types. - If one of the types is an ADT, the ADTs that have only one case are @@ -744,15 +728,15 @@ let handle_patt_var id (DE.{ term_descr; _ } as term) = match term_descr with | Cst ({ builtin = B.Base; id_ty; _ } as ty_c) -> let ty = dty_to_ty id_ty in - let v = Var.of_string @@ Fmt.to_to_string DE.Term.Const.print id in - let sy = Sy.Var v in + let v = Var.of_id @@ Id.of_term_cst ty_c in + let sy = Sy.var v in Cache.store_sy ty_c sy; v, id, ty | Var ({ builtin = B.Base; id_ty; _ } as ty_v) -> let ty = dty_to_ty id_ty in - let v = Var.of_string @@ Fmt.to_to_string DE.Term.Const.print id in - let sy = Sy.Var v in + let v = Var.of_id @@ Id.of_term_cst ty_v in + let sy = Sy.var v in Cache.store_sy ty_v sy; v, id, ty @@ -815,10 +799,10 @@ end = struct | Cst ({ builtin = B.Constructor _; _ } as cst) -> Constr (cst, []) - | Var ({ builtin = B.Base; path; _ } as t_v) -> + | Var ({ builtin = B.Base; _ } as t_v) -> (* Should the type be passed as an argument instead of re-evaluating it here? *) - let v = Var.of_string (get_basename path) in + let v = Var.of_id @@ Id.of_term_cst t_v in let sy = Sy.var v in Cache.store_sy t_v sy; (* Adding the matched variable to the store *) @@ -1439,9 +1423,8 @@ let rec mk_expr | Binder ((Let_par ls | Let_seq ls) as let_binder, body) -> let lsbis = List.map ( - fun ({ DE.path; _ } as tv, t) -> - let name = get_basename path in - let v = Var.of_string name in + fun (tv, t) -> + let v = Var.of_id @@ Id.of_term_cst tv in Cache.store_sy tv (Sy.var v); v, t ) ls @@ -1485,9 +1468,9 @@ let rec mk_expr (* the following is done in two iterations to preserve the order *) (* quantified variables *) let ntvl = List.rev_map ( - fun (DE.{ path; id_ty; _ } as t_v) -> + fun (DE.{ id_ty; _ } as t_v) -> dty_to_ty id_ty, - Var.of_string (get_basename path), + Var.of_id @@ Id.of_term_cst t_v, t_v ) tvl in @@ -1631,11 +1614,7 @@ and make_trigger ?(loc = Loc.dummy) ~name_base ~decl_kind | { DE.term_descr = Binder (Exists (_, qm_vars), e); _ } -> List.iter (fun (v : DE.term_var) -> - let var = - match v.path with - | Local { name } -> Var.local name - | _ -> assert false - in + let var = Var.local @@ Id.of_term_cst v in Cache.store_var v var) qm_vars; e @@ -1950,9 +1929,8 @@ let make dloc_file acc stmt = names in a row. *) List.iter (fun (def : Typer_Pipe.def) -> match def with - | `Term_def (_, ({ path; _ } as tcst), _, _, _) -> - let name_base = get_basename path in - let sy = Sy.name ~defined:true name_base in + | `Term_def (_, tcst, _, _, _) -> + let sy = Sy.name @@ Id.of_term_cst ~defined:true tcst in Cache.store_sy tcst sy | `Type_alias _ -> () | `Instanceof _ -> @@ -1968,15 +1946,15 @@ let make dloc_file acc stmt = | `Term_def ( _, ({ path; tags; _ } as tcst), tyvars, terml, body) -> Cache.store_tyvl tyvars; let st_loc = dl_to_ael dloc_file loc in - let name_base = get_basename path in + let name_base = Util.get_basename path in let binders, defn = let rty = dty_to_ty body.term_ty in let binders, rev_args = List.fold_left ( - fun (binders, acc) (DE.{ path; id_ty; _ } as tv) -> + fun (binders, acc) (DE.{ id_ty; _ } as tv) -> let ty = dty_to_ty id_ty in - let v = Var.of_string (get_basename path) in + let v = Var.of_id @@ Id.of_term_cst tv in let sy = Sy.var v in Cache.store_sy tv sy; let e = E.mk_term sy [] ty in diff --git a/src/lib/reasoners/ac.ml b/src/lib/reasoners/ac.ml index bedf316845..d21e28d35c 100644 --- a/src/lib/reasoners/ac.ml +++ b/src/lib/reasoners/ac.ml @@ -202,17 +202,19 @@ module Make (X : Sig.X) = struct let abstract2 sy t r acc = if List.exists (is_other_ac_symbol sy) (X.leaves r) then match X.ac_extract r, Expr.term_view t with - | Some ac, { f = Name { hs; kind = Ac; _ } ; xs; ty; _ } -> + | Some ac, { f = Name { id; kind = Ac; _ } ; xs; ty; _ } -> (* It should have been abstracted when building [r] *) assert (not (Sy.equal sy ac.h)); - let aro_sy = Sy.name ~ns:Internal ("@" ^ (HS.view hs)) in + let aro_sy = + Sy.name @@ Id.of_string ~ns:Internal ("@" ^ (Id.show id)) + in let aro_t = Expr.mk_term aro_sy xs ty in let eq = Expr.mk_eq ~iff:false aro_t t in X.term_embed aro_t, eq::acc | Some ac, { f = Op Mult; xs; ty; _ } -> (* It should have been abstracted when building [r] *) assert (not (Sy.equal sy ac.h)); - let aro_sy = Sy.name ~ns:Internal "@*" in + let aro_sy = Sy.name @@ Id.of_string ~ns:Internal "@*" in let aro_t = Expr.mk_term aro_sy xs ty in let eq = Expr.mk_eq ~iff:false aro_t t in X.term_embed aro_t, eq::acc diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml index afc1b7ae91..a1dc21a2dd 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 @@ Id.of_string ~ns:Internal "@mod" let calc_power (c : Q.t) (d : Q.t) (ty : Ty.t) = (* d must be integral and if we work on integer exponentation, @@ -246,7 +246,8 @@ module Shostak then (* becomes uninterpreted *) let tau = - E.mk_term (Sy.name ~kind:Sy.Ac ~ns:Internal "@*") [t1; t2] ty + let sy = Sy.name ~kind:Sy.Ac @@ Id.of_string ~ns:Internal "@*" in + E.mk_term sy [t1; t2] ty in let xtau, ctx' = X.make tau in P.add p (P.create [coef, xtau] Q.zero ty), List.rev_append ctx' ctx @@ -260,7 +261,10 @@ module Shostak (P.is_const p2 == None || (ty == Ty.Tint && P.is_const p1 == None)) then (* becomes uninterpreted *) - let tau = E.mk_term (Sy.name ~ns:Internal "@/") [t1; t2] ty in + let tau = + let sy = Sy.name @@ Id.of_string ~ns:Internal "@/" in + E.mk_term sy [t1; t2] ty + in let xtau, ctx' = X.make tau in P.add p (P.create [coef, xtau] Q.zero ty), List.rev_append ctx' ctx else @@ -287,7 +291,10 @@ module Shostak (P.is_const p1 == None || P.is_const p2 == None) then (* becomes uninterpreted *) - let tau = E.mk_term (Sy.name ~ns:Internal "@%") [t1; t2] ty in + let tau = + let sy = Sy.name @@ Id.of_string ~ns:Internal "@%" in + E.mk_term sy [t1; t2] ty + in let xtau, ctx' = X.make tau in P.add p (P.create [coef, xtau] Q.zero ty), List.rev_append ctx' ctx else diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml index 5d9f56787c..4b4bac58d4 100644 --- a/src/lib/reasoners/ccx.ml +++ b/src/lib/reasoners/ccx.ml @@ -249,7 +249,9 @@ module Main : S = struct end (*BISECT-IGNORE-END*) - let one, _ = X.make (Expr.mk_term (Sy.name ~ns:Internal "@bottom") [] Ty.Tint) + let one, _ = + let sy = Sy.name @@ Id.of_string ~ns:Internal "@bottom" in + X.make (Expr.mk_term sy [] Ty.Tint) let concat_leaves uf l = let concat_rec acc t = diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 347ef6cc48..5480e2d498 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -1875,8 +1875,7 @@ module Make (Th : Theory.S) = struct clear_instances_cache (); Th.reinit_cpt (); Symbols.clear_labels (); - Id.Namespace.reinit (); - Var.reinit_cnt (); + Id.reinit (); Satml_types.Flat_Formula.reinit_cpt (); Ty.reinit_decls (); IntervalCalculus.reinit_cache (); @@ -1888,7 +1887,6 @@ module Make (Th : Theory.S) = struct let () = Steps.save_steps (); - Var.save_cnt (); Expr.save_cache (); Hstring.save_cache (); Shostak.Combine.save_cache (); diff --git a/src/lib/reasoners/instances.ml b/src/lib/reasoners/instances.ml index 6f9f7af11d..280d3c7dab 100644 --- a/src/lib/reasoners/instances.ml +++ b/src/lib/reasoners/instances.ml @@ -168,8 +168,10 @@ module Make(X : Theory.S) : S with type tbox = X.t = struct let env = { env with 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 + | E.Iff (f1, f2) -> + let p = + E.mk_term (Symbols.name @@ Id.of_string ~ns:Internal name) [] Ty.Tbool + in let np = E.neg p in let defn = if E.equal f1 p then f2 @@ -179,7 +181,9 @@ 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 @@ Id.of_string ~ns:Internal 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/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml index 5e037b74ad..81d90fd544 100644 --- a/src/lib/reasoners/intervalCalculus.ml +++ b/src/lib/reasoners/intervalCalculus.ml @@ -2202,7 +2202,7 @@ let integrate_mapsTo_bindings sbs maps_to = ~function_name:"integrate_maps_to_bindings" "bad semantic trigger %a |-> %a@,\ left-hand side is not a constant!" - Var.print x E.print tx; + Var.pp x E.print tx; raise Exit | Some c -> let tc = mk_const_term (E.type_info t) c in @@ -2231,7 +2231,7 @@ let extend_with_domain_substitution = "[Error] %a <= %a <= %a@,\ Which value should we choose?" Q.print q1 - Var.print lb_var + Var.pp lb_var Q.print q2; assert (Q.compare q2 q1 >= 0); assert false diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index c0b448983c..94517019f6 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1393,9 +1393,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct | Ty.Tbool -> begin let bmodel = SAT.boolean_model env.satml in + let tlit = Shostak.Literal.make (LTerm t) in Compat.List.find_map (fun Atom.{lit; neg = {lit=neglit; _}; _} -> - let tlit = Shostak.Literal.make (LTerm t) in if Shostak.Literal.equal tlit lit then Some E.vrai else if Shostak.Literal.equal tlit neglit then @@ -1414,9 +1414,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let reinit_ctx () = Steps.reinit_steps (); Th.reinit_cpt (); - Id.Namespace.reinit (); + Id.reinit (); Symbols.clear_labels (); - Var.reinit_cnt (); Objective.Function.reinit_cnt (); Satml_types.Flat_Formula.reinit_cpt (); Ty.reinit_decls (); @@ -1429,7 +1428,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let () = Steps.save_steps (); - Var.save_cnt (); Expr.save_cache (); Hstring.save_cache (); Shostak.Combine.save_cache (); diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index ad9ad7962a..df1cb2a170 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -130,17 +130,17 @@ module Main_Default : S = struct | _ -> Ty.fresh_tvar () let logics_of_assumed st = - (* NB: using an [Hstring.Map] here depends on the fact that name mangling - is done pre-emptively in [Symbols.name] *) + (* NB: using an [Id.Map] here depends on the fact that name mangling + is done pre-emptively in [Id.of_string] or [Id.fresh]. *) SE.fold (fun t mp -> match E.term_view t with - | { E.f = Sy.Name { hs; kind = ((Sy.Ac | Sy.Other) as is_ac); _ }; + | { E.f = Sy.Name { id; kind = ((Sy.Ac | Sy.Other) as is_ac); _ }; xs; ty; _ } -> 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' = Id.Map.find id mp in assert (is_ac == is_ac'); let ty = generalize_types ty ty' in let xs = @@ -149,10 +149,10 @@ module Main_Default : S = struct xs, ty with Not_found -> xs, ty in - Hstring.Map.add hs (xs, ty, is_ac) mp + Id.Map.add id (xs, ty, is_ac) mp | _ -> mp - ) st Hstring.Map.empty + ) st Id.Map.empty module Ty_map = Map.Make (DE.Ty.Const) @@ -218,12 +218,12 @@ module Main_Default : S = struct let print_logics ?(header=true) logics = print_dbg ~header "@[(* logics: *)@ "; - Hstring.Map.iter + Id.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) + Id.pp hs print_arrow_type xs Ty.print ty )logics; diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index 0d94864e6b..afdc738b1b 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -1112,14 +1112,9 @@ module MED = Map.Make else Expr.compare a b end) -let is_suspicious_name hs = - match Hstring.view hs 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 { id; _ } when Id.is_suspicious id -> true | _ -> false let terms env = @@ -1127,8 +1122,8 @@ let terms env = (fun t r ((terms, suspicious) as acc) -> let Expr.{ f; _ } = Expr.term_view t in match f with - | Name { defined = true; _ } -> - (* We don't store names defined by the user. *) + | Name { id = Term_cst { defined = true; _ }; _ } -> + (* We do not store names defined by the user. *) acc | _ -> let suspicious = is_suspicious_symbol f || suspicious in @@ -1234,7 +1229,11 @@ let compute_concrete_model_of_val cache = acc end - | Sy.Name { hs = id; _ }, _, _ -> + | Sy.Name { id = Term_cst { tcst; defined }; _ }, _, _ + when not defined -> + (* XXX: Currently, all the declared constant term identifiers + are user-provided. This will change after adopting Dolmen + identifiers everywhere. *) let value = match ty with | Ty.Text _ -> @@ -1244,7 +1243,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 (tcst, arg_tys, ty) arg_vals value mdl), mrepr | _ -> Printer.print_err @@ -1273,24 +1272,24 @@ let extract_concrete_model cache = Expr.ArraysEx.store arr_val i v ) vals abstract in - let id, is_user = + let id, mdl = let Expr.{ f; _ } = Expr.term_view t in match f with - | Sy.Name { hs; ns = User; _ } -> hs, true - | Sy.Name { hs; _ } -> hs, false + | Sy.Name { id = Term_cst { tcst; defined } as id; _ } + when not defined -> + (* XXX: Currently, all the declared constant term identifiers + are user-provided. This will change after adopting Dolmen + identifiers everywhere. *) + id, ModelMap.add (tcst, [], ty) [] arr_val mdl + | Sy.Name { id; _ } -> + (* Internal identifiers can occur here if we need to generate + a model term for an embedded array but this array is not itself + declared by the user -- see the [embedded-array] test . *) + id, mdl | _ -> (* Excluded in [compute_concrete_model_of_val] *) assert false in - let mdl = - if is_user then - ModelMap.add (id, [], ty) [] 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 - declared by the user -- see the [embedded-array] test . *) - mdl - in (* We need to update the model [mdl] in order to substitute all the occurrences of the array identifier [id] by an appropriate model term. This cannot be performed while computing the model with diff --git a/src/lib/reasoners/use.ml b/src/lib/reasoners/use.ml index 1d6670acdd..65a52602f2 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 sy = Symbols.name @@ Id.of_string ~ns:Internal "@bottom" in + X.make (E.mk_term sy [] 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 45b8dcaf8b..20e2a9ef6e 100644 --- a/src/lib/structures/commands.ml +++ b/src/lib/structures/commands.ml @@ -46,9 +46,9 @@ type sat_tdecl = { } let print_aux fmt = function - | Decl (id, arg_tys, ret_ty) -> + | Decl (tcst, arg_tys, ret_ty) -> Fmt.pf fmt "declare %a with type (%a) -> %a" - Id.pp id + Util.pp_term_cst tcst Fmt.(list ~sep:comma Ty.print) arg_tys Ty.print ret_ty diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 43f4264d57..1d3d8e3bec 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -331,7 +331,7 @@ module SmtPrinter = struct Z.pp_print (Q.den q) let pp_binder ppf (var, ty) = - Fmt.pf ppf "(%a %a)" Var.print var Ty.pp_smtlib ty + Fmt.pf ppf "(%a %a)" Var.pp var Ty.pp_smtlib ty let pp_binders = Fmt.(box @@ iter_bindings ~sep:sp Var.Map.iter pp_binder) @@ -444,7 +444,7 @@ module SmtPrinter = struct | Sy.Let, [] -> let x = match bind with B_let x -> x | _ -> assert false in Fmt.pf ppf "@[<2>(let@ ((%a %a))@ %a@])" - Var.print x.let_v + Var.pp x.let_v pp x.let_e pp_boxed x.in_e @@ -479,17 +479,17 @@ 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 + | Sy.Name { id = Hstring { ns = Abstract; _ } as id; _ }, [] -> + Fmt.pf ppf "(as %a %a)" Id.pp id Ty.pp_smtlib ty - | Sy.Name { hs = n; _ }, [] -> Id.pp ppf n + | Sy.Name { id; _ }, [] -> Id.pp ppf id - | Sy.Name { hs = n; _ }, _ :: _ -> + | Sy.Name { id; _ }, _ :: _ -> Fmt.pf ppf "@[<2>(%a %a@])" - Id.pp n + Id.pp id Fmt.(list ~sep:sp pp |> box) xs - | Sy.Var v, [] -> Var.print ppf v + | Sy.Var v, [] -> Var.pp ppf v | Sy.Int i, [] -> pp_integer ppf i @@ -502,7 +502,7 @@ module SmtPrinter = struct Fmt.pf ppf "#b%s" (Z.format (Fmt.str "%%0%db" n) s) | Sy.MapsTo v, [t] -> - Fmt.pf ppf "@[<2>(ae.mapsto %a %a@])" Var.print v pp t + Fmt.pf ppf "@[<2>(ae.mapsto %a %a@])" Var.pp v pp t | Sy.In (_lb, _rb), [_t] -> (* WARNING: we don't print the content of this semantic trigger as @@ -533,7 +533,7 @@ end module AEPrinter = struct let pp_binder ppf (var, ty) = - Fmt.pf ppf "%a:%a" Var.print var Ty.pp_smtlib ty + Fmt.pf ppf "%a:%a" Var.pp var Ty.pp_smtlib ty let pp_binders ppf binders = if Var.Map.is_empty binders then @@ -631,7 +631,7 @@ module AEPrinter = struct (fun ppf x -> if Options.get_verbose () then Fmt.pf ppf " [sko = %a]" pp x.let_sko) x - Var.print x.let_v pp x.let_e pp_silent x.in_e + Var.pp x.let_v pp x.let_e pp_silent x.in_e | Sy.(Op Get), [e1; e2] -> Fmt.pf ppf "%a[%a]" pp e1 pp e2 @@ -982,17 +982,20 @@ let vrai = let faux = neg (vrai) let fresh_name ty = - mk_term (Sy.name ~ns:Fresh @@ Id.Namespace.Internal.fresh ()) [] ty + let sy = Sy.name @@ Id.fresh ~ns:Fresh () in + mk_term sy [] ty let mk_abstract ty = - mk_term (Sy.name ~ns:Abstract @@ Id.Namespace.Abstract.fresh ()) [] ty + let sy = Sy.name @@ Id.fresh ~ns:Abstract () in + mk_term sy [] ty let fresh_ac_name ty = - mk_term (Sy.name ~ns:Fresh_ac @@ Id.Namespace.Internal.fresh ()) [] ty + let sy = Sy.name @@ Id.fresh ~ns:Fresh_ac () in + mk_term sy [] ty let is_fresh_ac_name t = match t with - | { f = Name { ns = Fresh_ac; _ }; xs = []; _ } -> true + | { f = Name { id = Hstring { ns = Fresh_ac; _ }; _ }; xs = []; _ } -> true | _ -> false let positive_int i = mk_term (Sy.int i) [] Ty.Tint @@ -1814,7 +1817,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 @@ Id.of_string ~ns:Skolem str) "%s%s!%d" s tyvars diff --git a/src/lib/structures/id.ml b/src/lib/structures/id.ml index b8666d20a0..e1933ef937 100644 --- a/src/lib/structures/id.ml +++ b/src/lib/structures/id.ml @@ -16,45 +16,135 @@ (* *) (**************************************************************************) -type t = Hstring.t [@@deriving ord] +type name_space = Internal | Fresh | Fresh_ac | Skolem | Abstract -type typed = t * Ty.t list * Ty.t [@@deriving ord] +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 -let equal = Hstring.equal +module Internal = Make () +module Skolem = Make () +module Abstract = Make () -let pp ppf id = - Dolmen.Smtlib2.Script.Poly.Print.id ppf - (Dolmen.Std.Name.simple (Hstring.view id)) +type t = + | Term_cst of { tcst : Dolmen.Std.Expr.term_cst; defined : bool } + | Hstring of { hs : Hstring.t; ns : name_space } -let show id = Fmt.str "%a" pp id +type typed = Dolmen.Std.Expr.term_cst * Ty.t list * Ty.t -module Namespace = struct - module type S = sig - val fresh : ?base:string -> unit -> string - end +let compare_typed (t1, _, _) (t2, _, _) = + Dolmen.Std.Expr.Term.Const.compare t1 t2 - 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 +let mangle ns s = + match ns with + | Internal -> ".!" ^ s + | Fresh -> ".k" ^ s + | Fresh_ac -> ".K" ^ s + | Skolem -> ".?__" ^ s + | Abstract -> "@a" ^ s - module Internal = Make () +let of_term_cst ?(defined = false) tcst = + (* If the name we got from the user starts with either "." + or "@" (which are prefixes reserved for solver use in the SMT-LIB + standard), the name will be printed with an extra ".". So if the user + writes ".x" or "@x", it will be printed as "..x" and ".@x" instead. - module Skolem = Make () + Normally, this should not occur, but we do this to ensure no confusion + even if invalid names ever sneak through. *) + assert ( + let s = Util.show_term_cst tcst in + not (Compat.String.starts_with ~prefix:"." s) && + not (Compat.String.starts_with ~prefix:"@" s)); + Term_cst { tcst; defined } - module Abstract = Make () +let of_string ~ns s = + let () = + match ns with + | Fresh | Fresh_ac | Abstract -> invalid_arg "of_string" + | _ -> () + in + let hs = Hstring.make (mangle ns s) in + Hstring { hs; ns } - let reinit () = - Internal.reset_fresh_cpt (); - Skolem.reset_fresh_cpt (); - Abstract.reset_fresh_cpt () -end +let fresh ?base ~ns () = + let s = + match ns with + | Skolem -> Skolem.fresh ?base () + | Abstract -> Abstract.fresh ?base () + | _ -> Internal.fresh ?base () + in + let hs = Hstring.make (mangle ns s) in + Hstring { hs; ns } + +let compare i1 i2 = + match i1, i2 with + | Term_cst { tcst = t1; defined = d1 }, + Term_cst { tcst = t2; defined = d2 } -> + let c = Bool.compare d1 d2 in + if c <> 0 then c + else Dolmen.Std.Expr.Term.Const.compare t1 t2 + | Term_cst _, _ -> 1 + | _, Term_cst _ -> -1 + + | Hstring { hs = hs1; _ }, Hstring { hs = hs2; _ } -> + (* NB: Internal identifiers are pre-mangled, which means that we do not + need to take the name space into consideration when comparing. *) + Hstring.compare hs1 hs2 + +let equal i1 i2 = + match i1, i2 with + | Term_cst { tcst = t1; defined = d1 }, + Term_cst { tcst = t2; defined = d2 } -> + Bool.equal d1 d2 && Dolmen.Std.Expr.Term.Const.equal t1 t2 + | Hstring { hs = hs1; _ }, Hstring { hs = hs2; _ } -> + (* NB: Internal identifiers are pre-mangled, which means that we do not + need to take the name space into consideration when comparing. *) + Hstring.equal hs1 hs2 + | _ -> false + +let hash i = + match i with + | Term_cst { tcst; _ } -> + Dolmen.Std.Expr.Term.Const.hash tcst + | Hstring { hs; _ } -> + (* NB: Internal identifiers are pre-mangled, which means that we do not + need to take the name space into consideration when hashing. *) + Hstring.hash hs + +let pp ppf i = + match i with + | Term_cst { tcst; _ } -> Util.pp_term_cst ppf tcst + | Hstring { hs; _ } -> + (* Names are pre-mangled *) + Dolmen.Smtlib2.Script.Poly.Print.id ppf + @@ Dolmen.Std.Name.simple @@ Hstring.view hs + +let show = Fmt.to_to_string pp + +let is_suspicious i = + match i with + | Term_cst _ -> false + | Hstring { hs; _ } -> + match Hstring.view hs with + | "@/" | "@%" | "@*" -> true + | _ -> false + +let reinit () = + Internal.reset_fresh_cpt (); + Skolem.reset_fresh_cpt (); + Abstract.reset_fresh_cpt () + +module Map = Map.Make (struct + type nonrec t = t + let compare = compare + end) diff --git a/src/lib/structures/id.mli b/src/lib/structures/id.mli index 5666a0a8a4..437f4928ba 100644 --- a/src/lib/structures/id.mli +++ b/src/lib/structures/id.mli @@ -16,29 +16,115 @@ (* *) (**************************************************************************) -type t = Hstring.t [@@deriving ord] +(** The [name_space] type discriminates the different types of internal + identifiers. The same string in different name spaces is considered as + different identifiers. -type typed = t * Ty.t list * Ty.t -(** Typed identifier of function. In order: - - The identifier. - - Types of its arguments. - - The returned type. *) + Note that the identifier stored in the [Hstring] constructor below are + mangled during its creation: a special prefix is added depending on the + name space. *) +type name_space = + | Internal + (** This symbol is an internal implementation detail of the solver, such as + a proxy formula or the abstracted counterpart of AC symbols. + Internal identifiers are printed with a ".!" prefix. *) + | Fresh + (** This symbol is a "fresh" internal identifer. Fresh internal identifiers + play a similar role as internal identifiers, but they always represent a + constant that was introduced during solving as part of some kind of + purification or abstraction procedure. + + In order to correctly implement AC(X) in the presence of distributive + symbols, symbols generated for AC(X) abstraction use a special + namespace, [Fresh_ac] below. + + To ensure uniqueness, fresh identifiers must always be generated using + [Id.Namespace.Internal.fresh ()]. + + In particular, fresh identifiers are only used to denote constants, not + arbitrary functions. *) + | Fresh_ac + (** This symbol has been introduced as part of the AC(X) abstraction process. + This is notably used by some parts of AC(X) that check if terms contains + fresh symbols (see [contains_a_fresh_alien] in the [Arith] module for an + example). + + These correspond to the K sort in the AC(X) paper. They use a different + name space from other fresh symbols because we need to be able to know + whether a fresh symbol comes from the AC(X) abstraction procedure in order + to prevent loops. + + To ensure uniqueness, AC abstraction identifiers must always be generated + using [fresh ~ns:Fresh_ac ()]. *) + | Skolem + (** This symbol has been introduced as part of skolemization, and represents + the (dependent) variable of an existential quantifier. Skolem identifiers + can have arbitrary arity to depend on previous skolem names in binding + order (so if you have `(exists (x y) e)` then there will be a skolem + variable `sko_x` and a skolem function `(sko_y sko_x)`). *) + | Abstract + (** This symbol has been introduced as part of model generation, and + represents an abstract value. + + To ensure uniqueness, abstract identifiers must always be generated using + [fresh ~ns:Abstract ()]. *) + +type t = private + | Term_cst of { tcst : Dolmen.Std.Expr.term_cst; defined : bool } + (** This identifier was declared or defined by the user, and appears as is + somewhere in a source file. *) + + | Hstring of { hs : Hstring.t; ns : name_space } + +(* TODO: remove this type after replacing Alt-Ergo types by Dolmen types. *) +type typed = Dolmen.Std.Expr.term_cst * Ty.t list * Ty.t val compare_typed : typed -> typed -> int + +val of_term_cst : ?defined:bool -> Dolmen.Std.Expr.term_cst -> t +(** [of_term_cst ?defined t] creates an identifier from a constant term. + The argument [defined] is used to determine if the identifier is + declared or defined by user. *) + +val of_string : ns:name_space -> string -> t +(** [of_string ~ns s] creates an identifier in the name space [ns] from the + string [s]. + + Note that identifiers are pre-mangled: the [hs] field of the resulting + identifier may not be exactly the string that was passed to this function + (however, calling [of_string] with the same string but two different name + spaces is guaranteed to return two identifiers with distinct [hs] fields). + + @raise Invalid_argument if the name space is [Fresh], [Fresh_ac] or + [Abstract]. *) + +val fresh : ?base:string -> ns:name_space -> unit -> t +(** [fresh ?base ~ns ()] generates a fresh identifier within the name space [ns] + derived from the base string [base]. If [base] is not provided, an empty + string is used by default. + + The identifier is pre-mangled similarly to [of_string]. *) + +val compare : t -> t -> int +(** [compare i1 i2] compares the identifiers [i1] and [i2]. *) + val equal : t -> t -> bool -val show : t -> string +(** [equal i1 i2] checks if [i1] and [i2] are equal. *) + +val hash : t -> int +(** [hash i] computes a hash for the identifier [i]. On term constant + identifiers, this hash is perfect. *) + val pp : t Fmt.t +(** [pp ppf i] prints the identifier [i] on the formatter [ppf], quoting the + string, if it needs. *) + +val show : t -> string +(** Same as [pp] but outputs the result as a string. *) -module Namespace : sig - module type S = sig - val fresh : ?base:string -> unit -> string - end +val is_suspicious : t -> bool - module Internal : S - module Skolem : S - module Abstract : S +val reinit : unit -> unit +(** Resets the internal counters of the [fresh] function. *) - val reinit : unit -> unit - (** Resets the [fresh_internal_name], [fresh_skolem] and [fresh_abstract] - counters. *) -end +module Map : Map.S with type key = t diff --git a/src/lib/structures/modelMap.ml b/src/lib/structures/modelMap.ml index 47df05ccbe..015452e37b 100644 --- a/src/lib/structures/modelMap.ml +++ b/src/lib/structures/modelMap.ml @@ -127,7 +127,7 @@ type t = { let add ((id, arg_tys, _) as sy) 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" Util.pp_term_cst id; let constraints = match P.find sy values with | C g -> g @@ -157,7 +157,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 { id = id'; _ }, [] when Id.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))); @@ -188,7 +188,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 + Util.pp_term_cst 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 f3bc5406ef..0f0f6fd127 100644 --- a/src/lib/structures/modelMap.mli +++ b/src/lib/structures/modelMap.mli @@ -29,8 +29,8 @@ type t (** Type of model. *) val add : Id.typed -> 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]. *) +(** [add id args ret mdl] adds the binding [args -> ret] to the partial graph + associated with the identifier [id]. *) val empty : suspicious:bool -> Id.typed list -> t (** An empty model. The [suspicious] flag is used to remember that this @@ -38,8 +38,10 @@ val empty : suspicious:bool -> Id.typed list -> t model generation is known to be incomplete. *) val find : Id.typed -> t -> graph -(** [find sy mdl] returns the graph associated with the symbol [sy] in the model - [mdl], raises [Not_found] if it doesn't exist. *) +(** [find id mdl] returns the graph associated with the identifier [id] in the + model [mdl]. + + @raise Not_found if it does not exist. *) val fold: (Id.typed -> graph -> 'a -> 'a) -> t -> 'a -> 'a (** [fold f mdl init] folds over the bindings in the model [mdl] with the diff --git a/src/lib/structures/satml_types.ml b/src/lib/structures/satml_types.ml index be109c2de4..7f3ee6bb10 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 @@ Id.of_string ~ns:Internal @@ + "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 @@ Id.of_string ~ns:Internal + @@ "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 87e47fb45a..ad48a3ba21 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -79,32 +79,6 @@ type form = type name_kind = Ac | Other -type name_space = User | Internal | Fresh | Fresh_ac | Skolem | Abstract - -let compare_name_space ns1 ns2 = - match ns1, ns2 with - | User, User -> 0 - | User, _ -> -1 - | _, User -> 1 - - | Internal, Internal -> 0 - | Internal, _ -> -1 - | _, Internal -> 1 - - | Fresh, Fresh -> 0 - | Fresh, _ -> -1 - | _, Fresh -> 1 - - | Fresh_ac, Fresh_ac -> 0 - | Fresh_ac, _ -> -1 - | _, Fresh_ac -> 1 - - | Skolem, Skolem -> 0 - | Skolem, _ -> -1 - | _, Skolem -> 1 - - | Abstract, Abstract -> 0 - type bound_kind = Unbounded | VarBnd of Var.t | ValBnd of Numbers.Q.t type bound = (* private *) @@ -113,11 +87,7 @@ type bound = (* private *) type t = | True | False - | Name of - { hs : Id.t - ; kind : name_kind - ; defined : bool - ; ns : name_space } + | Name of { id : Id.t ; kind : name_kind } | Int of Z.t | Real of Q.t | Bitv of int * Z.t @@ -129,21 +99,7 @@ type t = | MapsTo of Var.t | Let -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 - -(* 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) id = Name { id ; kind } let var s = Var s let int i = Int (Z.of_string i) @@ -174,8 +130,10 @@ let is_ac x = match x with | _ -> false let is_internal sy = + (* In the current `Id` implementation, all constant terms are user-provided. + This will change once Dolmen identifiers are adopted everywhere. *) match sy with - | Name { ns = User; _ } -> false + | Name { id = Term_cst _; _ } -> false | Name _ -> true | _ -> false @@ -263,12 +221,10 @@ let compare s1 s2 = | Int z1, Int z2 -> Z.compare z1 z2 | Real h1, Real h2 -> Q.compare h1 h2 | 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 - if c <> 0 then c else - let c = compare_kinds k1 k2 in - if c <> 0 then c else compare_name_space ns1 ns2 + | Name { id = i1; kind = k1; _ }, + Name { id = i2; kind = k2; _ } -> + let c = Id.compare i1 i2 in + if c <> 0 then c else compare_kinds k1 k2 | Bitv (n1, s1), Bitv (n2, s2) -> let c = Int.compare n1 n2 in if c <> 0 then c else Z.compare s1 s2 @@ -295,8 +251,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 { id; kind = Ac; _ } -> 19 * Id.hash id + 5 + | Name { id; kind = Other; _ } -> 19 * Id.hash id + 6 | Int z -> 19 * Z.hash z + 7 | Real n -> 19 * Hashtbl.hash n + 7 | Var v -> 19 * Var.hash v + 8 @@ -307,7 +263,7 @@ let hash x = let string_of_bound_kind x = match x with | Unbounded -> "?" - | VarBnd v -> Var.to_string v + | VarBnd v -> Var.show v | ValBnd v -> Numbers.Q.to_string v let string_of_bound b = @@ -319,10 +275,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 @@ -427,9 +379,9 @@ 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) - | Var v when show_vars -> Fmt.pf ppf "'%s'" (Var.to_string v) - | Var v -> Fmt.string ppf (Var.to_string v) + | Name { id; _ } -> Id.pp ppf id + | Var v when show_vars -> Fmt.pf ppf "'%s'" (Var.show v) + | Var v -> Fmt.string ppf (Var.show v) (* Reals and Ints theories *) | Int i -> Z.pp_print ppf i @@ -442,7 +394,7 @@ module AEPrinter = struct (* Symbols used in semantic triggers *) | In (lb, rb) -> Fmt.pf ppf "%s, %s" (string_of_bound lb) (string_of_bound rb) - | MapsTo v -> Fmt.pf ppf "%a |->" Var.print v + | MapsTo v -> Fmt.pf ppf "%a |->" Var.pp v end module SmtPrinter = struct @@ -527,9 +479,9 @@ 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_var base = Var.of_string (fresh_skolem_string base) +let fresh_skolem_name base = name @@ Id.of_string ~ns:Skolem base + +let fresh_skolem_var base = Var.of_id @@ Id.fresh ~base ~ns:Skolem () let is_get f = equal f (Op Get) let is_set f = equal f (Op Set) diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli index eb93fb3e79..b7a037b206 100644 --- a/src/lib/structures/symbols.mli +++ b/src/lib/structures/symbols.mli @@ -77,70 +77,6 @@ type form = type name_kind = Ac | Other -(** The [name_space] type discriminates the different types of names. The same - string in different name spaces is considered as different names. - - Note that the names stored in the [Name] constructor below are mangled - during creation of the symbol: a special prefix is added depending on the - name space. *) -type name_space = - | User - (** This symbol was defined by the user, and appears as is somewhere in a - source file. - - As an exception, if the name we got from the user starts with either "." - or "@" (which are prefixes reserved for solver use in the SMT-LIB - standard), the name will be printed with an extra ".". So if the user - writes ".x" or "@x", it will be printed as "..x" and ".@x" instead. - - Normally, this shouldn't occur, but we do this to ensure no confusion - even if invalid names ever sneak through. *) - | Internal - (** This symbol is an internal implementation detail of the solver, such as - a proxy formula or the abstracted counterpart of AC symbols. - - Internal names are printed with a ".!" prefix. *) - | Fresh - (** This symbol is a "fresh" internal name. Fresh internal names play a - similar role as internal names, but they always represent a constant - that was introduced during solving as part of some kind of purification - or abstraction procedure. - - In order to correctly implement AC(X) in the presence of distributive - symbols, symbols generated for AC(X) abstraction use a special - namespace, [Fresh_ac] below. - - To ensure uniqueness, fresh names must always be generated using - [Id.Namespace.Internal.fresh ()]. - - In particular, fresh names are only used to denote constants, not - arbitrary functions. *) - | Fresh_ac - (** This symbol has been introduced as part of the AC(X) abstraction process. - This is notably used by some parts of AC(X) that check if terms contains - fresh symbols (see [contains_a_fresh_alien] in the [Arith] module for an - example). - - These correspond to the K sort in the AC(X) paper. They use a different - name space from other fresh symbols because we need to be able to know - whether a fresh symbol comes from the AC(X) abstraction procedure in order - to prevent loops. - - To ensure uniqueness, AC abstraction names must always be generated using - [Id.Namespace.Internal.fresh ()]. *) - | Skolem - (** This symbol has been introduced as part of skolemization, and represents - the (dependent) variable of an existential quantifier. Skolem names can - have arbitrary arity to depend on previous skolem names in binding order - (so if you have `(exists (x y) e)` then there will be a skolem variable - `sko_x` and a skolem function `(sko_y sko_x)`). *) - | Abstract - (** This symbol has been introduced as part of model generation, and - represents an abstract value. - - To ensure uniqueness, abstract names must always be generated using - [Id.Namespace.Abstract.fresh ()]. *) - type bound_kind = Unbounded | VarBnd of Var.t | ValBnd of Numbers.Q.t type bound = private @@ -149,12 +85,7 @@ type bound = private type t = | True | False - | Name of - { hs : Id.t - (** Note: [hs] is prefixed according to [ns]. *) - ; kind : name_kind - ; defined : bool - ; ns : name_space } + | Name of { id : Id.t ; kind : name_kind } | Int of Z.t | Real of Q.t | Bitv of int * Z.t @@ -166,15 +97,9 @@ type t = | MapsTo of Var.t | Let -(** Create a new symbol with the given name. - - By default, names are created in the [User] name space. - - Note that names are pre-mangled: the [hs] field of the resulting name may - 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 -> Id.t -> t +(** Create a new symbol with the given identifier. + By default, the kind is is [Other]. *) val var : Var.t -> t val int : string -> t @@ -205,15 +130,13 @@ 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. *) +(** [pp_ae_operator ppf op] prints the operator symbol [op] on the + formatter [ppf] using the Alt-Ergo native format. *) val pp_smtlib_operator : operator Fmt.t -(* [pp_smtlib_operator ppf op] prints the operator symbol [op] on the - formatter [ppf] using the SMT-LIB format. *) +(** [pp_smtlib_operator ppf op] prints the operator symbol [op] on the + formatter [ppf] using the SMT-LIB format. *) (*val dummy : t*) diff --git a/src/lib/structures/var.ml b/src/lib/structures/var.ml index a451f569b9..903735c5f7 100644 --- a/src/lib/structures/var.ml +++ b/src/lib/structures/var.ml @@ -25,7 +25,6 @@ (* *) (**************************************************************************) -type repr = Underscore | Local of Hstring.t | Named of Hstring.t (** A variable can be: - The special `Underscore` variable that is used to discard values in @@ -37,63 +36,61 @@ type repr = Underscore | Local of Hstring.t | Named of Hstring.t user. Depending on the input format, regular variable may start with '?' (e.g. in SMT-LIB format, this is allowed). *) +type t = + | Underscore + | Local of Id.t + | Named of Id.t + +let[@inline always] local id = + assert ( + let s = Id.show id in + Compat.String.starts_with ~prefix:"?" s); + Local id + +let[@inline always] of_id i = + assert ( + match i with + | Id.Term_cst _ | Hstring { ns = Skolem; _ } -> true + | _ -> false); + Named i + +(* Note: there is a single [Underscore] variable, with id 0. *) +let underscore = Underscore + +let is_local v = match v with Local _ -> true | _ -> false + +let uid v = + match v with + | Underscore -> 0 + | Local i -> 3 * Id.hash i + 1 + | Named i -> 3 * Id.hash i + 2 + +let hash = uid let equal_repr v1 v2 = match v1, v2 with | Underscore, Underscore -> true | Underscore, _ | _, Underscore -> false - | Local hs1, Local hs2 - | Named hs1, Named hs2 -> Hstring.equal hs1 hs2 + | Local i1, Local i2 + | Named i1, Named i2 -> Id.equal i1 i2 | Local _, Named _ | Named _, Local _ -> false -let pp_repr ppf = function - | Underscore -> Fmt.pf ppf "_" - | Local hs | Named hs -> Hstring.print ppf hs - -type t = { repr : repr ; id : int } - -let fresh, save_cnt, reinit_cnt = - let cpt = ref 0 in - let fresh repr = incr cpt; { repr ; id = !cpt } in - let saved_cnt = ref 0 in - let save_cnt () = - saved_cnt := !cpt - in - let reinit_cnt () = - cpt := !saved_cnt - in - fresh, save_cnt, reinit_cnt - -let of_hstring hs = fresh (Named hs) - -let of_string s = of_hstring (Hstring.make s) - -let local s = - assert (String.length s > 0 && Char.equal '?' s.[0]); - fresh (Local (Hstring.make s)) - -let is_local { repr; _ } = match repr with Local _ -> true | _ -> false - let compare a b = - let c = a.id - b.id in + let c = (uid a) - (uid b) in if c <> 0 then c else begin - assert (equal_repr a.repr b.repr); + assert (equal_repr a b); c end let equal a b = compare a b = 0 -let uid { id; _ } = id - -let hash = uid - -(* Note: there is a single [Underscore] variable, with id 1. *) -let underscore = fresh Underscore - -let print ppf { repr; id } = Fmt.pf ppf "%a~%d" pp_repr repr id +let pp ppf = function + | Underscore -> Fmt.pf ppf "_" + | Local i | Named i -> + Fmt.pf ppf "%a~%d" Id.pp i (Id.hash i) -let to_string = Fmt.to_to_string print +let show = Fmt.to_to_string pp module Set = Set.Make(struct type nonrec t = t let compare = compare end) @@ -104,5 +101,5 @@ module Map = struct let sep ppf () = Fmt.pf ppf " -> " in Fmt.box @@ Fmt.braces @@ Fmt.iter_bindings ~sep:Fmt.comma iter - @@ Fmt.pair ~sep print pp_elt + @@ Fmt.pair ~sep pp pp_elt end diff --git a/src/lib/structures/var.mli b/src/lib/structures/var.mli index 128eb2eb1e..2bfd651968 100644 --- a/src/lib/structures/var.mli +++ b/src/lib/structures/var.mli @@ -26,20 +26,20 @@ (**************************************************************************) type t +(** Type of variable. *) -val of_hstring : Hstring.t -> t -(** Create a *fresh* variable with the given name. +val of_id : Id.t -> t +(** Create a variable from an identifier. *) - Calling [of_hstring] twice with the same [Hstring.t] as argument will result - in *distinct* variables. *) - -val of_string : string -> t -(** Convenient alias for [of_hstring (Hstring.make s)]. *) - -val local : string -> t +val local : Id.t -> t (** Create a new "local" variable. Local variables are variables used exclusively in user-defined theories for semantic triggers, and are - implicitly bound at the level of the enclosing quantifier. *) + implicitly bound at the level of the enclosing quantifier. + They must starts with `?`. *) + +val underscore : t +(** Unique special variable. Used to indicate fields that should be ignored in + pattern matching and triggers. *) val is_local : t -> bool (** Indicates whether the given variable is a local variable (see {!local} above @@ -54,21 +54,9 @@ val hash : t -> int val uid : t -> int (** Globally unique identifier for the variable. *) -val underscore : t -(** Unique special variable. Used to indicate fields that should be ignored in - pattern matching and triggers. *) - -val print : Format.formatter -> t -> unit - -val to_string : t -> string - -val save_cnt: unit -> unit -(** Saves the values of the counter *) +val pp : Format.formatter -> t -> unit -val reinit_cnt: unit -> unit -(** Reinitializes the counter to the saved value with [save_cnt], 1 if no value - is saved, since after the initialization of the modules [cnt] is set to 1 - when initializing the [underscore] constant in the Symbols module *) +val show : t -> string module Set : Set.S with type elt = t diff --git a/src/lib/util/util.ml b/src/lib/util/util.ml index 6f43b934b8..2b0f407511 100644 --- a/src/lib/util/util.ml +++ b/src/lib/util/util.ml @@ -202,3 +202,29 @@ let rec print_list_pp ~sep ~pp fmt = function let internal_error msg = Format.kasprintf (fun s -> raise (Internal_error s)) msg + +module DStd = Dolmen.Std + +let pp_term_cst ppf t = + let show = Fmt.to_to_string DStd.Expr.Term.Const.print in + Dolmen.Smtlib2.Script.Poly.Print.id ppf + @@ DStd.Name.simple (show t) + +let show_term_cst = Fmt.to_to_string pp_term_cst + +(** Helper function: returns the basename of a dolmen path, since in AE + the problems are contained in one-file (for now at least), the path is + irrelevant and only the basename matters *) +let get_basename = function + | DStd.Path.Local { name; } + | Absolute { name; path = []; } -> name + | Absolute { name; path; } -> + Fmt.failwith + "Expected an empty path to the basename: \"%s\" but got: [%a]." + name (fun fmt l -> + match l with + | h :: t -> + Format.fprintf fmt "%s" h; + List.iter (Format.fprintf fmt "; %s") t + | _ -> () + ) path diff --git a/src/lib/util/util.mli b/src/lib/util/util.mli index 196e922c78..7c5d48443a 100644 --- a/src/lib/util/util.mli +++ b/src/lib/util/util.mli @@ -134,3 +134,12 @@ val print_list_pp: Format.formatter -> 'a list -> unit val internal_error : ('a, Format.formatter, unit, 'b) format4 -> 'a + +val pp_term_cst : Dolmen.Std.Expr.term_cst Fmt.t +(** [pp_term_cst ppf t] prints the constant term to the formatter [ppf], + surrounding it with quotes, if it needs. *) + +val show_term_cst : Dolmen.Std.Expr.term_cst -> string +(** Same as pp_term_cst but outpus the result as a string. *) + +val get_basename : Dolmen.Std.Path.t -> string diff --git a/tests/issues/854/function.default.expected b/tests/issues/854/function.default.expected index 63577badcf..6e5eeb8fb5 100644 --- a/tests/issues/854/function.default.expected +++ b/tests/issues/854/function.default.expected @@ -1,8 +1,8 @@ unknown ( - (define-fun a () Int 0) (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref)) + (define-fun a () Int 0) (define-fun f ((_arg_0 Int)) Int 0) (define-fun a1 () Int 0) ) diff --git a/tests/issues/854/original.default.expected b/tests/issues/854/original.default.expected index a0ce9f571c..7d40ab42e2 100644 --- a/tests/issues/854/original.default.expected +++ b/tests/issues/854/original.default.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.default.expected b/tests/issues/854/twice_eq.default.expected index 3488c940f2..ee4c1de0d3 100644 --- a/tests/issues/854/twice_eq.default.expected +++ b/tests/issues/854/twice_eq.default.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.default.expected b/tests/models/adt/arith.default.expected index 18e539f318..7da79872d1 100644 --- a/tests/models/adt/arith.default.expected +++ b/tests/models/adt/arith.default.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.default.expected b/tests/models/arith/arith11.default.expected index 216672887e..35ae71285c 100644 --- a/tests/models/arith/arith11.default.expected +++ b/tests/models/arith/arith11.default.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.default.expected b/tests/models/array/embedded-array.default.expected index 0cb5c3d3ec..057bc1a6c0 100644 --- a/tests/models/array/embedded-array.default.expected +++ b/tests/models/array/embedded-array.default.expected @@ -1,8 +1,8 @@ unknown ( + (define-fun s () S (as @a2 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)) ) diff --git a/tests/models/bool/bool1.default.expected b/tests/models/bool/bool1.default.expected index 1eb3e25e7d..3a2ce307f4 100644 --- a/tests/models/bool/bool1.default.expected +++ b/tests/models/bool/bool1.default.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.default.expected b/tests/models/bool/bool3.default.expected index 341a2df7ef..ed7a9b1e24 100644 --- a/tests/models/bool/bool3.default.expected +++ b/tests/models/bool/bool3.default.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/records/record3.default.expected b/tests/models/records/record3.default.expected index 8b2d9f83ae..b478bf755b 100644 --- a/tests/models/records/record3.default.expected +++ b/tests/models/records/record3.default.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.default.expected b/tests/models/uf/uf1.default.expected index d3b170c21e..2891baf569 100644 --- a/tests/models/uf/uf1.default.expected +++ b/tests/models/uf/uf1.default.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.default.expected b/tests/models/uf/uf2.default.expected index 232c59a455..faa7fb056c 100644 --- a/tests/models/uf/uf2.default.expected +++ b/tests/models/uf/uf2.default.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)) ) From 3f8f7390db7ad14e5be055c6b52812751e61168b Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 30 Jan 2025 18:52:58 +0100 Subject: [PATCH 2/2] Fix issue 1243 The fix consists in using `declared_ids` to guarantee that we never define symbols that have not been declared at the current assertion level in models. A proper fix requires a lot of work as we need to rework the push/pop mechanism of CDCL. This PR is rebased #1280 to ensure we won't mix identifiers from different assertion levels as it could happen with string-based identifiers. --- src/lib/reasoners/uf.ml | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index afdc738b1b..0ef6378683 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -1117,12 +1117,25 @@ let is_suspicious_symbol = function | Symbols.Name { id; _ } when Id.is_suspicious id -> true | _ -> false -let terms env = +module ConstSet = Set.Make (Dolmen.Std.Expr.Term.Const) + +let terms ~declared_ids env = + let declared = + List.fold_left + (fun acc (tcst, _, _) -> ConstSet.add tcst acc) + ConstSet.empty declared_ids + in ME.fold (fun t r ((terms, suspicious) as acc) -> let Expr.{ f; _ } = Expr.term_view t in match f with - | Name { id = Term_cst { defined = true; _ }; _ } -> + | Name { id = Term_cst { tcst; _ }; _ } + when not @@ ConstSet.mem tcst declared -> + (* XXX: the current push/pop mechanism of CDCL is insufficient + to guarantee that only identifiers declared at the current + assertion level reach this point. + The [declared_ids] argument does not have this issue. + See issue https://github.com/OCamlPro/alt-ergo/issues/1243. *) (* We do not store names defined by the user. *) acc | _ -> @@ -1256,7 +1269,7 @@ let extract_concrete_model cache = let compute_concrete_model_of_val = compute_concrete_model_of_val cache in let get_abstract_for = Cache.get_abstract_for cache.abstracts in fun ~prop_model ~declared_ids env -> - let terms, suspicious = terms env in + let terms, suspicious = terms ~declared_ids env in let model, mrepr = MED.fold (fun t _mk acc -> compute_concrete_model_of_val env t acc) terms (ModelMap.empty ~suspicious declared_ids, ME.empty)