Merge branch 'feat/fixed_daemon' into feat/deactivate_propagations

crates/huub/src/actions/initialization.rs

@@ -9,11 +9,24 @@ pub(crate) trait InitializationActions: DecisionActions {
 		&mut self,
 		clause: I,
 	) -> Result<(), ReformulationError>;
+
 	/// Create a new trailed integer value with the given initial value.
 	fn new_trailed_int(&mut self, init: IntVal) -> TrailedInt;
+
 	/// Enqueue a propagator to be enqueued when a boolean variable is assigned.
 	fn enqueue_on_bool_change(&mut self, var: BoolView);
+
 	/// Enqueue a propagator to be enqueued when an integer variable is changed
 	/// according to the given propagation condition.
 	fn enqueue_on_int_change(&mut self, var: IntView, condition: IntPropCond);
+
+	/// Enqueue the propagator when at least "n" of the given variables are fixed,
+	/// and whenever a subsequent variable is fixed.
+	///
+	/// # Warning
+	/// This function will panic
+	/// - if it is called when initiliazing a brancher,
+	/// - if it is called multiple times for the same propagator,
+	/// - or if the number of variables is lower than `n`.
+	fn enqueue_when_n_fixed(&mut self, n: usize, bool_vars: &[BoolView], int_vars: &[IntView]);
 }

crates/huub/src/solver/engine.rs

