From 6c3ae05ed7f2456fa353912b3e845a741266b9a1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Wed, 7 Aug 2024 10:41:58 +0200 Subject: [PATCH 1/3] feat(shostak): Transparent abstracted constants This patch introduces a new type of leaf in the Shostak module, called *abstract leaves*. Abstract leaves behave like constant terms, and are intended to replace the `X.term_embed (E.fresh_name ty)` pattern where possible. An abstract leaf is created by calling `X.abstract` on an existing semantic value `r`. The abstract leaf `X.abstract r` is automatically defined to be equal to `r` when processed by the `Uf` and `Ccx` modules. The benefits of abstract leaves over fresh term constants are twofold: - With fresh constants, when the same semantic value is abstracted multiple times, a new constant is created for each abstraction. Semantically, this is correct; however, this causes the introduction of unnecessary constants in the union-find that will just end up in the same equivalence class. With abstract leaves, abstracting the same semantic value multiple times always returns the same constant. - With fresh constants, an additional equation between the new constant and the original term to abstract must be kept and processed separately. Since abstract leaves embed their definition, the additional equations can be introduced automatically by the `Uf` and `Ccx` modules and do not need to be carried separately. Abstract leaves are currently only used by the AC theory. In the future, it is intended to be used as a basis for implementing application of interpreted-but-not-solvable functions to semantic values (so that for instance we can denote `bv2nat(r)` where `r` is a semantic value). While it would be straightforward to adapt abstract leaves to be able to create terminal leaves for `bv2nat(r)` (without definitional equations), we want congruence closure and computation (so that `bv2nat(x @ y)` automatically becomes `bv2nat(x) * 2^n + bv2nat(y)`) to work for such leaves. This require additional adaptations to CC(X), and is expected to need abstract leaves to enforce an AC(X)-compatible ordering. --- src/lib/reasoners/ac.ml | 50 ++++++------------ src/lib/reasoners/arith.ml | 9 +--- src/lib/reasoners/ccx.ml | 9 +++- src/lib/reasoners/intervalCalculus.ml | 10 ++-- src/lib/reasoners/shostak.ml | 75 +++++++++++++++++++++++---- src/lib/reasoners/sig.mli | 38 ++++++++++++++ src/lib/reasoners/uf.ml | 71 +++++++++++++++---------- src/lib/reasoners/uf.mli | 2 +- src/lib/structures/expr.ml | 8 --- src/lib/structures/expr.mli | 6 --- src/lib/structures/symbols.ml | 7 +-- src/lib/structures/symbols.mli | 17 ------ 12 files changed, 180 insertions(+), 122 deletions(-) diff --git a/src/lib/reasoners/ac.ml b/src/lib/reasoners/ac.ml index 95645ba25..6ce81f2a8 100644 --- a/src/lib/reasoners/ac.ml +++ b/src/lib/reasoners/ac.ml @@ -183,10 +183,10 @@ module Make (X : Sig.X) = struct presentation in the paper to accomodate those differences, globally, between the implementation and theoretical description of AC(X). - More precisely, `abstract2` will abstract terms that *contain* AC leaves - when they appear as argument of an AC symbol. This ensures that AC terms - satisfy the T_AC definition from page 22 of the paper, although - correctness of the corresponding abstraction process has not been proven. + More precisely, `abstract2` will abstract all AC leaves that appear in the + arguments of an AC symbol. This ensures that AC terms satisfy the T_AC + definition from page 22 of the paper, although correctness of the + corresponding abstraction process has not been formally proven. See also https://github.com/OCamlPro/alt-ergo/issues/989 [1]: Canonized Rewriting and Ground AC Completion Modulo Shostak Theories: @@ -196,42 +196,24 @@ module Make (X : Sig.X) = struct Volume 8, Issue 3. doi:10.2168/LMCS-8(3:16)2012 https://arxiv.org/pdf/1207.3262.pdf *) - 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; _ } -> - (* 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_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_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 - | _, { ty; _ } -> - let k = Expr.fresh_ac_name ty in - let eq = Expr.mk_eq ~iff:false k t in - X.term_embed k, eq::acc - - else - r, acc + let rec abstract2 sy r = + match List.find (is_other_ac_symbol sy) (X.leaves r) with + | ac_lv -> + (* Abstraction in depth: [f(x, y) + 1] -> [@ac(f(x, y) + 1] + and not [@ac(f(x, y) + 1)]. *) + abstract2 sy (X.subst ac_lv (X.abstract ~kind:Ac ac_lv) r) + | exception Not_found -> r let make t = match Expr.term_view t with | { Expr.f = sy; xs = [a;b]; ty; _ } when Sy.is_ac sy -> let ra, ctx1 = X.make a in let rb, ctx2 = X.make b in - let ra, ctx = abstract2 sy a ra (ctx1 @ ctx2) in - let rb, ctx = abstract2 sy b rb ctx in - let rxs = [ ra,1 ; rb,1 ] in - X.ac_embed {h=sy; l=compact (fold_flatten sy (fun x -> x) rxs); t=ty; - distribute = true}, - ctx + let l = flatten sy (rb, 1) @@ flatten sy (ra, 1) [] in + let l = List.map (fun (r, n) -> (abstract2 sy r, n)) l in + let l = compact (fold_flatten sy (fun x -> x) l) in + X.ac_embed {h=sy; l; t=ty;distribute = true}, + ctx1 @ ctx2 | {xs; _} -> Printer.print_err "AC theory expects only terms with 2 arguments; \ diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml index 01ab0206e..9f681604b 100644 --- a/src/lib/reasoners/arith.ml +++ b/src/lib/reasoners/arith.ml @@ -452,12 +452,7 @@ module Shostak List.fold_left (fun acc (_, x) -> max acc (nb_vars_in_alien x)) acc l let contains_a_fresh_alien xp = - List.exists - (fun x -> - match X.term_extract x with - | Some t, _ -> E.is_fresh_ac_name t - | _ -> false - ) (X.leaves xp) + List.exists (X.is_abstract ~kind:Ac) (X.leaves xp) let has_ac p kind = List.exists @@ -540,7 +535,7 @@ module Shostak List.fold_left (fun (l, sb) (b, y) -> if X.ac_extract y != None && X.str_cmp y x > 0 then - let k = X.term_embed (E.fresh_ac_name Ty.Tint) in + let k = X.abstract ~kind:Ac y in (b, k) :: l, (y, embed k)::sb else (b, y) :: l, sb) ([], []) l diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml index 5642c89d4..c5453c0b5 100644 --- a/src/lib/reasoners/ccx.ml +++ b/src/lib/reasoners/ccx.ml @@ -489,7 +489,14 @@ module Main : S = struct let { E.xs; _ } = E.term_view t in let env = List.fold_left (fun env t -> add_term env facts t ex) env xs in (* we update uf and use *) - let nuf, ctx = Uf.add env.uf t in + let nuf, abs, ctx = Uf.add env.uf t in + (* process definitional equality of abstracted terms *) + List.iter (fun r -> + match X.abstract_extract r with + | Some r' -> + add_fact facts (LSem (LR.mkv_eq r r'), Ex.empty, Th_util.Other) + | None -> assert false + ) abs; Debug.make_cst t ctx; List.iter (fun a -> add_fact facts (LTerm a, ex, Th_util.Other)) ctx; (*or Ex.empty ?*) diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml index aeb8ca415..1d6d322ea 100644 --- a/src/lib/reasoners/intervalCalculus.ml +++ b/src/lib/reasoners/intervalCalculus.ml @@ -2234,7 +2234,7 @@ let domain_matching _lem_name tr sbt env uf optimized = | E.Interval (t, lb, ub) -> let tt = E.apply_subst sbt t in assert (E.is_ground tt); - let uf, _ = Uf.add uf tt in + let uf, _, _ = Uf.add uf tt in let rr, _ex = Uf.find uf tt in let p = poly_of rr in let p', c', d = P.normal_form_pos p in @@ -2247,7 +2247,7 @@ let domain_matching _lem_name tr sbt env uf optimized = | E.NotTheoryConst t -> let tt = E.apply_subst sbt t in - let uf, _ = Uf.add uf tt in + let uf, _, _ = Uf.add uf tt in if X.leaves (fst (Uf.find uf tt)) == [] || X.leaves (fst (X.make tt)) == [] then raise (Sem_match_fails env); @@ -2255,7 +2255,7 @@ let domain_matching _lem_name tr sbt env uf optimized = | E.IsTheoryConst t -> let tt = E.apply_subst sbt t in - let uf, _ = Uf.add uf tt in + let uf, _, _ = Uf.add uf tt in let r, _ = X.make tt in if X.leaves r != [] then raise (Sem_match_fails env); idoms, maps_to, env, uf @@ -2265,8 +2265,8 @@ let domain_matching _lem_name tr sbt env uf optimized = let y = E.apply_subst sbt y in if not (terms_linear_dep env [x;y]) then raise (Sem_match_fails env); - let uf, _ = Uf.add uf x in - let uf, _ = Uf.add uf y in + let uf, _, _ = Uf.add uf x in + let uf, _, _ = Uf.add uf y in idoms, maps_to, env, uf )(Var.Map.empty, [], env, uf) tr.E.semantic in diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml index 8b308859b..9f332da4a 100644 --- a/src/lib/reasoners/shostak.ml +++ b/src/lib/reasoners/shostak.ml @@ -27,6 +27,22 @@ (*** Combination module of Shostak theories ***) +let equal_abs_kind k1 k2 = + match k1, k2 with + | Sig.Ac, Sig.Ac -> true + +let hash_abs_kind k = + match k with + | Sig.Ac -> 1 + +let compare_abs_kind k1 k2 = + match k1, k2 with + | Sig.Ac, Sig.Ac -> 0 + +let pp_abs_kind ppf k = + match k with + | Sig.Ac -> Fmt.pf ppf "ac" + [@@@ocaml.warning "-60"] module rec CX : sig include Sig.X @@ -51,6 +67,7 @@ struct type rview = | Term of Expr.t + | Abstract of Sig.abs_kind * CX.r | Ac of AC.t | Arith of ARITH.t | Records of RECORDS.t @@ -72,6 +89,7 @@ struct | Bitv t -> fprintf fmt "%a" BITV.print t | Adt t -> fprintf fmt "%a" ADT.print t | Term t -> fprintf fmt "%a" Expr.print t + | Abstract (k, t) -> fprintf fmt "@@%a(%a)" pp_abs_kind k CX.print t | Ac t -> fprintf fmt "%a" AC.print t end else begin @@ -86,6 +104,8 @@ struct fprintf fmt "Adt(%s):[%a]" ADT.name ADT.print t | Term t -> fprintf fmt "FT:[%a]" Expr.print t + | Abstract (k, t) -> + fprintf fmt "K:%a[%a]" pp_abs_kind k CX.print t | Ac t -> fprintf fmt "Ac:[%a]" AC.print t end @@ -165,6 +185,8 @@ struct | Bitv x -> 3 + 10 * BITV.hash x | Adt x -> 6 + 10 * ADT.hash x | Ac ac -> 9 + 10 * AC.hash ac + | Abstract (k, t) -> + 7 + 10 * (5003 * (hash_abs_kind k) + CX.hash t) | Term t -> 8 + 10 * Expr.hash t in abs res @@ -176,6 +198,8 @@ struct | Bitv x, Bitv y -> BITV.equal x y | Adt x, Adt y -> ADT.equal x y | Term x, Term y -> Expr.equal x y + | Abstract (kx, x), Abstract (ky, y) -> + equal_abs_kind kx ky && CX.equal x y | Ac x, Ac y -> AC.equal x y | _ -> false @@ -214,6 +238,16 @@ struct let term_embed t = hcons {v = Term t; id = -1000 (* dummy *)} + let abstract ~kind arg = + (* No need to nest abstractions + XXX: would it be OK to abstract terms into themselves? *) + let arg = + match arg.v with + | Abstract (_, arg) -> arg + | _ -> arg + in + hcons { v = Abstract (kind, arg); id = -1000 (* dummy *) } + let extract1 = function { v=Arith r; _ } -> Some r | _ -> None let extract2 = function { v=Records r; _ } -> Some r | _ -> None let extract3 = function { v=Bitv r; _ } -> Some r | _ -> None @@ -223,6 +257,18 @@ struct | { v = Ac t; _ } -> Some t | _ -> None + let is_abstract ?kind = function + | { v = Abstract (k, _); _ } -> ( + match kind with + | None -> true + | Some k' -> equal_abs_kind k k' + ) + | _ -> false + + let abstract_extract = function + | { v = Abstract (_, r); _ } -> Some r + | _ -> None + let term_extract r = match r.v with | Arith _ -> ARITH.term_extract r @@ -230,6 +276,7 @@ struct | Bitv _ -> BITV.term_extract r | Adt _ -> ADT.term_extract r | Ac _ -> None, false (* SYLVAIN : TODO *) + | Abstract _ -> None, false | Term t -> Some t, true let to_model_term r = @@ -240,7 +287,7 @@ struct | Bitv _ -> BITV.to_model_term r | Adt _ -> ADT.to_model_term r | Term t when Expr.is_model_term t -> Some t - | Ac _ | Term _ -> None + | Abstract _ | Ac _ | Term _ -> None in Option.bind res @@ fun t -> assert (Expr.is_model_term t); @@ -256,15 +303,17 @@ struct | { v = Adt t; _ } -> ADT.type_info t | { v = Ac x; _ } -> AC.type_info x | { v = Term t; _ } -> Expr.type_info t + | { v = Abstract (_, t); _ } -> CX.type_info t (* Constraint that must be maintained: - all theories should have Xi < Term < Ac *) + all theories should have Xi < Term < Abstract < Ac *) let theory_num x = match x with | Ac _ -> -1 - | Term _ -> -2 - | Arith _ -> -3 - | Records _ -> -4 - | Bitv _ -> -5 + | Abstract _ -> -2 + | Term _ -> -3 + | Arith _ -> -4 + | Records _ -> -5 + | Bitv _ -> -6 | Adt _ -> -7 let compare_tag a b = theory_num a - theory_num b @@ -278,6 +327,9 @@ struct | Bitv _, Bitv _ -> BITV.compare a b | Adt _, Adt _ -> ADT.compare a b | Term x, Term y -> Expr.compare x y + | Abstract (kx, x), Abstract (ky, y) -> + let c = compare_abs_kind kx ky in + if c <> 0 then c else CX.str_cmp x y | Ac x, Ac y -> AC.compare x y | va, vb -> compare_tag va vb @@ -322,7 +374,7 @@ struct | Bitv t -> BITV.leaves t | Adt t -> ADT.leaves t | Ac t -> r :: (AC.leaves t) - | Term _ -> [r] + | Term _ | Abstract _ -> [r] let is_constant r = match r.v with @@ -338,7 +390,7 @@ struct | Symbols.(True | False), [] -> true | _ -> false end - | Ac _ -> false + | Abstract _ | Ac _ -> false let subst p v r = if equal p v then r @@ -348,6 +400,7 @@ struct | Bitv t -> BITV.subst p v t | Adt t -> ADT.subst p v t | Ac t -> if equal p r then v else AC.subst p v t + | Abstract _ -> if equal p r then v else r | Term _ -> if equal p r then v else r let make t = @@ -416,7 +469,7 @@ struct ADT.is_mine_symb sb) let is_a_leaf r = match r.v with - | Term _ | Ac _ -> true + | Term _ | Ac _ | Abstract _ -> true | _ -> false let color ac = @@ -448,7 +501,7 @@ struct | Records a -> RECORDS.abstract_selectors a acc | Bitv a -> BITV.abstract_selectors a acc | Adt a -> ADT.abstract_selectors a acc - | Term _ -> a, acc + | Term _ | Abstract _ -> a, acc | Ac a -> AC.abstract_selectors a acc let abstract_equality a b = @@ -483,7 +536,7 @@ struct let sbs = List.filter (fun (p,_) -> match p.v with - | Ac _ -> true | Term _ -> SX.mem p original + | Ac _ | Abstract _ -> true | Term _ -> SX.mem p original | _ -> Printer.print_err "%a" CX.print p; assert false diff --git a/src/lib/reasoners/sig.mli b/src/lib/reasoners/sig.mli index 3050e1f23..7c780ccce 100644 --- a/src/lib/reasoners/sig.mli +++ b/src/lib/reasoners/sig.mli @@ -28,6 +28,12 @@ type 'a ac = {h: Symbols.t ; t: Ty.t ; l: ('a * int) list; distribute: bool} +type abs_kind = + Ac (** Semantic value abstracted for AC(X) purposes. *) +(** Type of abstractions that can be used in [abstract]. Used to distinguish + the reason for which a semantic value was abstracted, which some code + cares about (see {!module-Arith}). *) + type 'a solve_pb = { sbt : ('a * 'a) list; eqs : ('a * 'a) list } module type SHOSTAK = sig @@ -184,6 +190,38 @@ module type X = sig val ac_extract : r -> (r ac) option + val abstract : kind:abs_kind -> r -> r + (** [abstract ~kind r] returns an abstracted constant representing [r]. + + The abstract constant [abstract ~kind r] is {e definitionally equal} to + [r]: when processed by the {!module-Uf} and {!module-Ccx} modules in any + context, the equality [r = abstract ~kind r] is introduced automatically. + + Calling [abstract ~kind r] multiple times with the same [kind] and the + same [r] always returns the same abstracted constant. + + Abstracted constants, like terms, are terminal leaves: the only leaf of + [abstract ~kind r] is [abstract ~kind r] itself. In particular, + substituting the leaves of [r] does not impact [abstract ~kind r]. + *) + + val is_abstract : ?kind:abs_kind -> r -> bool + (** [is_abstract ?kind r] returns [true] if [r] is an abstracted constant + created with {!val-abstract} with the provided [kind] (if any). + *) + + val abstract_extract : r -> r option + (** [abstract_extract r] returns the inner abstracted semantic value + embedded in [r], if any. + + If [abstract_extract r] is [Some r'], then [r] is definitionally equal to + [r'], that is, the equation [r = r'] holds in all contexts. + + {b Note}: While [abstract_extract (abstract ~kind r)] and [r] are + guaranteed to be definitionally equal, they are not, in general, + guaranteed to be equal as semantic values according to {!val-equal}. + *) + val color : (r ac) -> r val fully_interpreted : Symbols.t -> bool diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index 46f330070..e5b3a0789 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -587,7 +587,7 @@ module Env = struct with GlobalDomains.Inconsistent ex -> raise (Ex.Inconsistent (ex, cl_extract env)) - let init_leaf env p = + let init_leaf env abs p = Debug.init_leaf p; let in_repr = MapX.mem p env.repr in let rp, ex_rp = @@ -600,6 +600,11 @@ module Env = struct | Some t, true when not (ME.mem t mk_env) -> ME.add t p mk_env | _ -> mk_env in + let abs = + match X.abstract_extract rp with + | Some _ when not in_repr -> rp :: abs + | Some _ | None -> abs + in let env = { env with make = make; @@ -620,21 +625,28 @@ module Env = struct else update_neqs p rp Ex.empty env } in Debug.check_invariants "init_leaf" env; - env + env, abs + + let init_leaves env abs v = + let env, abs = + List.fold_left + (fun (env, abs) lv -> init_leaf env abs lv) + (env, abs) + (X.leaves v) + in + init_leaf env abs v - let init_leaves env v = - let env = List.fold_left init_leaf env (X.leaves v) in - init_leaf env v + let is_dyn_leaf r = + Option.is_some (X.ac_extract r) || X.is_abstract r - let init_new_ac_leaves env mkr = + let init_new_dyn_leaves env mkr = List.fold_left - (fun env x -> - match X.ac_extract x with - | None -> env - | Some _ -> - if MapX.mem x env.repr then env - else init_leaves env x - ) env (X.leaves mkr) + (fun (env, abs) x -> + if is_dyn_leaf x && not (MapX.mem x env.repr) then + init_leaves env abs x + else + env, abs + ) (env, []) (X.leaves mkr) let init_term env t = let mkr, ctx = X.make t in @@ -650,7 +662,8 @@ module Env = struct if MapX.mem rp env.neqs then env.neqs (* pourquoi ce test *) else MapX.add rp MapL.empty env.neqs} in - (init_new_ac_leaves env mkr), ctx + let env, abs = init_new_dyn_leaves env mkr in + env, abs, ctx let head_cp eqs env pac ({ Sig.h ; _ } as ac) v dep = try (*if RS.mem h env.ac_rs then*) @@ -792,21 +805,27 @@ module Env = struct update_aux dep neqs_to_up env, tch let apply_sigma eqs env tch ((p, v, dep) as sigma) = - let env = init_leaves env p in - let env = init_leaves env v in + let env, abs = init_leaves env [] p in + let env, abs = init_leaves env abs v in let env = apply_sigma_ac eqs env sigma in let env, touched_sigma, tch = apply_sigma_uf env sigma tch in - up_uf_rs dep env ((p, touched_sigma, v) :: tch) + let env, tch = up_uf_rs dep env ((p, touched_sigma, v) :: tch) in + List.iter (fun r -> + match X.abstract_extract r with + | Some r' -> Queue.push (r, r', Ex.empty) eqs + | None -> assert false + ) abs; + env, tch end let add env t = Options.tool_req 3 "TR-UFX-Add"; - if ME.mem t env.make then env, [] + if ME.mem t env.make then env, [], [] else - let env, l = Env.init_term env t in + let env, abs, l = Env.init_term env t in Debug.check_invariants "add" env; - env, l + env, abs, l let ac_solve eqs dep (env, tch) (p, v) = Debug.ac_solve p v dep; @@ -859,9 +878,9 @@ let union env r1 r2 dep = Options.tool_req 3 "TR-UFX-Union"; let equations = Queue.create () in Queue.push (r1,r2, dep) equations; - let env, res = ac_x equations env [] in + let env, tch = ac_x equations env [] in Debug.check_invariants "union" env; - env, res + env, tch let union env r1 r2 dep = Timers.with_timer Timers.M_UF Timers.F_union @@ fun () -> @@ -890,7 +909,7 @@ let rec distinct env rl dep = with Not_found -> MapL.add d uex mdis in - let env = Env.init_leaf env rr in + let env, _ = Env.init_leaf env [] rr in let env = {env with neqs = MapX.add rr mdis env.neqs} in env, MapX.add rr uex mapr, (rr, ex, mapr)::newds ) @@ -992,8 +1011,8 @@ let empty = ac_rs = RS.empty } in - let env, _ = add env E.vrai in - let env, _ = add env E.faux in + let env, _, _ = add env E.vrai in + let env, _, _ = add env E.faux in distinct env [X.top; X.bot] Ex.empty let make uf t = ME.find t uf.make @@ -1065,7 +1084,7 @@ let assign_next env = we will not modify env in this function !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *) - let env, _ = add env s in (* important for termination *) + let env, _, _ = add env s in (* important for termination *) let eq = LX.view (LX.mk_eq rep (make env s)) in [eq, is_cs, Th_util.CS (Th_util.Th_UF, Numbers.Q.one)], env in diff --git a/src/lib/reasoners/uf.mli b/src/lib/reasoners/uf.mli index f231441e6..ecbea6b56 100644 --- a/src/lib/reasoners/uf.mli +++ b/src/lib/reasoners/uf.mli @@ -117,7 +117,7 @@ end module LX = Shostak.L val empty : t -val add : t -> Expr.t -> t * Expr.t list +val add : t -> Expr.t -> t * r list * Expr.t list val mem : t -> Expr.t -> bool diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index e07fc3e1c..1bbe89621 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -987,14 +987,6 @@ let fresh_name ty = let mk_abstract ty = mk_term (Sy.name ~ns:Abstract @@ Id.Namespace.Abstract.fresh ()) [] ty -let fresh_ac_name ty = - mk_term (Sy.name ~ns:Fresh_ac @@ Id.Namespace.Internal.fresh ()) [] ty - -let is_fresh_ac_name t = - match t with - | { f = Name { ns = Fresh_ac; _ }; xs = []; _ } -> true - | _ -> false - let positive_int i = mk_term (Sy.int i) [] Ty.Tint let int i = diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index 8c639480c..a68714e67 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -254,12 +254,6 @@ val real : string -> t val bitv : string -> Ty.t -> t val fresh_name : Ty.t -> t -(** Special names used for AC(X) abstraction. - These corresponds to the K sort in the AC(X) paper. *) - -val fresh_ac_name : Ty.t -> t -val is_fresh_ac_name : t -> bool - val mk_abstract : Ty.t -> t (** [mk_abstract ty] creates an abstract model term of type [ty]. This function is intended to be used only in models. *) diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index 3b00b1e45..e443d2ce6 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -75,7 +75,7 @@ type form = type name_kind = Ac | Other -type name_space = User | Internal | Fresh | Fresh_ac | Skolem | Abstract +type name_space = User | Internal | Fresh | Skolem | Abstract let compare_name_space ns1 ns2 = match ns1, ns2 with @@ -91,10 +91,6 @@ let compare_name_space ns1 ns2 = | Fresh, _ -> -1 | _, Fresh -> 1 - | Fresh_ac, Fresh_ac -> 0 - | Fresh_ac, _ -> -1 - | _, Fresh_ac -> 1 - | Skolem, Skolem -> 0 | Skolem, _ -> -1 | _, Skolem -> 1 @@ -132,7 +128,6 @@ let mangle ns s = | User -> s | Internal -> ".!" ^ s | Fresh -> ".k" ^ s - | Fresh_ac -> ".K" ^ s | Skolem -> ".?__" ^ s | Abstract -> "@a" ^ s diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli index 0aedea950..8611d1dcf 100644 --- a/src/lib/structures/symbols.mli +++ b/src/lib/structures/symbols.mli @@ -104,28 +104,11 @@ type name_space = 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 From 6d1f64319dc36cf40506311ab92594a7bf86f099 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Wed, 7 Aug 2024 16:50:57 +0200 Subject: [PATCH 2/3] Fix order --- src/lib/reasoners/shostak.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml index 9f332da4a..c9f28faca 100644 --- a/src/lib/reasoners/shostak.ml +++ b/src/lib/reasoners/shostak.ml @@ -306,11 +306,11 @@ struct | { v = Abstract (_, t); _ } -> CX.type_info t (* Constraint that must be maintained: - all theories should have Xi < Term < Abstract < Ac *) + all theories should have Xi < Abstract < Term < Ac *) let theory_num x = match x with | Ac _ -> -1 - | Abstract _ -> -2 - | Term _ -> -3 + | Term _ -> -2 + | Abstract _ -> -3 | Arith _ -> -4 | Records _ -> -5 | Bitv _ -> -6 @@ -328,8 +328,10 @@ struct | Adt _, Adt _ -> ADT.compare a b | Term x, Term y -> Expr.compare x y | Abstract (kx, x), Abstract (ky, y) -> - let c = compare_abs_kind kx ky in - if c <> 0 then c else CX.str_cmp x y + (* Make sure that new abstractions are smaller, i.e. + old abstractions are rewritten into new abstractions. *) + let c = Int.compare y.id x.id in + if c <> 0 then c else compare_abs_kind kx ky | Ac x, Ac y -> AC.compare x y | va, vb -> compare_tag va vb From 921916db042397f2e69ac152e44dc258d87e5356 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <129742207+bclement-ocp@users.noreply.github.com> Date: Mon, 19 Aug 2024 14:33:49 +0200 Subject: [PATCH 3/3] Update src/lib/reasoners/ac.ml Co-authored-by: Pierrot --- src/lib/reasoners/ac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lib/reasoners/ac.ml b/src/lib/reasoners/ac.ml index 6ce81f2a8..955019970 100644 --- a/src/lib/reasoners/ac.ml +++ b/src/lib/reasoners/ac.ml @@ -199,7 +199,7 @@ module Make (X : Sig.X) = struct let rec abstract2 sy r = match List.find (is_other_ac_symbol sy) (X.leaves r) with | ac_lv -> - (* Abstraction in depth: [f(x, y) + 1] -> [@ac(f(x, y) + 1] + (* Abstraction in depth: [f(x, y) + 1] -> [@ac(f(x, y)) + 1] and not [@ac(f(x, y) + 1)]. *) abstract2 sy (X.subst ac_lv (X.abstract ~kind:Ac ac_lv) r) | exception Not_found -> r