From 187ff41e855525bdd1e2160194c0330f3e2f75cd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Wed, 6 Dec 2023 17:23:56 +0100 Subject: [PATCH] refactor(BV): Fold `Congruence` into `Constraints` In #944, the `Congruence` module was added to simplify handling dependences for both domains and constraints, because we tracked domains separately for all terms. After #1004, we now track domains only for uninterpreted leaves, and the `Congruence` module is only used for `Constraints`. This leads to a sort of double indirection: the `Congruence` module keeps track of reverse uninterpreted leaves -> class representative dependencies, and then the `Constraints` module keeps track of reverse class representative -> constraint dependencies. This patch removes the `Congruence` module entirely; instead, the `Constraints` module is now keeping track of reverse uninterpreted leaves -> constraint dependencies directly. Further refactoring work will move the `Congruence` module to `Rel_utils` as it can be a generally useful module for other theories. --- src/lib/reasoners/bitv_rel.ml | 100 +++++++++++------------- src/lib/reasoners/rel_utils.ml | 137 --------------------------------- 2 files changed, 44 insertions(+), 193 deletions(-) diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml index 1f26eb58c2..0f1c68b219 100644 --- a/src/lib/reasoners/bitv_rel.ml +++ b/src/lib/reasoners/bitv_rel.ml @@ -33,7 +33,6 @@ module Ex = Explanation module Sy = Symbols module X = Shostak.Combine module L = Xliteral -module Congruence = Rel_utils.Congruence (* Currently we only compute, but in the future we may want to perform the same simplifications as in [Bitv.make]. We currently don't, because we don't @@ -280,8 +279,7 @@ module type Constraint = sig The explanation [ex] justifies the equality [p = v]. *) - val fold_deps : (X.r -> 'a -> 'a) -> t -> 'a -> 'a - (** [fold_deps f c acc] accumulates [f] over the arguments of [c]. *) + val fold_leaves : (X.r -> 'a -> 'a) -> t -> 'a -> 'a type domain @@ -381,25 +379,25 @@ end = struct let subst_repr rr nrr = function | Band (x, y, z) -> - let x = if X.equal x rr then nrr else x - and y = if X.equal y rr then nrr else y - and z = if X.equal z rr then nrr else z in + let x = X.subst rr nrr x + and y = X.subst rr nrr y + and z = X.subst rr nrr z in Band (x, y, z) | Bor (x, y, z) -> - let x = if X.equal x rr then nrr else x - and y = if X.equal y rr then nrr else y - and z = if X.equal z rr then nrr else z in + let x = X.subst rr nrr x + and y = X.subst rr nrr y + and z = X.subst rr nrr z in Bor (x, y, z) | Bxor xs -> Bxor ( SX.fold (fun r xs -> - let r = if X.equal r rr then nrr else r in + let r = X.subst rr nrr r in if SX.mem r xs then SX.remove r xs else SX.add r xs ) xs SX.empty ) | Bnot (x, y) -> - let x = if X.equal x rr then nrr else x - and y = if X.equal y rr then nrr else y in + let x = X.subst rr nrr x + and y = X.subst rr nrr y in Bnot (x, y) (* The explanation justifies why the constraint holds. *) @@ -426,6 +424,11 @@ end = struct let acc = f y acc in acc + let fold_leaves f c acc = + fold_deps (fun r acc -> + List.fold_left (fun acc r -> f r acc) acc (X.leaves r) + ) c acc + type domain = Domains.t let propagate { repr; ex } dom = @@ -595,13 +598,13 @@ end = struct CS.fold (fun cs (cs_map, cs_set, fresh) -> let fresh = CS.remove cs fresh in let cs_set = CS.remove cs cs_set in - let cs_map = Constraint.fold_deps (cs_remove cs) cs cs_map in + let cs_map = Constraint.fold_leaves (cs_remove cs) cs cs_map in let cs' = Constraint.subst ex rr nrr cs in if CS.mem cs' cs_set then cs_map, cs_set, fresh else let cs_set = CS.add cs' cs_set in - let cs_map = Constraint.fold_deps (cs_add cs') cs' cs_map in + let cs_map = Constraint.fold_leaves (cs_add cs') cs' cs_map in (cs_map, cs_set, CS.add cs' fresh) ) ids (bcs.cs_map, bcs.cs_set, bcs.fresh) in @@ -614,9 +617,7 @@ end = struct bcs else let cs_set = CS.add c bcs.cs_set in - let cs_map = - Constraint.fold_deps (cs_add c) c bcs.cs_map - in + let cs_map = Constraint.fold_leaves (cs_add c) c bcs.cs_map in let fresh = CS.add c bcs.fresh in { cs_set ; cs_map ; fresh } @@ -633,32 +634,26 @@ end = struct | exception Not_found -> dom end -(* Add one constraint and register its arguments as relevant for congruence *) -let add_constraint (bcs, cgr) c = - let bcs = Constraints.add bcs c in - let cgr = Constraint.fold_deps Congruence.add c cgr in - (bcs, cgr) - -let extract_constraints (bcs, cgr) uf r t = +let extract_constraints bcs uf r t = match E.term_view t with (* BVnot is already internalized in the Shostak but we want to know about it without needing a round-trip through Uf *) | { f = Op BVnot; xs = [ x ] ; _ } -> let rx, exx = Uf.find uf x in - add_constraint (bcs, cgr) @@ Constraint.bvnot ~ex:exx r rx + Constraints.add bcs @@ Constraint.bvnot ~ex:exx r rx | { f = Op BVand; xs = [ x; y ]; _ } -> let rx, exx = Uf.find uf x and ry, exy = Uf.find uf y in - add_constraint (bcs, cgr) @@ Constraint.bvand ~ex:(Ex.union exx exy) r rx ry + Constraints.add bcs @@ Constraint.bvand ~ex:(Ex.union exx exy) r rx ry | { f = Op BVor; xs = [ x; y ]; _ } -> let rx, exx = Uf.find uf x and ry, exy = Uf.find uf y in - add_constraint (bcs, cgr) @@ Constraint.bvor ~ex:(Ex.union exx exy) r rx ry + Constraints.add bcs @@ Constraint.bvor ~ex:(Ex.union exx exy) r rx ry | { f = Op BVxor; xs = [ x; y ]; _ } -> let rx, exx = Uf.find uf x and ry, exy = Uf.find uf y in - add_constraint (bcs, cgr) @@ Constraint.bvxor ~ex:(Ex.union exx exy) r rx ry - | _ -> (bcs, cgr) + Constraints.add bcs @@ Constraint.bvxor ~ex:(Ex.union exx exy) r rx ry + | _ -> bcs let rec mk_eq ex lhs w z = match lhs with @@ -713,13 +708,12 @@ let add_eqs = includes constraints that changed due to substitutions) - The constraints involving variables whose domain changed since the last propagation *) -let propagate cgr = +let propagate = let rec propagate changed bcs dom = match Domains.choose_changed dom with - | r, dom -> ( - propagate (SX.add r changed) bcs @@ - Congruence.fold_parents (Constraints.propagate bcs) cgr r dom - ) + | r, dom -> + propagate (SX.add r changed) bcs @@ + Constraints.propagate bcs r dom | exception Not_found -> changed, dom in fun bcs dom -> @@ -735,22 +729,20 @@ type t = { delayed : Rel_utils.Delayed.t ; domain : Domains.t ; constraints : Constraints.t - ; congruence : Congruence.t ; size_splits : Q.t } let empty _ = { delayed = Rel_utils.Delayed.create dispatch ; domain = Domains.empty ; constraints = Constraints.empty - ; congruence = Congruence.empty ; size_splits = Q.one } let assume env uf la = let delayed, result = Rel_utils.Delayed.assume env.delayed uf la in - let (congruence, domain, constraints, eqs, size_splits) = + let (domain, constraints, eqs, size_splits) = try - let (congruence, (constraints, domain), size_splits) = - List.fold_left (fun (cgr, (bcs, dom), ss) (a, _root, ex, orig) -> + let ((constraints, domain), size_splits) = + List.fold_left (fun ((bcs, dom), ss) (a, _root, ex, orig) -> let ss = match orig with | Th_util.CS (Th_bitv, n) -> Q.(ss * n) @@ -764,10 +756,8 @@ let assume env uf la = match a, orig with | L.Eq (rr, nrr), Subst when is_bv_r rr -> let dom = Domains.subst ex rr nrr dom in - let cgr, bcs = - Congruence.subst rr nrr cgr (Constraints.subst ex) bcs - in - (cgr, (bcs, dom), ss) + let bcs = Constraints.subst ex rr nrr bcs in + ((bcs, dom), ss) | L.Distinct (false, [rr; nrr]), _ when is_1bit rr -> (* We don't (yet) support [distinct] in general, but we must support it for case splits to avoid looping. @@ -780,16 +770,16 @@ let assume env uf la = let rr, exrr = Uf.find_r uf rr in let nrr, exnrr = Uf.find_r uf nrr in let ex = Ex.union ex (Ex.union exrr exnrr) in - let bcs, cgr = - add_constraint (bcs, cgr) @@ Constraint.bvnot ~ex rr nrr + let bcs = + Constraints.add bcs @@ Constraint.bvnot ~ex rr nrr in - (cgr, (bcs, dom), ss) - | _ -> (cgr, (bcs, dom), ss) + ((bcs, dom), ss) + | _ -> ((bcs, dom), ss) ) - (env.congruence, (env.constraints, env.domain), env.size_splits) + ((env.constraints, env.domain), env.size_splits) la in - let eqs, constraints, domain = propagate congruence constraints domain in + let eqs, constraints, domain = propagate constraints domain in if Options.get_debug_bitv () && not (Lists.is_empty eqs) then ( Printer.print_dbg ~module_name:"Bitv_rel" ~function_name:"assume" @@ -798,7 +788,7 @@ let assume env uf la = ~module_name:"Bitv_rel" ~function_name:"assume" "bitlist constraints: @[%a@]" Constraints.pp constraints; ); - (congruence, domain, constraints, eqs, size_splits) + (domain, constraints, eqs, size_splits) with Bitlist.Inconsistent ex -> raise @@ Ex.Inconsistent (ex, Uf.cl_extract uf) in @@ -808,7 +798,7 @@ let assume env uf la = let result = { result with assume = List.rev_append assume result.assume } in - { delayed ; constraints ; domain ; congruence ; size_splits }, result + { delayed ; constraints ; domain ; size_splits }, result let query _ _ _ = None @@ -879,11 +869,9 @@ let add env uf r t = try let dr = Bitlist.unknown n Ex.empty in let dom = Domains.update Ex.empty r env.domain dr in - let (bcs, congruence) = - extract_constraints (env.constraints, env.congruence) uf r t - in - let eqs', bcs, dom = propagate congruence bcs dom in - { env with congruence ; constraints = bcs ; domain = dom }, + let bcs = extract_constraints env.constraints uf r t in + let eqs', bcs, dom = propagate bcs dom in + { env with constraints = bcs ; domain = dom }, List.rev_append eqs' eqs with Bitlist.Inconsistent ex -> raise @@ Ex.Inconsistent (ex, Uf.cl_extract uf) diff --git a/src/lib/reasoners/rel_utils.ml b/src/lib/reasoners/rel_utils.ml index 3705683715..6687c0c156 100644 --- a/src/lib/reasoners/rel_utils.ml +++ b/src/lib/reasoners/rel_utils.ml @@ -192,140 +192,3 @@ end = struct in env, { Sig_rel.assume = assume_nontrivial_eqs eqs la; remove = [] } end - -module Congruence : sig - (** The [Congruence] module implements a simil-congruence closure algorithm on - semantic values. - - It provides an interface to register some semantic values of interest, and - for applying a callback when the representative of those registered values - change. - *) - - type t - (** The type of congruences. *) - - val empty : t - (** The empty congruence. *) - - val add : X.r -> t -> t - (** [add r t] registers the semantic value [r] in the congruence. *) - - val remove : X.r -> t -> t - (** [remove r t] unregisters the semantic value [r] from the congruence. - - Note that if substitutions have been applied to the congruence after a - value has been added, those same substitutions must be applied to the - semantic value prior to calling [remove], or [Invalid_argument] will be - raised. - - @raise [Invalid_argument] if [r] is not a registered semantic value. *) - - val subst : X.r -> X.r -> t -> (X.r -> X.r -> 'a -> 'a) -> 'a -> t * 'a - (** [subst p v t f x] performs a local congruence closure of the - substitution [p -> v]. - - More precisely, it will fold [f] over the pairs [(rr, nrr)] such that: - - [rr] was registered in the congruence - - [nrr] is [X.subst p v rr] - - For each such pair, [rr] is then unregistered from the congruence, and - [nrr] is registered instead. - - [f] is intended to perform a substitution operation on the type ['a], - merging the values associated with [rr] into the values associated with - [nrr]. *) - - val fold_parents : (X.r -> 'a -> 'a) -> t -> X.r -> 'a -> 'a - (** [fold_parents f t r acc] folds function [f] over all the registered terms - whose current representative contains [r] as a leaf. *) -end = struct - module SX = Shostak.SXH - module MX = Shostak.MXH - - type t = - { parents : SX.t MX.t - (** Map from leaves to terms that contain them as a leaf. - - [p] is in [parents(x)] => [x] is in [leaves(p)] *) - ; registered : SX.t - (** The set of terms we care about. If [x] is in [registered], - then [x] is also in [parents(y)] for each [y] in [leaves(x)]. *) - } - - let empty = { parents = MX.empty ; registered = SX.empty } - - let fold_parents f { parents; _ } r acc = - match MX.find r parents with - | deps -> SX.fold f deps acc - | exception Not_found -> acc - - let add r t = - if SX.mem r t.registered then - t - else - let parents = - List.fold_left (fun parents leaf -> - MX.update leaf (function - | Some deps -> Some (SX.add r deps) - | None -> Some (SX.singleton r) - ) parents - ) t.parents (X.leaves r) - in - { parents ; registered = SX.add r t.registered } - - let remove r t = - if SX.mem r t.registered then - let parents = - List.fold_left (fun parents leaf -> - MX.update leaf (function - | Some deps -> - let deps = SX.remove r deps in - if SX.is_empty deps then None else Some deps - | None -> - (* [r] is in registered, and [leaf] is in [leaves(r)], so - [r] must be in [parents(leaf)]. *) - assert false - ) parents - ) t.parents (X.leaves r) - in - { parents ; registered = SX.remove r t.registered } - else - invalid_arg "Congruence.remove" - - let subst rr nrr cgr f t = - match MX.find rr cgr.parents with - | rr_deps -> - let cgr = { cgr with parents = MX.remove rr cgr.parents } in - SX.fold (fun r (cgr, t) -> - let r' = X.subst rr nrr r in - (* [r] contains [rr] as a leaf by definition *) - assert (not (X.equal r r')); - - (* Update the other leaves *) - let parents = - List.fold_left (fun parents other_leaf -> - if X.equal other_leaf rr then - parents - else - MX.update other_leaf (function - | Some deps -> - let deps = SX.remove r deps in - if SX.is_empty deps then None else Some deps - | None -> assert false - ) parents - ) cgr.parents (X.leaves r) - in - - (* It is no longer here, but it could be added back later -- let's not - skip it! *) - let registered = SX.remove r cgr.registered in - - (* Add the new representative to the congruence if needed *) - let cgr = add r' { parents ; registered } in - - (* Propagate the substitution *) - cgr, f r r' t - ) rr_deps (cgr, t) - | exception Not_found -> cgr, t -end