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..0ef6378683 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -1112,23 +1112,31 @@ 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 = +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 { defined = true; _ } -> - (* We don't store names defined by the user. *) + | 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 | _ -> let suspicious = is_suspicious_symbol f || suspicious in @@ -1234,7 +1242,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 +1256,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 @@ -1257,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) @@ -1273,24 +1285,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)) )