Skip to content

Commit

Permalink
refactor(BV): Track domains for uninterpreted leaves only (#1004)
Browse files Browse the repository at this point in the history 
This patch changes the internal representation of domains in the
bitvector relations. Without the patch, we are keeping track of domains
for *all* bit-vector terms, which is correct but wasteful. With the
patch, we only track the domains of (currently) uninterpreted class
representatives, and rebuild the domain associated with other terms
on-the-fly before propagation.

This avoids carrying around huge domain maps with a potentially large
amount of duplication, and allow to share propagations between terms
that include identical sub-terms immediately without a round-trip
through Uf (without the patch, if we learn that `0 @ x -> 01??`, it does
not immediately propagate that `1 @ x -> 11??`; we first have to assert
`x<2,2> = 1` which gets solved into the substitution `x |-> 1 @ x'` and
we only learn `11 @ x' -> 11??` when performing the substitution). On
the other hand, it means that `Domains.get` and `Domains.update` are a
bit more expensive now.

Since the `Congruence` is now only used for constraints, and not for
domains, we only need to add the arguments of the constraints to the
`Congruence` (which should also be a slight performance boost).  Other
changes to the use of the `Congruence` module are needed to fix the
mismatch between what is stored in the `Domains` (whose keys are now
uninterpreted terms) and the `Constraints` (the actual arguments of the
constraints in the original problem). There is one exception: we now add
the arguments of `Distinct` to the congruence, which is required for
completeness because the terms that we generate during case splits are
not guaranteed to already exist (in fact, in general they don't, since
we create 1-bit extractions that have no reason to be in the original
problem).

Note that there is also a small bugfix in `Congruence`: when performing
a substitution we need to remove the old terms, otherwise we will forget
dependencies if we ever add it back later.
  • Loading branch information
@bclement-ocp
bclement-ocp authored Jan 9, 2024
1 parent 214ea7c commit bd9f133
Show file tree
Hide file tree
Showing 2 changed files with 167 additions and 108 deletions.
260 changes: 153 additions & 107 deletions src/lib/reasoners/bitv_rel.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -111,9 +111,6 @@ module Domains : sig
Use this to ensure that the representation is always normalized.
[v] must have an existing associated domain (possibly unconstrained)
before calling [subst]. Call [update] beforehand.
The explanation [ex] justifies the equality [p = v].
@raise Bitlist.Inconsistent if this causes any domain in [d] to become
Expand All @@ -131,7 +128,12 @@ module Domains : sig
end = struct
type t =
{ bitlists : Bitlist.t MX.t
(** Mapping from semantic values to their bitlist domain. *)
(** Mapping from semantic values to their bitlist domain.
Note: this mapping only contains domain for leaves (i.e. uninterpreted
terms or AC symbols); domains associated with more complex semantic
values are rebuilt on-the-fly using the structure of said semantic
values. *)
; changed : SX.t
(** Elements whose domain has changed since last propagation. *)
}
Expand All @@ -144,7 +146,7 @@ end = struct
ppf t.bitlists
let empty = { bitlists = MX.empty ; changed = SX.empty }

let update ex r t bl =
let update_leaf ex r t bl =
let changed = ref false in
let bitlists =
MX.update r (function
Expand All @@ -171,45 +173,67 @@ end = struct
let changed = if !changed then SX.add r t.changed else t.changed in
{ changed; bitlists }

let get r t =
let update_signed ex { Bitv.value; negated } t bl =
let bl = if negated then Bitlist.lognot bl else bl in
update_leaf ex value t bl

let update ex r t bl =
fst @@ List.fold_left (fun (t, bl) { Bitv.bv; sz } ->
(* Extract the bitlist associated with the current component *)
let mid = Bitlist.width bl - sz in
let bl_tail =
if mid = 0 then Bitlist.empty else
Bitlist.extract bl 0 (mid - 1)
in
let bl = Bitlist.extract bl mid (Bitlist.width bl - 1) in

match bv with
| Bitv.Cte z ->
(* Nothing to update, but still check for consistency! *)
ignore @@ Bitlist.intersect bl (Bitlist.exact sz z Ex.empty) ex;
t, bl_tail
| Other r -> update_signed ex r t bl, bl_tail
| Ext (r, r_size, i, j) ->
(* r<i, j> = bl -> r = ?^(r_size - j - 1) @ bl @ ?^i *)
assert (i + r_size - j - 1 + Bitlist.width bl = r_size);
let hi = Bitlist.unknown (r_size - j - 1) Ex.empty in
let lo = Bitlist.unknown i Ex.empty in
update_signed ex r t Bitlist.(hi @ bl @ lo), bl_tail
) (t, bl) (Shostak.Bitv.embed r)

let get_leaf r t =
try MX.find r t.bitlists with
| Not_found ->
match X.type_info r with
| Tbitv n -> Bitlist.unknown n Explanation.empty
| _ -> assert false

let get_signed { Bitv.value; negated } t =
let bl = get_leaf value t in
if negated then Bitlist.lognot bl else bl

let get r t =
List.fold_left (fun bl { Bitv.bv; sz } ->
Bitlist.concat bl @@
match bv with
| Bitv.Cte z -> Bitlist.exact sz z Ex.empty
| Other r -> get_signed r t
| Ext (r, _r_size, i, j) -> Bitlist.extract (get_signed r t) i j
) Bitlist.empty (Shostak.Bitv.embed r)

let subst ex rr nrr t =
match MX.find rr t.bitlists with
| bl ->
let has_changed = ref (SX.mem rr t.changed) in
let bitlists =
MX.update nrr (function
| Some bl' as o ->
let bl'' = Bitlist.intersect bl bl' ex in
(* Keep simpler explanations, and don't loop adding the domain to
the changed set infinitely. *)
if Bitlist.equal bl' bl'' then
o
else (
has_changed := true;
if Options.get_debug_bitv () then
Printer.print_dbg
~module_name:"Bitv_rel" ~function_name:"Domain.subst"
"domain shrunk for %a: %a -> %a"
X.print nrr Bitlist.pp bl' Bitlist.pp bl'';
Some (Bitlist.intersect bl bl' ex)
)
| None ->
(* We require that [nrr] has a domain before calling [subst]. *)
Printer.print_err
"Bitv_rel: substituting %a -> %a without domain"
X.print rr X.print nrr;
assert false
) @@ MX.remove rr t.bitlists
(* Note: even if [rr] had changed its domain, we don't need to keep that
information because if the constraints that used to apply to [rr] were
not already valid, they will be marked as fresh in the [Constraints.t]
after substitution there and propagated already. *)
let t =
{ changed = SX.remove rr t.changed
; bitlists = MX.remove rr t.bitlists
}
in
let changed = SX.remove rr t.changed in
let changed = if !has_changed then SX.add nrr changed else changed in
{ changed ; bitlists }
update ex nrr t bl
| exception Not_found -> t

let choose_changed t =
Expand Down Expand Up @@ -481,6 +505,11 @@ module Constraints : sig
Fresh constraints are constraints that were never propagated yet. *)

val fold_r : (X.r -> 'a -> 'a) -> t -> 'a -> 'a
(** [fold_r f cs acc] folds [f] over any representative [r] that is currently
associated with a constraint (i.e. at least one constraint currently
applies to [r]). *)

val propagate : t -> X.r -> Domains.t -> Domains.t
(** [propagate cs r dom] propagates the constraints associated with [r] in the
constraint set [cs] and returns the new domain map after propagation. *)
Expand Down Expand Up @@ -568,50 +597,48 @@ end = struct
let acc = CS.fold f bcs.fresh acc in
{ bcs with fresh = CS.empty }, acc

let fold_r f bcs acc =
MX.fold (fun r _ acc -> f r acc) bcs.cs_map acc

let propagate bcs r dom =
match MX.find r bcs.cs_map with
| cs -> CS.fold Constraint.propagate cs dom
| exception Not_found -> dom
end

let extract_constraints bcs uf r t =
(* 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 =
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
Constraints.add bcs @@
add_constraint (bcs, cgr) @@
{ repr = Constraint.hcons @@ Bnot (r, rx) ; ex = exx }
| { f = Op BVand; xs = [ x; y ]; _ } ->
let rx, exx = Uf.find uf x
and ry, exy = Uf.find uf y in
Constraints.add bcs @@
add_constraint (bcs, cgr) @@
{ repr = Constraint.hcons @@ Band (r, rx, ry) ; ex = Ex.union exx exy }
| { f = Op BVor; xs = [ x; y ]; _ } ->
let rx, exx = Uf.find uf x
and ry, exy = Uf.find uf y in
Constraints.add bcs @@
add_constraint (bcs, cgr) @@
{ repr = Constraint.hcons @@ Bor (r, rx, ry) ; ex = Ex.union exx exy }
| { f = Op BVxor; xs = [ x; y ]; _ } ->
let rx, exx = Uf.find uf x
and ry, exy = Uf.find uf y in
let xs = SX.singleton r in
let xs = if SX.mem rx xs then SX.remove rx xs else SX.add rx xs in
let xs = if SX.mem ry xs then SX.remove ry xs else SX.add ry xs in
Constraints.add bcs @@
add_constraint (bcs, cgr) @@
{ repr = Constraint.hcons @@ Bxor xs ; ex = Ex.union exx exy }
| _ -> bcs

(** [abstract_bitlist r ex] builds a bitlist representation of the semantic
bit-vector value [r] *)
let abstract_bitlist =
let rec aux = function
| [] -> Bitlist.empty
| { Bitv.bv = Bitv.Cte n; sz } :: bs ->
Bitlist.(exact sz n Ex.empty @ aux bs)
| { sz; bv = (Other _ | Ext _) } :: bs ->
Bitlist.(unknown sz Ex.empty @ aux bs)
in fun bs -> Bitlist.add_explanation (aux bs)
| _ -> (bcs, cgr)

let rec mk_eq ex lhs w z =
match lhs with
Expand Down Expand Up @@ -666,12 +693,12 @@ let add_eqs =
includes constraints that changed due to substitutions)
- The constraints involving variables whose domain changed since the last
propagation *)
let propagate =
let propagate cgr =
let rec propagate changed bcs dom =
match Domains.choose_changed dom with
| r, dom -> (
propagate (SX.add r changed) bcs @@
Constraints.propagate bcs r dom
Congruence.fold_parents (Constraints.propagate bcs) cgr r dom
)
| exception Not_found -> changed, dom
in
Expand Down Expand Up @@ -709,31 +736,32 @@ let assume env uf la =
| Th_util.CS (Th_bitv, n) -> Q.(ss * n)
| _ -> ss
in
let is_1bit r =
match X.type_info r with
| Tbitv 1 -> true
| _ -> false
in
match a, orig with
| L.Eq (rr, nrr), Subst when is_bv_r rr ->
let cc, acc =
Congruence.subst rr nrr cgr (fun rr nrr (bcs, dom) ->
let bl =
abstract_bitlist (Shostak.Bitv.embed nrr) Ex.empty
in
let dom = Domains.update Ex.empty nrr dom bl in
( Constraints.subst ex rr nrr bcs
, Domains.subst ex rr nrr dom )
) (bcs, dom)
in (cc, acc, ss)
| L.Distinct (false, [rr; nrr]), NCS (Th_bitv, _) ->
(* We don't support [distinct] in general yet, but we must
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)
| 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.
Note that for 1-bit vectors (i.e. booleans), we have `x <> y`
iff `x = not y`. *)
assert Stdlib.(X.type_info rr = Ty.Tbitv 1);
let drr = abstract_bitlist (Shostak.Bitv.embed rr) Ex.empty in
let dnrr = abstract_bitlist (Shostak.Bitv.embed nrr) Ex.empty in
let dom = Domains.update Ex.empty rr dom drr in
let dom = Domains.update Ex.empty nrr dom dnrr in
let bcs =
Constraints.add bcs @@
We are a bit more general and support it for 1-bit vectors, for
which `distinct` can be expressed using `bvnot`.
Note that we are not guaranteed that the arguments are already
in normal form! *)
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) @@
{ repr = Constraint.hcons @@ Bnot (rr, nrr) ; ex }
in
(cgr, (bcs, dom), ss)
Expand All @@ -742,7 +770,7 @@ let assume env uf la =
(env.congruence, (env.constraints, env.domain), env.size_splits)
la
in
let eqs, constraints, domain = propagate constraints domain in
let eqs, constraints, domain = propagate congruence constraints domain in
if Options.get_debug_bitv () && not (Lists.is_empty eqs) then (
Printer.print_dbg
~module_name:"Bitv_rel" ~function_name:"assume"
Expand Down Expand Up @@ -770,35 +798,51 @@ let case_split env _uf ~for_model =
[]
else
(* Look for representatives with minimal, non-fully known, domain size.
We first look among the constrained variables, then if there are no
constrained variables, all the remaining variables.
[nunk] is the number of unknown bits. *)
let f_acc r bl acc =
let nunk = Bitlist.num_unknown bl in
if nunk = 0 then
acc
else
match acc with
| Some (nunk', _) when nunk > nunk' -> acc
| Some (nunk', xs) when nunk = nunk' ->
Some (nunk', SX.add r xs)
| _ -> Some (nunk, SX.singleton r)
in
let _, candidates =
match
Domains.fold (fun r bl acc ->
let nunk = Bitlist.num_unknown bl in
if nunk = 0 then
acc
else
match acc with
| Some (nunk', _) when nunk > nunk' -> acc
| Some (nunk', xs) when nunk = nunk' ->
Some (nunk', SX.add r xs)
| _ -> Some (nunk, SX.singleton r)
) env.domain None
Constraints.fold_r (fun r acc ->
List.fold_left (fun acc { Bitv.bv; _ } ->
match bv with
| Bitv.Cte _ -> acc
| Other r | Ext (r, _, _, _) ->
let bl = Domains.get r.value env.domain in
f_acc r.value bl acc
) acc (Shostak.Bitv.embed r)
) env.constraints None
with
| Some (nunk, xs) -> nunk, xs
| None -> 0, SX.empty
| None ->
match Domains.fold f_acc env.domain None with
| Some (nunk, xs) -> nunk, xs
| None -> 0, SX.empty
in
(* For now, just pick a value for the most significant bit. *)
match SX.choose candidates with
| r ->
let biv = Shostak.Bitv.embed r in
let rec aux = function
| [] -> assert false
| { Bitv.bv = Bitv.Cte _; _ } :: biv -> aux biv
| part :: _ ->
Bitv.extract part.sz (part.sz - 1) (part.sz - 1) [ part ]
let bl = Domains.get r env.domain in
let w = Bitlist.width bl in
let unknown = Z.extract (Z.lognot @@ Bitlist.bits_known bl) 0 w in
let bitidx = Z.numbits unknown - 1 in
let lhs =
Shostak.Bitv.is_mine @@
Bitv.extract w bitidx bitidx (Shostak.Bitv.embed r)
in
let lhs = Shostak.Bitv.is_mine @@ aux biv in
(* Just always pick zero for now. *)
let zero = Shostak.Bitv.is_mine Bitv.[ { bv = Cte Z.zero ; sz = 1 } ] in
if Options.get_debug_bitv () then
Expand All @@ -811,19 +855,21 @@ let case_split env _uf ~for_model =
let add env uf r t =
let delayed, eqs = Rel_utils.Delayed.add env.delayed uf r t in
let env, eqs =
if is_bv_r r then
try
let bcs = extract_constraints env.constraints uf r t in
let dr = abstract_bitlist (Shostak.Bitv.embed r) Ex.empty in
let dom = Domains.update Ex.empty r env.domain dr in
let congruence = Congruence.add r env.congruence in
let eqs', bcs, dom = propagate bcs dom in
{ env with congruence ; constraints = bcs ; domain = dom },
List.rev_append eqs' eqs
with Bitlist.Inconsistent ex ->
raise @@ Ex.Inconsistent (ex, Uf.cl_extract uf)
else
env, eqs
match X.type_info r with
| Tbitv n -> (
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 },
List.rev_append eqs' eqs
with Bitlist.Inconsistent ex ->
raise @@ Ex.Inconsistent (ex, Uf.cl_extract uf)
)
| _ -> env, eqs
in
{ env with delayed }, eqs

Expand Down
Loading

0 comments on commit bd9f133

Please sign in to comment.