Skip to content

Commit

Permalink
fix(BV, CP): Run cross-propagators to completion (#1221)
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
bclement-ocp authored Aug 28, 2024
1 parent 68850d4 commit 8728bf7
Showing 1 changed file with 24 additions and 7 deletions.
31 changes: 24 additions & 7 deletions src/lib/reasoners/domains.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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

Expand All @@ -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 =
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down

0 comments on commit 8728bf7

Please sign in to comment.