change arry_var_int_element propagator to be incremental

crates/huub/src/actions/inspection.rs

@@ -15,4 +15,5 @@ pub(crate) trait InspectionActions: TrailingActions {
 		}
 	}
 	fn check_int_in_domain(&self, var: IntView, val: IntVal) -> bool;
+	fn check_int_is_fixed(&self, var: IntView) -> bool;
 }

crates/huub/src/propagator/array_var_int_element.rs

@@ -7,7 +7,7 @@ use crate::{
 	},
 	propagator::{conflict::Conflict, int_event::IntEvent, PropagationActions, Propagator},
 	solver::{
-		engine::queue::PriorityLevel,
+		engine::{queue::PriorityLevel, trail::TrailedInt},
 		poster::{BoxedPropagator, Poster, QueuePreferences},
 		value::IntVal,
 		view::IntView,
@@ -19,20 +19,22 @@ use crate::{
 pub(crate) struct ArrayVarIntElementBounds {
 	vars: Vec<IntView>,                // Variables to be selected
 	y: IntView,                        // The selected variable
-	idx: IntView,                      // Variable that stores the index of the selected variable
+	index: IntView,                    // Variable that stores the index of the selected variable
 	action_list: Vec<(u32, IntEvent)>, // List of x variables that have been modified since the last propagation
+	min_support: TrailedInt,           // The minimum support of the selected variable
+	max_support: TrailedInt,           // The maximum support of the selected variable
 }
 
 impl ArrayVarIntElementBounds {
 	pub(crate) fn prepare<V: Into<IntView>, VI: IntoIterator<Item = V>>(
 		vars: VI,
 		y: IntView,
-		idx: IntView,
+		index: IntView,
 	) -> impl Poster {
 		ArrayVarIntElementBoundsPoster {
 			vars: vars.into_iter().map(Into::into).collect(),
 			y,
-			idx,
+			index,
 		}
 	}
 }
@@ -53,139 +55,140 @@ where
 
 	#[tracing::instrument(name = "array_int_element", level = "trace", skip(self, actions))]
 	fn propagate(&mut self, actions: &mut P) -> Result<(), Conflict> {
-		let idx_is_fixed =
-			actions.get_int_lower_bound(self.idx) == actions.get_int_upper_bound(self.idx);
-		if idx_is_fixed {
-			let fixed_idx = actions.get_int_lower_bound(self.idx);
+		// ensure bounds of y and self.vars[self.index] are consistent when self.index is fixed
+		if actions.check_int_is_fixed(self.index) {
+			let fixed_index = actions.get_int_lower_bound(self.index);
 			// propagate only when the fixed index is not out of bound
-			if fixed_idx >= 0 && fixed_idx < self.vars.len() as IntVal {
-				let fixed_var = self.vars[fixed_idx as usize];
+			if fixed_index >= 0 && fixed_index < self.vars.len() as IntVal {
+				let index_val_lit = actions.get_int_val_lit(self.index).unwrap();
+				let fixed_var = self.vars[fixed_index as usize];
 				actions.set_int_lower_bound(
 					self.y,
 					actions.get_int_lower_bound(fixed_var),
-					|a: &mut P| {
-						[
-							a.get_int_lit(self.idx, LitMeaning::Eq(fixed_idx)),
-							a.get_int_lower_bound_lit(fixed_var),
-						]
-					},
+					|a: &mut P| [index_val_lit, a.get_int_lower_bound_lit(fixed_var)],
 				)?;
 				actions.set_int_lower_bound(
 					fixed_var,
 					actions.get_int_lower_bound(self.y),
-					|a: &mut P| {
-						[
-							a.get_int_lit(self.idx, LitMeaning::Eq(fixed_idx)),
-							a.get_int_lower_bound_lit(self.y),
-						]
-					},
+					|a: &mut P| [index_val_lit, a.get_int_lower_bound_lit(self.y)],
 				)?;
 				actions.set_int_upper_bound(
 					self.y,
-					actions.get_int_upper_bound(self.y),
-					|a: &mut P| {
-						[
-							a.get_int_lit(self.idx, LitMeaning::Eq(fixed_idx)),
-							a.get_int_upper_bound_lit(fixed_var),
-						]
-					},
+					actions.get_int_upper_bound(fixed_var),
+					|a: &mut P| [index_val_lit, a.get_int_upper_bound_lit(fixed_var)],
 				)?;
 				actions.set_int_upper_bound(
 					fixed_var,
 					actions.get_int_upper_bound(self.y),
-					|a: &mut P| {
-						[
-							a.get_int_lit(self.idx, LitMeaning::Eq(fixed_idx)),
-							a.get_int_upper_bound_lit(self.y),
-						]
-					},
+					|a: &mut P| [index_val_lit, a.get_int_upper_bound_lit(self.y)],
 				)?;
 				return Ok(());
 			}
 		}
 
-		// remove values from the index variable when:
-		// 1. y.upper_bound < self.vars[i].lower_bound -> idx != i
-		// 2. y.lower_bound > self.vars[i].upper_bound -> idx != i
 		let y_lb = actions.get_int_lower_bound(self.y);
 		let y_ub = actions.get_int_upper_bound(self.y);
+		let min_support = actions.get_trailed_int(self.min_support);
+		let max_support = actions.get_trailed_int(self.max_support);
+		let mut need_min_support = true;
+		let mut need_max_support = true;
+		let mut new_min_support = -1;
+		let mut new_max_support = -1;
+		let mut new_min = IntVal::MAX;
+		let mut new_max = IntVal::MIN;
+		if min_support != -1 {
+			let min_lb = actions.get_int_lower_bound(self.vars[min_support as usize]);
+			need_min_support = min_lb > y_lb;
+			new_min_support = min_support;
+			new_min = min_lb;
+		}
+		if max_support != -1 {
+			let max_ub = actions.get_int_upper_bound(self.vars[max_support as usize]);
+			need_max_support = max_ub < y_ub;
+			new_max_support = max_support;
+			new_max = max_ub;
+		}
+
+		// Iterate through all variables:
+		// 1. remove values from the index variable when:
+		// 	(1) y.upper_bound < self.vars[i].lower_bound -> index != i
+		//  (2) y.lower_bound > self.vars[i].upper_bound -> index != i
+		// 2. update min_support and max_support if necessary
 		for (i, v) in self.vars.iter().enumerate() {
-			if actions.check_int_in_domain(self.idx, i as IntVal) {
-				let v_lb = actions.get_int_lower_bound(*v);
-				let v_ub = actions.get_int_upper_bound(*v);
+			let (v_lb, v_ub) = actions.get_int_bounds(*v);
+			if actions.check_int_in_domain(self.index, i as IntVal) {
 				if y_ub < v_lb {
-					actions.set_int_not_eq(self.idx, i as IntVal, |a: &mut P| {
+					actions.set_int_not_eq(self.index, i as IntVal, |a: &mut P| {
 						[
 							a.get_int_lit(self.y, LitMeaning::Less(v_lb)),
 							a.get_int_lower_bound_lit(*v),
 						]
 					})?;
 				}
 				if v_ub < y_lb {
-					actions.set_int_not_eq(self.idx, i as IntVal, |a: &mut P| {
+					actions.set_int_not_eq(self.index, i as IntVal, |a: &mut P| {
 						[
 							a.get_int_lit(self.y, LitMeaning::GreaterEq(v_ub + 1)),
 							a.get_int_upper_bound_lit(*v),
 						]
 					})?;
 				}
 			}
-		}
 
-		// propagate the lower bound of the selected variable y
-		// y.lower_bound >= min(i in domain(x))(self.vars[i].lower_bound)
-		let mut min_lb = IntVal::MAX;
-		for (i, v) in self.vars.iter().enumerate() {
-			if actions.check_int_in_domain(self.idx, i as IntVal) {
-				let v_lb = actions.get_int_lower_bound(*v);
-				if v_lb < min_lb {
-					min_lb = v_lb;
-					if min_lb <= y_lb {
-						break;
-					}
-				}
+			// update min_support if i is in the domain of self.index and the lower bound of v is less than the current min
+			if need_min_support
+				&& actions.check_int_in_domain(self.index, i as IntVal)
+				&& v_lb < new_min
+			{
+				new_min_support = i as IntVal;
+				new_min = v_lb;
+				need_min_support = new_min > y_lb; // stop finding min_support if new_min ≤ y_lb
+			}
+
+			// update max_support if i is in the domain of self.index and the upper bound of v is greater than the current max
+			if need_max_support
+				&& actions.check_int_in_domain(self.index, i as IntVal)
+				&& v_ub > new_max
+			{
+				new_max_support = i as IntVal;
+				new_max = v_ub;
+				need_max_support = new_max < y_ub; // stop finding max_support if new_max ≥ y_ub
 			}
 		}
-		if min_lb > y_lb {
-			actions.set_int_lower_bound(self.y, min_lb, |a: &mut P| {
+
+		let _ = actions.set_trailed_int(self.min_support, new_min_support);
+		let _ = actions.set_trailed_int(self.max_support, new_max_support);
+
+		// propagate the lower bound of the selected variable y if min_support is not valid anymore
+		// y.lower_bound >= min(i in domain(x))(self.vars[i].lower_bound)
+		if new_min > y_lb {
+			actions.set_int_lower_bound(self.y, new_min, |a: &mut P| {
 				self.vars
 					.iter()
 					.enumerate()
 					.map(|(i, &v)| {
-						if a.check_int_in_domain(self.idx, i as IntVal) {
-							a.get_int_lit(v, LitMeaning::GreaterEq(min_lb))
+						if a.check_int_in_domain(self.index, i as IntVal) {
+							a.get_int_lit_relaxed(v, LitMeaning::GreaterEq(new_min)).0
 						} else {
-							a.get_int_lit(self.idx, LitMeaning::NotEq(i as IntVal))
+							a.get_int_lit(self.index, LitMeaning::NotEq(i as IntVal))
 						}
 					})
 					.collect_vec()
 			})?;
 		}
 
-		// propagate the upper bound of the selected variable y
+		// propagate the upper bound of the selected variable y if max_support is not valid anymore
 		// y.upper_bound <= max(i in domain(x))(self.vars[i].upper_bound)
-		let mut max_ub = IntVal::MIN;
-		for (i, v) in self.vars.iter().enumerate() {
-			if actions.check_int_in_domain(self.idx, i as IntVal) {
-				let v_ub = actions.get_int_upper_bound(*v);
-				if v_ub > max_ub {
-					max_ub = v_ub;
-					if max_ub >= y_ub {
-						break;
-					}
-				}
-			}
-		}
-		if max_ub < y_ub {
-			actions.set_int_upper_bound(self.y, max_ub, |a: &mut P| {
+		if new_max < y_ub {
+			actions.set_int_upper_bound(self.y, new_max, |a: &mut P| {
 				self.vars
 					.iter()
 					.enumerate()
 					.map(|(i, &v)| {
-						if a.check_int_in_domain(self.idx, i as IntVal) {
-							a.get_int_lit(v, LitMeaning::Less(max_ub + 1))
+						if a.check_int_in_domain(self.index, i as IntVal) {
+							a.get_int_lit_relaxed(v, LitMeaning::Less(new_max + 1)).0
 						} else {
-							a.get_int_lit(self.idx, LitMeaning::NotEq(i as IntVal))
+							a.get_int_lit(self.index, LitMeaning::NotEq(i as IntVal))
 						}
 					})
 					.collect_vec()
@@ -197,7 +200,7 @@ where
 }
 
 struct ArrayVarIntElementBoundsPoster {
-	idx: IntView,
+	index: IntView,
 	y: IntView,
 	vars: Vec<IntView>,
 }
@@ -209,14 +212,16 @@ impl Poster for ArrayVarIntElementBoundsPoster {
 		let prop = ArrayVarIntElementBounds {
 			vars: self.vars.into_iter().map(Into::into).collect(),
 			y: self.y,
-			idx: self.idx,
+			index: self.index,
 			action_list: Vec::new(),
+			min_support: actions.new_trailed_int(-1),
+			max_support: actions.new_trailed_int(-1),
 		};
 		for (i, v) in prop.vars.iter().enumerate() {
 			actions.subscribe_int(*v, IntEvent::Bounds, i as u32);
 		}
 		actions.subscribe_int(prop.y, IntEvent::Bounds, prop.vars.len() as u32);
-		actions.subscribe_int(prop.idx, IntEvent::Domain, prop.vars.len() as u32 + 1);
+		actions.subscribe_int(prop.index, IntEvent::Domain, prop.vars.len() as u32 + 1);
 		Ok((
 			Box::new(prop),
 			QueuePreferences {
@@ -268,17 +273,17 @@ mod tests {
 			EncodingType::Eager,
 			EncodingType::Lazy,
 		);
-		let idx = IntVar::new_in(
+		let index = IntVar::new_in(
 			&mut slv,
 			RangeList::from_iter([0..=2]),
 			EncodingType::Eager,
 			EncodingType::Lazy,
 		);
 
-		slv.add_propagator(ArrayVarIntElementBounds::prepare(vec![a, b, c], y, idx))
+		slv.add_propagator(ArrayVarIntElementBounds::prepare(vec![a, b, c], y, index))
 			.unwrap();
 		slv.expect_solutions(
-			&[idx, y, a, b, c],
+			&[index, y, a, b, c],
 			expect![[r#"
 		0, 3, 3, 2, 4
 		0, 3, 3, 2, 5
@@ -307,9 +312,9 @@ mod tests {
 		let b = prb.new_int_var((4..=5).into());
 		let c = prb.new_int_var((4..=10).into());
 		let y = prb.new_int_var((1..=2).into());
-		let idx = prb.new_int_var((0..=2).into());
+		let index = prb.new_int_var((0..=2).into());
 
-		prb += Constraint::ArrayVarIntElement(vec![a, b, c], idx, y);
+		prb += Constraint::ArrayVarIntElement(vec![a, b, c], index, y);
 		prb.assert_unsatisfiable();
 	}
 
@@ -335,17 +340,17 @@ mod tests {
 			EncodingType::Eager,
 			EncodingType::Lazy,
 		);
-		let idx = IntVar::new_in(
+		let index = IntVar::new_in(
 			&mut slv,
 			RangeList::from_iter([0..=0, 3..=3]),
 			EncodingType::Eager,
 			EncodingType::Lazy,
 		);
 
-		slv.add_propagator(ArrayVarIntElementBounds::prepare(vec![a, b], y, idx))
+		slv.add_propagator(ArrayVarIntElementBounds::prepare(vec![a, b], y, index))
 			.unwrap();
 		slv.expect_solutions(
-			&[idx, y, a, b],
+			&[index, y, a, b],
 			expect![[r#"
     0, 3, 3, 1
     0, 3, 3, 2

crates/huub/src/solver.rs

@@ -564,6 +564,7 @@ where
 			fn get_int_bounds(&self, var: IntView) -> (IntVal, IntVal);
 			fn get_int_val(&self, var: IntView) -> Option<IntVal>;
 			fn check_int_in_domain(&self, var: IntView, val: IntVal) -> bool;
+			fn check_int_is_fixed(&self, var: IntView) -> bool;
 		}
 	}
 }

crates/huub/src/solver/engine.rs

@@ -843,6 +843,10 @@ impl InspectionActions for State {
 			false
 		}
 	}
+	fn check_int_is_fixed(&self, var: IntView) -> bool {
+		let (lb, ub) = self.get_int_bounds(var);
+		lb == ub
+	}
 }
 
 impl TrailingActions for State {

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

@@ -200,6 +200,7 @@ impl InspectionActions for SolvingContext<'_> {
 			fn get_int_bounds(&self, var: IntView) -> (IntVal, IntVal);
 			fn get_int_val(&self, var: IntView) -> Option<IntVal>;
 			fn check_int_in_domain(&self, var: IntView, val: IntVal) -> bool;
+			fn check_int_is_fixed(&self, var: IntView) -> bool;
 		}
 	}
 }

crates/huub/src/solver/initialization_context.rs

@@ -131,6 +131,7 @@ where
 			fn get_int_bounds(&self, var: IntView) -> (IntVal, IntVal);
 			fn get_int_val(&self, var: IntView) -> Option<IntVal>;
 			fn check_int_in_domain(&self, var: IntView, val: IntVal) -> bool;
+			fn check_int_is_fixed(&self, var: IntView) -> bool;
 		}
 	}
 }