@@ -30,7 +30,7 @@ use crate::{
 	propagator::reason::Reason,
 	solver::{
 		engine::{
-			activation_list::{ActivationList, IntEvent},
+			activation_list::{BoolActivationList, IntActivationList, IntEvent},
 			bool_to_int::BoolToIntMap,
 			int_var::{IntVar, IntVarRef, LitMeaning, OrderStorage},
 			queue::{PriorityLevel, PriorityQueue},
@@ -134,9 +134,14 @@ pub(crate) struct State {
 
 	// ---- Queueing Infrastructure ----
 	/// Boolean variable enqueueing information
-	pub(crate) bool_activation: HashMap<RawVar, Vec<PropRef>>,
+	pub(crate) bool_activation: HashMap<RawVar, BoolActivationList>,
 	/// Integer variable enqueueing information
-	pub(crate) int_activation: IndexVec<IntVarRef, ActivationList>,
+	pub(crate) int_activation: IndexVec<IntVarRef, IntActivationList>,
+	/// Fixed Deamons
+	///
+	/// These are propagators that are enqueued when set number of values have been
+	/// assigned.
+	pub(crate) fixed_daemons: HashMap<PropRef, TrailedInt>,
 	/// Queue of propagators awaiting action
 	pub(crate) propagator_queue: PriorityQueue<PropRef>,
 	/// Priority within the queue for each propagator
@@ -172,6 +177,7 @@ impl Default for State {
 			vsids: false,
 			bool_activation: Default::default(),
 			int_activation: Default::default(),
+			fixed_daemons: Default::default(),
 			propagator_queue: Default::default(),
 			propagator_priority: Default::default(),
 			enqueued: Default::default(),
@@ -647,22 +653,50 @@ impl State {
 				self.enqueued[prop] = true;
 			}
 		}
+		if event == IntEvent::Fixed {
+			for prop in self.int_activation[int_var].fixed_daemons() {
+				let counter = self.fixed_daemons[&prop];
+				let count = self.trail.get_trailed_int(counter) - 1;
+				let _ = self.trail.set_trailed_int(counter, count);
+				if count <= 0 && !self.enqueued[prop] {
+					self.propagator_queue
+						.insert(self.propagator_priority[prop], prop);
+					self.enqueued[prop] = true;
+				}
+			}
+		}
 	}
 
 	fn enqueue_propagators(&mut self, lit: RawLit, skip: Option<PropRef>) {
-		for &prop in self.bool_activation.get(&lit.var()).into_iter().flatten() {
-			if Some(prop) != skip && !self.enqueued[prop] {
-				if !self.vsids
-					|| self.activity_scores[prop] >= self.config.propagator_activity_threshold
-					|| (self.config.enqueue_functional && self.functional[prop])
-				{
+		if let Some(activator) = self.bool_activation.get(&lit.var()) {
+			// Enqueue all propagators that are directly activated by the given literal
+			for prop in activator.activations() {
+				if Some(prop) != skip && !self.enqueued[prop] {
+					if !self.vsids
+						|| self.activity_scores[prop] >= self.config.propagator_activity_threshold
+						|| (self.config.enqueue_functional && self.functional[prop])
+					{
+						self.propagator_queue
+							.insert(self.propagator_priority[prop], prop);
+					} else {
+						trace!(propagator = usize::from(prop), "deactivate propagator");
+						self.propagator_queue.insert(PriorityLevel::Inactive, prop);
+					}
+					self.enqueued[prop] = true;
+				}
+			}
+
+			// Decrease all fixed daemons that are associated with the given literal and
+			// activate them if they are now zero
+			for prop in activator.fixed_daemons() {
+				let counter = self.fixed_daemons[&prop];
+				let count = self.trail.get_trailed_int(counter) - 1;
+				let _ = self.trail.set_trailed_int(counter, count);
+				if count <= 0 && !self.enqueued[prop] {
 					self.propagator_queue
 						.insert(self.propagator_priority[prop], prop);
-				} else {
-					trace!(propagator = usize::from(prop), "deactivate propagator");
-					self.propagator_queue.insert(PriorityLevel::Inactive, prop);
+					self.enqueued[prop] = true;
 				}
-				self.enqueued[prop] = true;
 			}
 		}
 

crates/huub/src/solver/engine/activation_list.rs

@@ -2,6 +2,14 @@ use std::{mem, ops::Add};
 
 use crate::solver::engine::PropRef;
 
+#[derive(Clone, Debug, Default, Eq, PartialEq)]
+/// A data structure that store a list of propagators to be enqueued based on
+/// different propagation conditions.
+pub(crate) struct BoolActivationList {
+	activations: Vec<PropRef>,
+	fixed_daemons: Vec<PropRef>,
+}
+
 #[derive(Clone, Debug, Default, Eq, PartialEq)]
 /// A data structure that store a list of propagators to be enqueued based on
 /// different propagation conditions.
@@ -15,12 +23,13 @@ use crate::solver::engine::PropRef;
 /// index of the LowerBound condition, enqueue all propagators untill the
 /// beginning of the UpperBound condition, and then continue from the beginning
 /// of the Bound condition to the end of the list.
-pub(crate) struct ActivationList {
+pub(crate) struct IntActivationList {
 	activations: Vec<PropRef>,
 	lower_bound_idx: u32,
 	upper_bound_idx: u32,
 	bounds_idx: u32,
 	domain_idx: u32,
+	fixed_daemons: Vec<PropRef>,
 }
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
@@ -61,7 +70,29 @@ pub(crate) enum IntPropCond {
 	Domain,
 }
 
-impl ActivationList {
+impl BoolActivationList {
+	/// Add a propagator to the list of propagators to be enqueued when the boolean
+	/// variable is assigned.
+	pub(crate) fn add(&mut self, prop: PropRef) {
+		self.activations.push(prop);
+	}
+
+	/// Add propagator whose fixed daemon should be decreased when the boolean is
+	/// assigned.
+	pub(crate) fn add_fixed_daemon(&mut self, prop: PropRef) {
+		self.fixed_daemons.push(prop);
+	}
+
+	pub(crate) fn activations(&self) -> impl Iterator<Item = PropRef> + '_ {
+		self.activations.iter().copied()
+	}
+
+	pub(crate) fn fixed_daemons(&self) -> impl Iterator<Item = PropRef> + '_ {
+		self.fixed_daemons.iter().copied()
+	}
+}
+
+impl IntActivationList {
 	/// Add a propagator to the list of propagators to be enqueued based on the
 	/// given condition.
 	pub(crate) fn add(&mut self, mut prop: PropRef, condition: IntPropCond) {
@@ -121,6 +152,10 @@ impl ActivationList {
 		};
 	}
 
+	pub(crate) fn add_fixed_daemon(&mut self, prop: PropRef) {
+		self.fixed_daemons.push(prop);
+	}
+
 	/// Get an iterator over the list of propagators to be enqueued.
 	pub(crate) fn activated_by(&self, event: IntEvent) -> impl Iterator<Item = PropRef> + '_ {
 		let r1 = if event == IntEvent::LowerBound {
@@ -141,6 +176,12 @@ impl ActivationList {
 			.copied()
 			.chain(self.activations[r2].iter().copied())
 	}
+
+	/// Add a propagator whose fixed daemon should be decreased when the variable
+	/// is fixed to a single value.
+	pub(crate) fn fixed_daemons(&self) -> impl Iterator<Item = PropRef> + '_ {
+		self.fixed_daemons.iter().copied()
+	}
 }
 
 impl Add<IntEvent> for IntEvent {
@@ -166,7 +207,7 @@ mod tests {
 	use itertools::Itertools;
 
 	use crate::solver::engine::{
-		activation_list::{ActivationList, IntEvent, IntPropCond},
+		activation_list::{IntActivationList, IntEvent, IntPropCond},
 		PropRef,
 	};
 
@@ -181,7 +222,7 @@ mod tests {
 		];
 
 		for list in props.iter().permutations(5) {
-			let mut activation_list = ActivationList::default();
+			let mut activation_list = IntActivationList::default();
 			for (prop, cond) in list.iter() {
 				activation_list.add(*prop, *cond);
 			}

crates/huub/src/solver/initialization_context.rs

@@ -54,7 +54,7 @@ impl<'a, Oracle: PropagatingSolver<Engine>> InitializationActions
 						.bool_activation
 						.entry(lit.var())
 						.or_default()
-						.push(prop);
+						.add(prop);
 				}
 			}
 			BoolViewInner::Const(_) => {}
@@ -88,6 +88,69 @@ impl<'a, Oracle: PropagatingSolver<Engine>> InitializationActions
 			(InitRef::Brancher, _) => {} // ignore: branchers don't receive notifications, and contained literals are already observed.
 		}
 	}
+
+	fn enqueue_when_n_fixed(&mut self, mut n: usize, bool_vars: &[BoolView], int_vars: &[IntView]) {
+		let InitRef::Propagator(prop) = self.init_ref else {
+			panic!("enqueue_when_n_fixed can only be called for propagators")
+		};
+		assert!(
+			n <= bool_vars.len() + int_vars.len(),
+			"waiting on more fixed events than there are variables"
+		);
+		assert!(
+			!self
+				.slv
+				.engine_mut()
+				.state
+				.fixed_daemons
+				.contains_key(&prop),
+			"propagator is already waiting on fixed events"
+		);
+
+		// Filter constants and extract variable references
+		let mut lits = Vec::new();
+		let mut ints = Vec::new();
+		for bv in bool_vars {
+			match bv.0 {
+				BoolViewInner::Lit(lit) => lits.push(lit),
+				BoolViewInner::Const(_) => n -= 1,
+			}
+		}
+		for iv in int_vars {
+			match iv.0 {
+				IntViewInner::Bool { lit, .. } => lits.push(lit),
+				IntViewInner::Const(_) => n -= 1,
+				IntViewInner::Linear { var, .. } | IntViewInner::VarRef(var) => ints.push(var),
+			}
+		}
+
+		if n <= 0 {
+			todo!("immediately enqueue the propagator")
+		}
+
+		for lit in lits {
+			self.slv.engine_mut().state.trail.grow_to_boolvar(lit.var());
+			self.slv.oracle.add_observed_var(lit.var());
+			self.slv
+				.engine_mut()
+				.state
+				.bool_activation
+				.entry(lit.var())
+				.or_default()
+				.add_fixed_daemon(prop);
+		}
+		for var in ints {
+			self.slv.engine_mut().state.int_activation[var].add_fixed_daemon(prop)
+		}
+
+		let count = self.slv.engine_mut().state.trail.track_int(n as i64);
+		let _ = self
+			.slv
+			.engine_mut()
+			.state
+			.fixed_daemons
+			.insert(prop, count);
+	}
 }
 
 impl<'a, Oracle: PropagatingSolver<Engine>> TrailingActions for InitializationContext<'a, Oracle> {