From 0a1f35ee0f362ac541636ac4496e8849dd4ada2d Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 2 Apr 2024 14:46:35 +0200 Subject: [PATCH] ADT destructors are delayed functions Before this PR, the ADT destructors worked as follow: - Destructor applictions from the user input were guarded: there are considered as aliens by the ADT theory; - If the domain of an ADT semantic values became a singleton or if the input contains a tester application on this value, the ADT destructor application on this semantic value became interpreted. The reason of this contruction is because all the functions are total in the SMT-LIB standard, even the destructors. So a destructor is partially interpreted: If `v` is an ADT value and `d` is a destructor of this ADT associated with the constructor `c`, then: - `d v` can be anything if the constructor of `v` isn't necessary `c`; - `d v` is the field of `c` associated with `d` if the only possible constructor for `v` is `c`. This PR uses the new mechanism `Rel_utils.Delayed` to delay the computation of `d v` until we know that `v` is of the form `(c ...)`. --- src/lib/frontend/cnf.ml | 4 +- src/lib/frontend/d_cnf.ml | 2 +- src/lib/frontend/models.ml | 5 +- src/lib/frontend/parsed_interface.ml | 4 +- src/lib/frontend/parsed_interface.mli | 2 +- src/lib/frontend/typechecker.ml | 18 +- src/lib/reasoners/adt.ml | 16 +- src/lib/reasoners/adt_rel.ml | 333 +++++++------------------- src/lib/reasoners/rel_utils.ml | 6 + src/lib/structures/expr.ml | 12 +- src/lib/structures/parsed.ml | 4 +- src/lib/structures/parsed.mli | 2 +- src/lib/structures/symbols.ml | 18 +- src/lib/structures/symbols.mli | 4 +- src/lib/structures/typed.ml | 8 +- src/lib/structures/typed.mli | 6 +- src/parsers/native_parser.mly | 2 +- 17 files changed, 144 insertions(+), 302 deletions(-) diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml index 22c165d896..14a641b61d 100644 --- a/src/lib/frontend/cnf.ml +++ b/src/lib/frontend/cnf.ml @@ -149,8 +149,8 @@ let rec make_term quant_basename t = let t2 = mk_term t2 in E.mk_ite cond t1 t2 - | TTproject (b, t, s) -> - E.mk_term (Sy.destruct ~guarded:b (Hstring.view s)) [mk_term t] ty + | TTproject (t, s) -> + E.mk_term (Sy.destruct (Hstring.view s)) [mk_term t] ty | TTmatch (e, pats) -> let e = make_term quant_basename e in diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index 2d45eb98c6..7448d199e7 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -1046,7 +1046,7 @@ let rec mk_expr | Trecord _ -> Sy.Op (Sy.Access (Hstring.make name)) | Tadt _ -> - Sy.destruct ~guarded:true name + Sy.destruct name | _ -> assert false in E.mk_term sy [e] ty diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml index eefc11ce75..4ed2f92ec2 100644 --- a/src/lib/frontend/models.ml +++ b/src/lib/frontend/models.ml @@ -185,9 +185,8 @@ module Pp_smtlib_term = struct else fprintf fmt "(%a %a %a)" print e1 Sy.print f print e2 - | Sy.Op Sy.Destruct (hs, grded), [e] -> - fprintf fmt "%a#%s%a" - print e (if grded then "" else "!") Hstring.print hs + | Sy.Op Sy.Destruct hs, [e] -> + fprintf fmt "%a#%a" print e Hstring.print hs | Sy.In(lb, rb), [t] -> diff --git a/src/lib/frontend/parsed_interface.ml b/src/lib/frontend/parsed_interface.ml index 57e00ede67..6d69c801fa 100644 --- a/src/lib/frontend/parsed_interface.ml +++ b/src/lib/frontend/parsed_interface.ml @@ -337,5 +337,5 @@ let mk_match loc expr cases = let mk_algebraic_test loc expr cstr = mk_localized loc (PPisConstr (expr, cstr)) -let mk_algebraic_project loc ~guarded expr cstr = - mk_localized loc (PPproject (guarded, expr, cstr)) +let mk_algebraic_project loc expr cstr = + mk_localized loc (PPproject (expr, cstr)) diff --git a/src/lib/frontend/parsed_interface.mli b/src/lib/frontend/parsed_interface.mli index 440b5f12f5..3faf1bd301 100644 --- a/src/lib/frontend/parsed_interface.mli +++ b/src/lib/frontend/parsed_interface.mli @@ -258,4 +258,4 @@ val mk_match : Loc.t -> lexpr -> (pattern * lexpr) list -> lexpr val mk_algebraic_test : Loc.t -> lexpr -> string -> lexpr -val mk_algebraic_project : Loc.t -> guarded:bool -> lexpr -> string -> lexpr +val mk_algebraic_project : Loc.t -> lexpr -> string -> lexpr diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml index 8a5003fe87..65181541ce 100644 --- a/src/lib/frontend/typechecker.ml +++ b/src/lib/frontend/typechecker.ml @@ -494,7 +494,7 @@ module Env = struct let pp_profile = PFunction ([pur_ty], lbl_ty) in let mk_sy s = if record then (Symbols.Op (Access (Hstring.make s))) - else Symbols.destruct ~guarded:true s + else Symbols.destruct s in let kind = if record then RecordDestr else AdtDestr in add_logics ~kind env mk_sy [destr, ""] pp_profile loc @@ -621,7 +621,7 @@ let mk_adequate_app p s te_args ty logic_kind = | Env.RecordDestr, [te], _ -> TTdot(te, hp) - | Env.AdtDestr, [te], _ -> TTproject (true, te, hp) + | Env.AdtDestr, [te], _ -> TTproject (te, hp) | Env.RecordDestr, _, _ -> assert false | Env.RecordConstr, _, _ -> assert false @@ -951,14 +951,14 @@ let rec type_term ?(call_from_type_form=false) env f = | Ty.TypeClash(t1,t2) -> Errors.typing_error (Unification(t1,t2)) loc end - | PPproject (grded, t, lbl) -> + | PPproject (t, lbl) -> let te = type_term env t in begin try match Env.fresh_type env lbl loc with | _, {Env.args = [arg] ; result}, Env.AdtDestr -> Ty.unify te.c.tt_ty arg; - TTproject (grded, te, Hstring.make lbl), Ty.shorten result + TTproject (te, Hstring.make lbl), Ty.shorten result | _, {Env.args = [arg] ; result}, Env.RecordDestr -> Ty.unify te.c.tt_ty arg; @@ -1675,7 +1675,7 @@ let rec no_alpha_renaming_b ((up, m) as s) f = | PPisConstr (e, _) -> no_alpha_renaming_b s e - | PPproject (_, e, _) -> + | PPproject (e, _) -> no_alpha_renaming_b s e let rec alpha_renaming_b ((up, m) as s) f = @@ -1925,10 +1925,10 @@ let rec alpha_renaming_b ((up, m) as s) f = let cases' = if !same_cases then cases else cases' in { f with pp_desc = PPmatch(e', cases') } - | PPproject(grded, f1, a) -> + | PPproject(f1, a) -> let ff1 = alpha_renaming_b s f1 in if f1 == ff1 then f - else {f with pp_desc = PPproject(grded, ff1, a)} + else {f with pp_desc = PPproject(ff1, a)} | PPisConstr(f1, a) -> let ff1 = alpha_renaming_b s f1 in @@ -2089,8 +2089,8 @@ let rec mono_term {c = {tt_ty=tt_ty; tt_desc=tt_desc}; annot = id} = | TTite (cond, t1, t2) -> TTite (monomorphize_form cond, mono_term t1, mono_term t2) - | TTproject (grded, t, lbl) -> - TTproject (grded, mono_term t, lbl) + | TTproject (t, lbl) -> + TTproject (mono_term t, lbl) | TTmatch (e, pats) -> let e = mono_term e in let pats = List.rev_map (fun (p, f) -> p, mono_term f) (List.rev pats) in diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml index 66c95d0f82..fec249da7e 100644 --- a/src/lib/reasoners/adt.ml +++ b/src/lib/reasoners/adt.ml @@ -88,12 +88,12 @@ module Shostak (X : ALIEN) = struct not (Options.get_disable_adts ()) && match sy, ty with | Sy.Op (Sy.Constr _), Ty.Tadt _ -> true - | Sy.Op Sy.Destruct (_, guarded), _ -> - (* A guarded destructor isn't interpreted by the ADT theory. + | Sy.Op Sy.Destruct _, Ty.Tadt _ -> + (* A destructor is partially interpreted by the ADT theory. If we assume the tester of the constructor associated with this destructor, we propagate the non-guarded version of the destructor. See the documentation of [env.selectors] in [Adt_rel]. *) - not guarded + false | _ -> false let embed r = @@ -192,12 +192,7 @@ module Shostak (X : ALIEN) = struct in is_mine @@ Constr {c_name = hs; c_ty = ty; c_args}, ctx - | Sy.Op Sy.Destruct (hs, guarded), [e], _ -> - if not guarded then - let sel = Select {d_name = hs ; d_arg = e ; d_ty = ty} in - is_mine sel, ctx - else - X.term_embed t, ctx + | Sy.Op Sy.Destruct _, [_], _ -> X.term_embed t, ctx (* No risk ! if equal sel (embed sel_x) then X.term_embed t, ctx else sel_x, ctx (* canonization OK *) @@ -236,8 +231,7 @@ module Shostak (X : ALIEN) = struct | Alien r | Select { d_arg = r; _ } -> X.is_constant r - | Constr { c_args; _ } -> - List.for_all (fun (_, r) -> X.is_constant r) c_args + | Constr _ -> true [@@ocaml.ppwarning "TODO: not sure"] let fully_interpreted _ = diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index b5e49afa74..710b7c64a6 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -32,7 +32,6 @@ module X = Shostak.Combine module Th = Shostak.Adt type r = X.r -type uf = Uf.t module Ex = Explanation module E = Expr @@ -61,13 +60,7 @@ type t = constructors. The explanation justifies that any value assigned to the semantic value has to use a constructor lying in the domain. *) - (* TODO: rename this field. *) - seen_destr : SE.t; - (* Set of all the guarded destructors known by the theory. A guarded - destructor isn't interpreted by the ADT theory. - - This field is used to prevent transforming twice a guarded - destructor to its non-guarded version and for debugging purposes. *) + delayed : Rel_utils.Delayed.t; (* TODO: rename this field. *) seen_access : SE.t; @@ -83,30 +76,6 @@ type t = read to remember we have already forced a constructor because we have assumed its associated tester. *) - selectors : (E.t * Ex.t) list MHs.t MX.t; - (* Map of pending destructor equations. A destructor equation on an - ADT term [t] is an equation of the form: - d t = d' t - where [d] is a guarded destructor and [d'] its non-guarded version. - - More precisely, this map matches a class representative [r] with a map - of constructors of the ADT type [X.type_info r] to a list of - destructor equations of the form [d t = d' t] where [t] lies in the - class of [r]. If a class representative changes, the structure is - updated by [update_cs_modulo_eq]. - - Consider [d] a guarded destructor and [c] its associated constructor. - - - When we register the destructor application [d t] in [add_aux], we - produce an equation [d t = d' t] where [d'] is the non-guarded - version of [d]. If we don't already know that the value of [t] has - to use the constructor [c], we put the equation [d t = d' t] in this - map. Otherwise we propagate the equation to CC(X). - - - When we assume a tester on [c] (see [assume_is_constr]), we retrieve - and propagate to CC(X) all the pending destructor equations - associated with the constructor [c]. *) - size_splits : Numbers.Q.t; (* Product of the size of all the facts learnt by CS assumed in the theory. @@ -135,13 +104,37 @@ type t = content is propagated to the environment of CC(X). *) } +let calc_destructor d e uf = + let r, ex = Uf.find uf e in + match Th.embed r with + | Constr { c_args; _ } -> + begin match List.assoc d c_args with + | v -> Some (v, ex) + | exception Not_found -> None + end + + | _ -> + None + +let delayed_destructor uf op = function + | [e] -> + begin match op with + | Sy.Destruct d -> + calc_destructor d e uf + | _ -> assert false + end + | _ -> assert false + +let dispatch = function + | Symbols.Destruct _ -> Some delayed_destructor + | _ -> None + let empty classes = { classes; domains = MX.empty; - seen_destr = SE.empty; + delayed = Rel_utils.Delayed.create dispatch; seen_access = SE.empty; seen_testers = MX.empty; - selectors = MX.empty; size_splits = Numbers.Q.one; new_terms = SE.empty; pending_deds = []; @@ -171,18 +164,6 @@ module Debug = struct X.print r Fmt.(iter ~sep:(const string "|") HSS.iter Hstring.print) hss - let pp_selectors ppf (r, mhs) = - let pp_selector ppf (hs, l) = - let pp ppf (a, _) = - Fmt.pf ppf "(%a is %a) ==> %a" - X.print r - Hstring.print hs - E.print a - in - Fmt.(list ~sep:sp pp) ppf l - in - Fmt.iter_bindings MHs.iter pp_selector ppf mhs - let print_env loc env = if Options.get_debug_adt () then begin print_dbg ~flushed:false ~module_name:"Adt_rel" ~function_name:"print_env" @@ -193,10 +174,6 @@ module Debug = struct "@]@ @[-- seen testers ---------------------------@ "; print_dbg ~flushed:false ~header:false "%a" Fmt.(iter_bindings ~sep:cut MX.iter pp_testers) env.seen_testers; - print_dbg ~flushed:false ~header:false - "@]@ @[-- selectors ------------------------------@ "; - print_dbg ~flushed:false ~header:false "%a" - Fmt.(iter_bindings ~sep:cut MX.iter pp_selectors) env.selectors; print_dbg ~header:false "@]@ -------------------------------------------"; end @@ -354,100 +331,14 @@ let update_tester r hs env = let old = try MX.find r env.seen_testers with Not_found -> HSS.empty in {env with seen_testers = MX.add r (HSS.add hs old) env.seen_testers} -(* Check if [((_ is hs) r)] is [true]. *) -let trivial_tester r hs = - match Th.embed r with (* can filter further/better *) - | Adt.Constr { c_name; _ } -> Hstring.equal c_name hs - | _ -> false - -let constr_of_destr ty dest = - if Options.get_debug_adt () then - Printer.print_dbg - ~module_name:"Adt_rel" ~function_name:"constr_of_destr" - "ty = %a" Ty.print ty; - match ty with - | Ty.Tadt (name, params) -> - let cases = - match Ty.type_body name params with - | Ty.Adt cases -> cases - in - begin - try - List.find - (fun {Ty.destrs; _} -> - List.exists (fun (d, _) -> Hstring.equal dest d) destrs - )cases - with Not_found -> assert false (* invariant *) - end - | _ -> assert false - - -[@@ocaml.ppwarning "XXX improve. For each selector, store its \ - corresponding constructor when typechecking ?"] -let add_guarded_destr env uf t hs e t_ty = - if Options.get_debug_adt () then - Printer.print_dbg ~flushed:false - ~module_name:"Adt_rel" ~function_name:"add_guarded_destr" - "new (guarded) Destr: %a@ " E.print t; - let env = { env with seen_destr = SE.add t env.seen_destr } in - let {Ty.constr = c; _} = constr_of_destr (E.type_info e) hs in - let access = E.mk_term (Sy.destruct (Hs.view hs) ~guarded:false) [e] t_ty in - (* XXX : Never add non-guarded access to list of new terms ! - This may/will introduce bugs when instantiating - let env = {env with new_terms = SE.add access env.new_terms} in - *) - let is_c = E.mk_tester (Hstring.view c) e in - let eq = E.mk_eq access t ~iff:false in - if Options.get_debug_adt () then - Printer.print_dbg ~header:false - "associated with constr %a@,%a => %a" - Hstring.print c - E.print is_c - E.print eq; - let r_e, ex_e = try Uf.find uf e with Not_found -> assert false in - if trivial_tester r_e c || seen_tester r_e c env then - {env with pending_deds = - (Literal.LTerm eq, ex_e, Th_util.Other) :: env.pending_deds} - else - let m_e = try MX.find r_e env.selectors with Not_found -> MHs.empty in - let old = try MHs.find c m_e with Not_found -> [] in - { env with selectors = - MX.add r_e (MHs.add c ((eq, ex_e)::old) m_e) - env.selectors } - - -[@@ocaml.ppwarning "working with X.term_extract r would be sufficient ?"] -let add_aux env (uf:uf) (r:r) t = - if Options.get_disable_adts () then env - else - let { E.f = sy; xs; ty; _ } = E.term_view t in +let add env uf r t = + if Options.get_disable_adts () then env, [] + else begin + let delayed, eqs = Rel_utils.Delayed.add env.delayed uf r t in + let E.{ f = sy; ty; _ } = E.term_view t in let env = add_adt env uf t r sy ty in - match sy, xs with - | Sy.Op Sy.Destruct (hs, true), [e] -> - (* guarded *) - if Options.get_debug_adt () then - Printer.print_dbg - ~module_name:"Adt_rel" ~function_name:"add_aux" - "add guarded destruct: %a" E.print t; - if (SE.mem t env.seen_destr) then env - else add_guarded_destr env uf t hs e ty - - | Sy.Op Sy.Destruct (_, false), [_] -> - (* not guarded *) - if Options.get_debug_adt () then - Printer.print_dbg - ~module_name:"Adt_rel" ~function_name:"add_aux" - "[ADTs] add unguarded destruct: %a" E.print t; - { env with seen_access = SE.add t env.seen_access } - - | Sy.Op Sy.Destruct _, _ -> - (* The arity of the [Sy.Destruct] operator is 1. *) - assert false - - | _ -> env - -let add env (uf:uf) (r:r) t = - add_aux env (uf:uf) (r:r) t, [] + { env with delayed }, eqs + end (* Update the counter of case-split size in [env]. *) let count_splits env la = @@ -519,26 +410,6 @@ let add_diseq uf hss sm1 sm2 dep env eqs = | _ -> env, eqs -(* Helper function used in [assume_is_constr] and [assume_not_is_constr]. - Retrieves the pending destructor equations associated with the semantic - value [r] and the constructor [hs]. This function removes also these - equations from [env.selectors]. *) -let assoc_and_remove_selector hs r env = - try - let mhs = MX.find r env.selectors in - let deds = MHs.find hs mhs in - let mhs = MHs.remove hs mhs in - let env = - if MHs.is_empty mhs then - { env with selectors = MX.remove r env.selectors } - else - { env with selectors = MX.add r mhs env.selectors } - in - deds, env - - with Not_found -> - [], env - (* Assumes the tester `((_ is hs) r)` where [r] can be a constructor application or a uninterpreted semantic value. @@ -566,15 +437,7 @@ let assume_is_constr uf hs r dep env eqs = if seen_tester r hs env then env, eqs else - let deds, env = assoc_and_remove_selector hs r env in - let eqs = - List.fold_left - (fun eqs (ded, dep') -> - (Literal.LTerm ded, Ex.union dep dep', Th_util.Other) :: eqs - )eqs deds - in let env = update_tester r hs env in - let dom, ex = try MX.find r env.domains with Not_found -> @@ -600,8 +463,6 @@ let assume_not_is_constr uf hs r dep env eqs = | Adt.Constr{ c_name; _ } when Hs.equal c_name hs -> raise (Ex.Inconsistent (dep, env.classes)); | _ -> - - let _, env = assoc_and_remove_selector hs r env in let dom, ex = try MX.find r env.domains with Not_found -> @@ -681,46 +542,6 @@ let add_aux env r = added with function add. *) let add_rec env r = List.fold_left add_aux env (X.leaves r) -(* Update the field [env.selectors] when a Subst equality have - been propagated to CC(X). - - If [r2] becomes the class representative of [r1], this function is - called and [env.selectors] maps [r2] to the union of the old - selectors of [r2] and [r1]. *) -let update_cs_modulo_eq r1 r2 ex env eqs = - (* PB Here: even if Subst, we are not sure that it was - r1 |-> r2, because LR.mkv_eq may swap r1 and r2 *) - try - let old = MX.find r1 env.selectors in - if Options.get_debug_adt () then - Printer.print_dbg ~flushed:false - ~module_name:"Adt_rel" ~function_name:"update_cs_modulo_eq" - "update selectors modulo eq: %a |-> %a@ " - X.print r1 X.print r2; - let mhs = try MX.find r2 env.selectors with Not_found -> MHs.empty in - let eqs = ref eqs in - let _new = - MHs.fold - (fun hs l mhs -> - if trivial_tester r2 hs then begin - if Options.get_debug_adt () then - Printer.print_dbg - ~flushed:false ~header:false - "make deduction because %a ? %a is trivial@ " - X.print r2 Hs.print hs; - List.iter - (fun (a, dep) -> - eqs := (Literal.LTerm a, dep, Th_util.Other) :: !eqs) l; - end; - let l = List.rev_map (fun (a, dep) -> a, Ex.union ex dep) l in - MHs.add hs l mhs - )old mhs - in - if Options.get_debug_adt () then - Printer.print_dbg ~header:false ""; - { env with selectors = MX.add r2 _new env.selectors }, !eqs - with Not_found -> env, eqs - (* Remove duplicate literals in the list [la]. *) let remove_redundancies la = let cache = ref SLR.empty in @@ -739,6 +560,7 @@ let assume env uf la = env, { Sig_rel.assume = []; remove = [] } else let la = remove_redundancies la in (* should be done globally in CCX *) + let delayed, result = Rel_utils.Delayed.assume env.delayed uf la in let env = count_splits env la in let classes = Uf.cl_extract uf in let env = { env with classes = classes } in @@ -756,16 +578,10 @@ let assume env uf la = (fun (env,eqs) (a, b, c, d) -> Debug.assume a; match a, b, c, d with - | Xliteral.Eq(r1,r2), _, ex, orig -> + | Xliteral.Eq (r1, r2), _, ex, _ -> (* needed for models generation because fresh terms are not added with function add *) let env = add_rec (add_rec env r1) r2 in - let env, eqs = - if orig == Th_util.Subst then - update_cs_modulo_eq r1 r2 ex env eqs - else - env, eqs - in aux true r1 r2 ex env eqs (values_of (X.type_info r1)) | Xliteral.Distinct(false, [r1;r2]), _, ex, _ -> @@ -798,41 +614,72 @@ let assume env uf la = Printer.print_dbg ~module_name:"Adt_rel" ~function_name:"assume" "assume deduced %d equalities@ %a" (List.length eqs) (Printer.pp_list_no_space print) eqs; - env, { Sig_rel.assume = eqs; remove = [] } + let eqs = List.rev_append eqs result.assume in + { env with delayed }, { Sig_rel.assume = eqs; remove = [] } (* ################################################################ *) let two = Numbers.Q.from_int 2 +let constr_of_destr ty d = + match ty with + | Ty.Tadt (name, params) -> + begin + let Ty.Adt cases = Ty.type_body name params in + try + let r = + List.find + (fun Ty.{ destrs; _ } -> + List.exists (fun (d', _) -> Hstring.equal d d') destrs + ) cases + in + r.constr + with Not_found -> assert false + end + + | _ -> assert false + +exception Found of X.r * Hstring.t + +(* Pick a delayed destructor application in [env.delayed]. + + @raise Found (r, d) if there is a delayed application of the destructor + [d] on the semantic value [r]. *) +let pick_delayed_destructor env = + Rel_utils.Delayed.iter_delayed + (fun r sy _e -> + match sy with + | Sy.Destruct d -> + raise_notrace @@ Found (r, d) + | _ -> + () + ) env.delayed + (* Do a case-split by choosing a semantic value [r] and constructor [c] - for which there are pending destructor equations and propagate the + for which there are delayed destructor applications and propagate the literal [(not (_ is c) r)]. *) let case_split env _uf ~for_model = if Options.get_disable_adts () || not (Options.get_enable_adts_cs()) then [] - else - begin - assert (not for_model); - if Options.get_debug_adt () then Debug.print_env "before cs" env; - try - let r, mhs = MX.choose env.selectors in - if Options.get_debug_adt () then - Printer.print_dbg ~flushed:false - ~module_name:"Adt_rel" ~function_name:"case_split" - "found r = %a@ " X.print r; - let hs, _ = MHs.choose mhs in - if Options.get_debug_adt () then - Printer.print_dbg ~header:false - "found hs = %a" Hs.print hs; - (* CS on negative version would be better in general. *) - let cs = LR.mkv_builtin false (Sy.IsConstr hs) [r] in - [ cs, true, Th_util.CS (Th_util.Th_adt, two) ] - with Not_found -> - Debug.no_case_split (); - [] - end + else begin + assert (not for_model); + if Options.get_debug_adt () then Debug.print_env "before cs" env; + match pick_delayed_destructor env with + | exception Found (r, d) -> + if Options.get_debug_adt () then + Printer.print_dbg ~flushed:false + ~module_name:"Adt_rel" ~function_name:"case_split" + "found r = %a and d = %a@ " X.print r Hstring.print d; + (* CS on negative version would be better in general. *) + let c = constr_of_destr (X.type_info r) d in + let cs = LR.mkv_builtin false (Sy.IsConstr c) [r] in + [ cs, true, Th_util.CS (Th_util.Th_adt, two) ] + | () -> + Debug.no_case_split (); + [] + end let optimizing_objective _env _uf _o = None diff --git a/src/lib/reasoners/rel_utils.ml b/src/lib/reasoners/rel_utils.ml index 4ce89a0f87..c843b307a7 100644 --- a/src/lib/reasoners/rel_utils.ml +++ b/src/lib/reasoners/rel_utils.ml @@ -114,6 +114,9 @@ module Delayed : sig (** [assume] is a simple wrapper for [update] that is compatible with the [assume] signature of a relation. *) val assume : t -> Uf.t -> X.r Sig_rel.input list -> t * X.r Sig_rel.result + + (** [iter_delayed f t] iterates on the delayed applications of [t]. *) + val iter_delayed : (X.r -> Symbols.operator -> Expr.t -> unit) -> t -> unit end = struct module OMap = Map.Make(struct type t = Symbols.operator @@ -193,6 +196,9 @@ end = struct ) [] la in env, { Sig_rel.assume = assume_nontrivial_eqs eqs la; remove = [] } + + let iter_delayed f t = + MX.iter (fun r -> OMap.iter (fun op -> Expr.Set.iter (f r op))) t.used_by end module type Domain = sig diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 828697b15d..d3e22cdd60 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -634,9 +634,9 @@ module AEPrinter = struct | Sy.(Op (Constr _ as op)), _::_ -> Fmt.pf ppf "%a(%a)" Symbols.pp_ae_operator op Fmt.(list ~sep:comma pp) xs - | Sy.(Op Destruct (hs, grded)), [e] -> - Fmt.pf ppf "%a#%s%a" - pp e (if grded then "" else "!") Hstring.print hs + | Sy.(Op Destruct hs), [e] -> + Fmt.pf ppf "%a#%a" + pp e Hstring.print hs | Sy.Op op, [e1; e2] -> Fmt.pf ppf "(%a %a %a)" pp e1 Symbols.pp_ae_operator op pp e2 @@ -1953,8 +1953,8 @@ module Triggers = struct | { f = Op (Access _); _ }, _ -> -1 | _, { f = Op (Access _); _ } -> 1 - | { f = Op (Destruct (_,a1)) ; xs = [t1]; _ }, - { f = Op (Destruct (_,a2)) ; xs = [t2]; _ } -> + | { f = Op (Destruct a1) ; xs = [t1]; _ }, + { f = Op (Destruct a2) ; xs = [t2]; _ } -> let c = Stdlib.compare a1 a2 in (* should be Hstring.compare *) if c<>0 then c else cmp_trig_term t1 t2 @@ -2536,7 +2536,7 @@ let mk_match e cases = let ty = type_info e in let mk_destr = match ty with - | Ty.Tadt _ -> (fun hs -> Sy.destruct ~guarded:true (Hstring.view hs)) + | Ty.Tadt _ -> (fun hs -> Sy.destruct (Hstring.view hs)) | Ty.Trecord _ -> (fun hs -> Sy.Op (Sy.Access hs)) | Ty.Tsum _ -> (fun _hs -> assert false) (* no destructors for Tsum *) | _ -> assert false diff --git a/src/lib/structures/parsed.ml b/src/lib/structures/parsed.ml index 01a8077598..033ffc4fab 100644 --- a/src/lib/structures/parsed.ml +++ b/src/lib/structures/parsed.ml @@ -166,7 +166,7 @@ and pp_desc = | PPcast of lexpr * ppure_type | PPmatch of lexpr * (pattern * lexpr) list | PPisConstr of lexpr * string - | PPproject of bool * lexpr * string + | PPproject of lexpr * string let rec pp_lexpr fmt {pp_desc; _} = let open Format in @@ -231,7 +231,7 @@ let rec pp_lexpr fmt {pp_desc; _} = fprintf fmt "cast %a -> %a" pp_lexpr le pp_ppure_type ppt | PPmatch (_le, _plel) -> fprintf fmt "match" | PPisConstr (le, s) -> fprintf fmt "isConstr: %a %s" pp_lexpr le s - | PPproject (b, le, s) -> fprintf fmt "project: %b %a %s" b pp_lexpr le s + | PPproject (le, s) -> fprintf fmt "project: %a %s" pp_lexpr le s and pp_lexpr_list fmt tl = Format.fprintf fmt "@[%a@]" diff --git a/src/lib/structures/parsed.mli b/src/lib/structures/parsed.mli index 33c348ac22..8f7571decd 100644 --- a/src/lib/structures/parsed.mli +++ b/src/lib/structures/parsed.mli @@ -99,7 +99,7 @@ and pp_desc = | PPcast of lexpr * ppure_type | PPmatch of lexpr * (pattern * lexpr) list | PPisConstr of lexpr * string - | PPproject of bool * lexpr * string + | PPproject of lexpr * string val pp_lexpr : Format.formatter -> lexpr -> unit val pp_lexpr_list : Format.formatter -> lexpr list -> unit diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index dd31bf7a5e..d868f69406 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -39,7 +39,7 @@ type operator = (* ADTs *) | Access of Hstring.t | Record | Constr of Hstring.t (* enums, adts *) - | Destruct of Hstring.t * bool + | Destruct of Hstring.t (* Arrays *) | Get | Set (* BV *) @@ -150,7 +150,7 @@ let bitv s = in Bitv (String.length s, biv) let real r = Real (Q.of_string r) let constr s = Op (Constr (Hstring.make s)) -let destruct ~guarded s = Op (Destruct (Hstring.make s, guarded)) +let destruct s = Op (Destruct (Hstring.make s)) let mk_bound kind sort ~is_open ~is_lower = {kind; sort; is_open; is_lower} @@ -181,10 +181,9 @@ let compare_kinds k1 k2 = let compare_operators op1 op2 = Util.compare_algebraic op1 op2 (function - | Access h1, Access h2 | Constr h1, Constr h2 -> Hstring.compare h1 h2 - | Destruct (h1, b1), Destruct(h2, b2) -> - let c = Stdlib.compare b1 b2 in - if c <> 0 then c else Hstring.compare h1 h2 + | Access h1, Access h2 | Constr h1, Constr h2 + | Destruct h1, Destruct h2 -> + Hstring.compare h1 h2 | Extract (i1, j1), Extract (i2, j2) -> let r = Int.compare i1 i2 in if r = 0 then Int.compare j1 j2 else r @@ -360,9 +359,8 @@ module AEPrinter = struct (* DT theory *) | Record -> Fmt.pf ppf "@Record" | Access s -> Fmt.pf ppf "@Access_%a" Hstring.print s - | Constr s -> Hstring.print ppf s - | Destruct (s, g) -> - Fmt.pf ppf "%s%a" (if g then "" else "!") Hstring.print s + | Constr s + | Destruct s -> Hstring.print ppf s (* Float theory *) | Float -> Fmt.pf ppf "float" @@ -457,7 +455,7 @@ module SmtPrinter = struct (* DT theory *) | Record -> () - | Access s | Constr s | Destruct (s, _) -> Hstring.print ppf s + | Access s | Constr s | Destruct s -> Hstring.print ppf s (* Float theory *) | Float -> Fmt.pf ppf "ae.round" diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli index 40734ccb44..4834545ff9 100644 --- a/src/lib/structures/symbols.mli +++ b/src/lib/structures/symbols.mli @@ -39,7 +39,7 @@ type operator = (* ADTs *) | Access of Hstring.t | Record | Constr of Hstring.t (* enums, adts *) - | Destruct of Hstring.t * bool + | Destruct of Hstring.t (* Arrays *) | Get | Set (* BV *) @@ -164,7 +164,7 @@ val int : string -> t val bitv : string -> t val real : string -> t val constr : string -> t -val destruct : guarded:bool -> string -> t +val destruct : string -> t val mk_bound : bound_kind -> Ty.t -> is_open:bool -> is_lower:bool -> bound val mk_in : bound -> bound -> t val mk_maps_to : Var.t -> t diff --git a/src/lib/structures/typed.ml b/src/lib/structures/typed.ml index 0ba7a0a66d..8570b388f2 100644 --- a/src/lib/structures/typed.ml +++ b/src/lib/structures/typed.ml @@ -90,7 +90,7 @@ and 'a tt_desc = | TTnamed of Hstring.t * 'a atterm | TTite of 'a atform * 'a atterm * 'a atterm - | TTproject of bool * 'a atterm * Hstring.t + | TTproject of 'a atterm * Hstring.t | TTmatch of 'a atterm * (pattern * 'a atterm) list | TTform of 'a atform @@ -245,9 +245,9 @@ let rec print_term = | TTite(cond, t1, t2) -> fprintf fmt "(if %a then %a else %a)" print_formula cond print_term t1 print_term t2 - | TTproject (grded, t1, s) -> - fprintf fmt "%a#%s%s" - print_term t1 (if grded then "" else "!") (Hstring.view s) + | TTproject (t1, s) -> + fprintf fmt "%a#%s" + print_term t1 (Hstring.view s) | TTform f -> fprintf fmt "%a" print_formula f diff --git a/src/lib/structures/typed.mli b/src/lib/structures/typed.mli index 2b84ccad08..47ca2a3a4d 100644 --- a/src/lib/structures/typed.mli +++ b/src/lib/structures/typed.mli @@ -131,10 +131,8 @@ and 'a tt_desc = (** Conditional branching, of the form [TTite (condition, then_branch, else_branch)]. *) - | TTproject of bool * 'a atterm * Hstring.t - (** Field (conditional) access on ADTs. The boolean is true when the - projection is 'guarded' and cannot be simplified (because - functions are total) *) + | TTproject of 'a atterm * Hstring.t + (** Field (conditional) access on ADTs. *) | TTmatch of 'a atterm * (pattern * 'a atterm) list (** pattern matching on ADTs *) diff --git a/src/parsers/native_parser.mly b/src/parsers/native_parser.mly index 1c5ceda187..0058f761fe 100644 --- a/src/parsers/native_parser.mly +++ b/src/parsers/native_parser.mly @@ -448,7 +448,7 @@ simple_expr : { mk_algebraic_test ($startpos, $endpos) se id } | se = simple_expr SHARP label = ident - { mk_algebraic_project ($startpos, $endpos) ~guarded:true se label } + { mk_algebraic_project ($startpos, $endpos) se label } array_assignements: | assign = array_assignement { [assign] }