Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

refactor(BV): Track domains for uninterpreted leaves only #1004

Merged
merged 1 commit into from
Jan 9, 2024
Merged

refactor(BV): Track domains for uninterpreted leaves only #1004

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
260 changes: 153 additions & 107 deletions src/lib/reasoners/bitv_rel.ml
View file
Open in desktop
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
Halbaroth marked this conversation as resolved.
Show resolved Hide resolved

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 *)
Halbaroth marked this conversation as resolved.
Show resolved Hide resolved
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
Loading