feat(BV,CP): Use a FIFO queue for constraint propagation (#1054)

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

@@ -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
   )

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,26 @@ 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
+  (** Structural constraint associated with [X.r]. See
+      {!Rel_utils.Domains.structural_propagation}. *)
+
+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 +423,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

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
@@ -536,14 +544,14 @@ module Constraints_make(Constraint : Constraint) : sig
       constraints that applies to semantic values, and remembers the relation
       between constraints and semantic values.
 
-      The constraints associated with specific semantic values can be notified
-      (see [notify]), which is used to only propagate constraints involving
-      semantic values whose domain has changed.
+      The constraints applying to a given semantic value can be recovered using
+      the [iter_pending] functions.
 
-      The constraints that have been notified are called "pending
-      constraints", and the set thereof is the "pending set". These are
-      constraints that need to be propagated, and can be recovered using
-      [next_pending]. *)
+      New constraints are marked as "pending" when added to the constraint set
+      (whether by a call to [add] or following a substitution). These
+      constraints should ultimately be propagated; they can be accessed through
+      the [iter_pending]. Once pending constraints have been propagated, the
+      "pending" constraints should be cleared with [clear_pending]. *)
 
   val pp : t Fmt.t
   (** Pretty-printer for constraint sets. *)
@@ -564,31 +572,29 @@ 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. Hence if [has_pending t] returns [false], [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 +683,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

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

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