From c61e536ce50d39825c56510d4c04997894d8b768 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <basile.clement@ocamlpro.com>
Date: Wed, 28 Aug 2024 11:06:21 +0200
Subject: [PATCH] fix(BV, CP): Run cross-propagators to completion

Since #1185, when substitutions change the domain of a variable, we no
longer trigger propagations, which means that we can end up in a state
where the bitlist and interval domains are not consistent (i.e. running
[constrain_bitlist_from_interval] or [constrain_interval_from_bitlist]
would shrink some domains).

This was initially part of #1185 but was accidentally removed as part of
a simplification pass during review. Add it back.
---
 src/lib/reasoners/domains.ml | 31 ++++++++++++++++++++++++-------
 1 file changed, 24 insertions(+), 7 deletions(-)

diff --git a/src/lib/reasoners/domains.ml b/src/lib/reasoners/domains.ml
index 379c38144..f8b49076c 100644
--- a/src/lib/reasoners/domains.ml
+++ b/src/lib/reasoners/domains.ml
@@ -100,6 +100,11 @@ sig
 
   val watches : key -> t -> W.Set.t
   (** Returns the set of watches associated with object [x]. *)
+
+  val needs_propagation : t -> bool
+  (** Returns [true] if the domain needs propagation. This means that the domain
+      associated with some variables has been shrunk, and cross-domain
+      propagation might be needed. *)
 end
 =
 struct
@@ -116,6 +121,9 @@ struct
     ; watching : SX.t W.Map.t
     (** Map from watches to the variables they watch. Used to be able
         to remove watches. *)
+    ; changed : SX.t
+    (** Set of variables whose domain has changed. Used for cross-domain
+        propagations.*)
     }
 
   type key = X.t
@@ -130,7 +138,8 @@ struct
   let empty =
     { domains = MX.empty
     ; watches = MX.empty
-    ; watching = W.Map.empty }
+    ; watching = W.Map.empty
+    ; changed = SX.empty }
 
   let find x t = MX.find x t.domains
 
@@ -154,7 +163,8 @@ struct
         MX.remove x t.watches, watching
       | exception Not_found -> t.watches, t.watching
     in
-    { domains ; watches ; watching }
+    let changed = SX.remove x t.changed in
+    { domains ; watches ; watching ; changed }
 
   let add_watches x ws t =
     let watches =
@@ -168,7 +178,7 @@ struct
               | Some xs -> Some (SX.add x xs)) watching
         ) ws t.watching
     in
-    { domains = t.domains ; watches ; watching }
+    { domains = t.domains ; watches ; watching ; changed = t.changed }
 
   let remove_watch w t =
     match W.Map.find w t.watching with
@@ -186,14 +196,17 @@ struct
           ) xs t.watches
       in
       let watching = W.Map.remove w t.watching in
-      { domains = t.domains ; watches ; watching }
+      { domains = t.domains ; watches ; watching ; changed = t.changed }
     | exception Not_found -> t
 
   let watches x t =
     try MX.find x t.watches with Not_found -> W.Set.empty
 
   let add x d t =
-    { t with domains = MX.add x d t.domains }
+    { t with domains = MX.add x d t.domains ; changed = SX.add x t.changed }
+
+  let needs_propagation t =
+    not (SX.is_empty t.changed)
 
   module Ephemeral = struct
     type key = X.t
@@ -244,7 +257,8 @@ struct
         entry
   end
 
-  let edit ~notify ~default { domains ; watches ; watching } =
+  let edit ~notify ~default { domains ; watches ; watching ; changed } =
+    SX.iter notify changed;
     { Ephemeral.domains
     ; watches
     ; watching
@@ -263,7 +277,8 @@ struct
     in
     { domains
     ; watches = t.Ephemeral.watches
-    ; watching = t.Ephemeral.watching }
+    ; watching = t.Ephemeral.watching
+    ; changed = SX.empty }
 end
 
 module Make
@@ -337,6 +352,8 @@ struct
     ; triggers = t.triggers }
 
   let needs_propagation t =
+    DMA.needs_propagation t.atoms ||
+    DMC.needs_propagation t.composites ||
     not (W.Set.is_empty t.triggers)
 
   let[@inline] variables { variables ; _ } = variables