From 4f40796ad665efb814463d76c2ed4cc327ed88d9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Tue, 5 Mar 2024 14:19:57 +0100 Subject: [PATCH] feat(BV,CP): Use a FIFO queue for constraint propagation This patch changes the bit-vector propagator to use a FIFO queue to select which propagator to run. Using a FIFO queue gives fairness guarantees on the constraints that get propagated, and does not depend on hash-consing shenanigans as in the current implementation. The implementation is a simple wrapper around the `Queue` module from the stdlib and a hash table to ensure uniqueness of constraints in the queue. --- src/lib/dune | 2 +- src/lib/reasoners/bitv_rel.ml | 70 +++++++++++++++++++++------ src/lib/reasoners/rel_utils.ml | 86 +++++++++++++++++----------------- src/lib/util/uqueue.ml | 65 +++++++++++++++++++++++++ src/lib/util/uqueue.mli | 60 ++++++++++++++++++++++++ 5 files changed, 226 insertions(+), 57 deletions(-) create mode 100644 src/lib/util/uqueue.ml create mode 100644 src/lib/util/uqueue.mli diff --git a/src/lib/dune b/src/lib/dune index 56ea4c9a95..3391e92faf 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -58,7 +58,7 @@ Expr Var Ty Typed Xliteral ModelMap Id Objective Literal ; util Emap Gc_debug Hconsing Hstring Heap Lists Loc - MyUnix Numbers + MyUnix Numbers Uqueue Options Timers Util Vec Version Steps Printer My_zip Theories ) diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml index 698ac1a885..c7dbb445d9 100644 --- a/src/lib/reasoners/bitv_rel.ml +++ b/src/lib/reasoners/bitv_rel.ml @@ -135,6 +135,10 @@ module Domains = Rel_utils.Domains_make(Domain) module Constraint : sig include Rel_utils.Constraint + val equal : t -> t -> bool + + val hash : t -> int + val bvand : X.r -> X.r -> X.r -> t (** [bvand x y z] is the constraint [x = y & z] *) @@ -238,6 +242,10 @@ end = struct let compare { tag = t1; _ } { tag = t2; _ } = Stdlib.compare t1 t2 + let equal t1 t2 = Int.equal t1.tag t2.tag + + let hash t1 = Hashtbl.hash t1.tag + let subst rr nrr c = hcons @@ subst_repr rr nrr c.repr @@ -387,6 +395,24 @@ let add_eqs = fun acc x bl -> aux x (Bitlist.width bl) acc bl +type any_constraint = + | Constraint of Constraint.t Rel_utils.explained + | Structural of X.r + +module QC = Uqueue.Make(struct + type t = any_constraint + + let equal a b = + match a, b with + | Constraint ca, Constraint cb -> Constraint.equal ca.value cb.value + | Constraint _, Structural _ | Structural _, Constraint _ -> false + | Structural xa, Structural xb -> X.equal xa xb + + let hash = function + | Constraint c -> 2 * Constraint.hash c.value + | Structural r -> 2 * X.hash r + 1 + end) + (* Propagate: - The constraints that were never propagated since they were added @@ -395,23 +421,39 @@ let add_eqs = Iterate until fixpoint is reached. *) let propagate = - let rec propagate changed bcs dom = - match Constraints.next_pending bcs with - | { value; explanation = ex }, bcs -> + let touch bcs queue r = + QC.push queue (Structural r); + Constraints.iter_parents (fun c -> QC.push queue (Constraint c)) r bcs + in + let rec propagate queue changed bcs dom = + match QC.pop queue with + | Constraint { Rel_utils.value; explanation = ex } -> let dom = Constraint.propagate ~ex value dom in - propagate changed bcs dom - | exception Not_found -> - match Domains.choose_changed dom with - | r, dom -> - propagate (SX.add r changed) (Constraints.notify r bcs) dom - | exception Not_found -> - changed, bcs, dom + Domains.iter_changed (touch bcs queue) dom; + propagate queue changed bcs (Domains.clear_changed dom) + | Structural r -> + let dom = Domains.structural_propagation r dom in + Domains.iter_changed (touch bcs queue) dom; + let changed = SX.add r changed in + propagate queue changed bcs (Domains.clear_changed dom) + | exception QC.Empty -> + assert (not (Domains.has_changed dom)); + changed, dom in fun eqs bcs dom -> - let changed, bcs, dom = propagate SX.empty bcs dom in - SX.fold (fun r acc -> - add_eqs acc (Shostak.Bitv.embed r) (Domains.get r dom) - ) changed eqs, bcs, dom + (* Optimization to avoid unnecessary allocations *) + if Constraints.has_pending bcs || Domains.has_changed dom then + let queue = QC.create 17 in + Constraints.iter_pending (fun c -> QC.push queue (Constraint c)) bcs; + let bcs = Constraints.clear_pending bcs in + Domains.iter_changed (touch bcs queue) dom; + let dom = Domains.clear_changed dom in + let changed, dom = propagate queue SX.empty bcs dom in + SX.fold (fun r acc -> + add_eqs acc (Shostak.Bitv.embed r) (Domains.get r dom) + ) changed eqs, bcs, dom + else + eqs, bcs, dom type t = { delayed : Rel_utils.Delayed.t diff --git a/src/lib/reasoners/rel_utils.ml b/src/lib/reasoners/rel_utils.ml index c90158be22..ff4b3d37f8 100644 --- a/src/lib/reasoners/rel_utils.ml +++ b/src/lib/reasoners/rel_utils.ml @@ -294,15 +294,21 @@ module type Domains = sig @raise Inconsistent if this causes any domain in [d] to become empty. *) - val choose_changed : t -> X.r * t - (** [choose_changed d] returns a pair [r, d'] such that: + val has_changed : t -> bool + (** Returns [true] if any element is marked as changed. - - The domain associated with [r] has changed since the last time - [choose_changed] was called. - - [r] has (by definition) not changed in [d'] + Elements are marked as changed when their domain shrinks due to a call to + either [subst] or [update], and are unmarked by [clear_changed]. *) - Moreover, prior to returning [r], structural propagation is - automatically performed. + val iter_changed : (X.r -> unit) -> t -> unit + (** Iterate over the changed elements. See [has_changed]. *) + + val clear_changed : t -> t + (** Returns an identical domain, except that no elements are marked as + changed. *) + + val structural_propagation : X.r -> t -> t + (** Perform structural propagation for the given representative. More precisely, if [r] is a leaf, the domain of [r] is propagated to any semantic value that contains [r] as a leaf according to the structure of @@ -489,10 +495,12 @@ struct else Domain.fold_leaves update r (get r t) t - let choose_changed t = - let r = SX.choose t.changed in - let t = { t with changed = SX.remove r t.changed } in - r, structural_propagation r t + let has_changed t = + not @@ SX.is_empty t.changed + + let iter_changed f t = SX.iter f t.changed + + let clear_changed t = { t with changed = SX.empty } end module type Constraint = sig @@ -564,31 +572,28 @@ module Constraints_make(Constraint : Constraint) : sig The explanation [ex] justifies the equality [p = v]. *) - val notify : X.r -> t -> t - (** [notify r t] marks all constraints involving [r] (i.e. all constraints - that have [r] as one of their arguments) as pending. + val iter_parents : (Constraint.t explained -> unit) -> X.r -> t -> unit + (** [iter_parents f r t] calls [f] on all the constraints that apply directly + to [r] (precisely, all the constraints [r] is an argument of). *) - This function should be used when the domain of [r] is updated, if - domains are tracked for all representatives. *) + val iter_pending : (Constraint.t explained -> unit) -> t -> unit + (** [iter_pending f t] calls [f] on all the constraints currently marked as + pending. Constraints are marked as pending when they are added, including + when a new constraint is added due to substitution of an old constraint + (whether the old constraint was pending or not). *) - val notify_leaf : X.r -> t -> t - (** [notify_leaf r t] marks all constraints that have [r] as a leaf (i.e. - all constraints that have at least one argument [a] such that [r] is in - [X.leaves a]) as pending. + val clear_pending : t -> t + (** [clear_pending t] returns a copy of [t] except that no constraints are + marked as pending. *) - This function should be used when the domain of [r] is updated, if - domains are tracked for leaves only. *) + val has_pending : t -> bool + (** [has_pending t] returns [true] if there is any constraint marked as + pending, in which case [iter_pending] and [clear_pending] are guaranteed + to be no-ops. Should only be used for optimization. *) val fold_args : (X.r -> 'a -> 'a) -> t -> 'a -> 'a (** [fold_args f t acc] folds [f] over all the term representatives that are arguments of at least one constraint. *) - - val next_pending : t -> Constraint.t explained * t - (** [next_pending t] returns a pair [c, t'] where [c] was pending in [t] and - [t'] is identical to [t], except that [c] is no longer a pending - constraint. - - @raise Not_found if there are no pending constraints. *) end = struct module CS = Set.Make(struct type t = Constraint.t explained @@ -677,24 +682,21 @@ end = struct ) cs t | exception Not_found -> t - let notify r t = + let iter_parents f r t = match MX.find r t.args_map with - | cs -> - CS.fold (fun c t -> { t with pending = CS.add c t.pending }) cs t - | exception Not_found -> t + | cs -> CS.iter f cs + | exception Not_found -> () - let notify_leaf r t = - match MX.find r t.leaves_map with - | cs -> - CS.fold (fun c t -> { t with pending = CS.add c t.pending }) cs t - | exception Not_found -> t + let iter_pending f t = + CS.iter f t.pending + + let clear_pending t = + { t with pending = CS.empty } + + let has_pending t = not @@ CS.is_empty t.pending let fold_args f c acc = MX.fold (fun r _ acc -> f r acc ) c.args_map acc - - let next_pending t = - let c = CS.choose t.pending in - c, { t with pending = CS.remove c t.pending } end diff --git a/src/lib/util/uqueue.ml b/src/lib/util/uqueue.ml new file mode 100644 index 0000000000..ce7a6cb995 --- /dev/null +++ b/src/lib/util/uqueue.ml @@ -0,0 +1,65 @@ +(**************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2024 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of OCamlPro *) +(* Non-Commercial Purpose License, version 1. *) +(* *) +(* As an exception, Alt-Ergo Club members at the Gold level can *) +(* use this file under the terms of the Apache Software License *) +(* version 2.0. *) +(* *) +(* More details can be found in the directory licenses/ *) +(* *) +(**************************************************************************) + +module type S = sig + type elt + + type t + + val create : int -> t + + val push : t -> elt -> unit + + exception Empty + + val pop : t -> elt + + val peek : t -> elt + + val is_empty : t -> bool + + val clear : t -> unit +end + +module Make(H : Hashtbl.HashedType) : S with type elt = H.t = struct + module HT = Hashtbl.Make(H) + + type elt = H.t + + type t = { queue : H.t Queue.t ; elements : unit HT.t} + + let create n = + { queue = Queue.create () ; elements = HT.create n } + + let push { queue ; elements } x = + if HT.mem elements x then () else ( + HT.replace elements x (); + Queue.push x queue + ) + + exception Empty = Queue.Empty + + let pop { queue ; elements } = + let x = Queue.pop queue in + HT.remove elements x; x + + let peek { queue; _ } = Queue.peek queue + + let is_empty { queue; _ } = Queue.is_empty queue + + let clear { queue ; elements } = + Queue.clear queue; HT.clear elements +end diff --git a/src/lib/util/uqueue.mli b/src/lib/util/uqueue.mli new file mode 100644 index 0000000000..4a5d9da187 --- /dev/null +++ b/src/lib/util/uqueue.mli @@ -0,0 +1,60 @@ +(**************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2024 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of OCamlPro *) +(* Non-Commercial Purpose License, version 1. *) +(* *) +(* As an exception, Alt-Ergo Club members at the Gold level can *) +(* use this file under the terms of the Apache Software License *) +(* version 2.0. *) +(* *) +(* More details can be found in the directory licenses/ *) +(* *) +(**************************************************************************) + +(** First-in first-out *unique* queues. + + This module implements queues (FIFOs) without duplicates, with in-place + modifications. Implemented as a wrapper around the [Queue] and [Hashtbl] (to + ensure uniqueness) modules from the stdlib. *) + +module type S = sig + type elt + (** The type of elements in the unique queue. *) + + type t + (** The type of unique queues with [elt] elements. *) + + val create : int -> t + (** Create a new empty unique queue. The [int] parameter is passed to the + backing [Hashtbl] used to ensure uniqueness. *) + + val push : t -> elt -> unit + (** [push q x] adds [x] at the end of the queue [q]. Does nothing if [x] is + already present in the queue. *) + + exception Empty + (** Raised when [pop] or [peek] are applied to an empty queue. *) + + val pop : t -> elt + (** [pop q] removes and returns the first element in queue [q], or raises + [Empty] if the queue is empty. + + @raise Empty if the queue is empty. *) + + val peek : t -> elt + (** [peek q] returns the first element in queue [q] without removing it, or + raises [Empty] if the queue is empty. + + @raise Empty if the queue is empty. *) + + val is_empty : t -> bool + (** Returns [true] if the queue is empty, [false] otherwise. *) + + val clear : t -> unit + (** Discard all elements from the queue. *) +end + +module Make(H : Hashtbl.HashedType) : S with type elt = H.t