Add int_abs bounds consistent propagator

crates/huub/src/model/constraint.rs

@@ -16,6 +16,7 @@ use crate::{
 		array_int_minimum::ArrayIntMinimumBounds,
 		array_var_int_element::ArrayVarIntElementBounds,
 		disjunctive_stict::DisjunctiveStrictEdgeFinding,
+		int_abs::IntAbsBounds,
 		int_div::IntDivBounds,
 		int_lin_le::{IntLinearLessEqBounds, IntLinearLessEqImpBounds},
 		int_lin_ne::{IntLinearNotEqImpValue, IntLinearNotEqValue},
@@ -38,6 +39,7 @@ pub enum Constraint {
 	ArrayVarBoolElement(Vec<BoolExpr>, IntView, BoolExpr),
 	ArrayVarIntElement(Vec<IntView>, IntView, IntView),
 	DisjunctiveStrict(Vec<IntView>, Vec<IntVal>),
+	IntAbs(IntView, IntView),
 	IntDiv(IntView, IntView, IntView),
 	IntLinEq(Vec<IntView>, IntVal),
 	IntLinEqImp(Vec<IntView>, IntVal, BoolExpr),
@@ -182,6 +184,12 @@ impl Constraint {
 				))?;
 				Ok(())
 			}
+			Constraint::IntAbs(origin, abs) => {
+				let origin = origin.to_arg(slv, map);
+				let abs = abs.to_arg(slv, map);
+				slv.add_propagator(IntAbsBounds::prepare(origin, abs))?;
+				Ok(())
+			}
 			Constraint::IntDiv(numerator, denominator, result) => {
 				let numerator = numerator.to_arg(slv, map);
 				let denominator = denominator.to_arg(slv, map);
@@ -485,6 +493,31 @@ impl Model {
 				}
 				Some(Constraint::DisjunctiveStrict(starts, durations))
 			}
+			Constraint::IntAbs(origin, abs) => {
+				let lb = self.get_int_lower_bound(&origin);
+				let ub = self.get_int_upper_bound(&origin);
+				if ub < 0 {
+					self.set_int_lower_bound(&abs, -ub, con)?;
+					self.set_int_upper_bound(&abs, -lb, con)?;
+				} else if lb >= 0 {
+					self.set_int_lower_bound(&abs, lb, con)?;
+					self.set_int_upper_bound(&abs, ub, con)?;
+				} else {
+					self.set_int_lower_bound(&abs, 0, con)?;
+					let abs_max = ub.max(-lb);
+					self.set_int_upper_bound(&abs, abs_max, con)?;
+				}
+				let abs_ub = ub.abs();
+				debug_assert!(abs_ub >= 0);
+				self.set_int_lower_bound(&origin, -abs_ub, con)?;
+				self.set_int_upper_bound(&abs, abs_ub, con)?;
+				if lb >= 0 {
+					// TODO: Unify
+					Some(Constraint::IntLinEq(vec![origin, -abs], 0))
+				} else {
+					Some(Constraint::IntAbs(origin, abs))
+				}
+			}
 			Constraint::IntDiv(num, denom, res) => {
 				self.diff_int_domain(&denom, &RangeList::from(0..=0), con)?;
 				Some(Constraint::IntDiv(num, denom, res))

crates/huub/src/propagator.rs

@@ -3,6 +3,7 @@ pub(crate) mod array_int_minimum;
 pub(crate) mod array_var_int_element;
 pub(crate) mod conflict;
 pub(crate) mod disjunctive_stict;
+pub(crate) mod int_abs;
 pub(crate) mod int_div;
 pub(crate) mod int_event;
 pub(crate) mod int_lin_le;

crates/huub/src/propagator/int_abs.rs

@@ -0,0 +1,179 @@
+use std::iter::once;
+
+use crate::{
+	actions::{
+		explanation::ExplanationActions, initialization::InitializationActions,
+		trailing::TrailingActions,
+	},
+	propagator::{conflict::Conflict, int_event::IntEvent, PropagationActions, Propagator},
+	solver::{
+		engine::queue::PriorityLevel,
+		poster::{BoxedPropagator, Poster, QueuePreferences},
+	},
+	IntView, LitMeaning, ReformulationError,
+};
+
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+/// Bounds propagator for one integer variable being the absolute value of another
+pub(crate) struct IntAbsBounds {
+	/// The integer variable whose absolute value is being taken
+	origin: IntView,
+	/// Whether the bounds of the origin variable have changed since the last propagation
+	orig_changed: bool,
+	/// The integer variable representing the absolute value
+	abs: IntView,
+	/// Whether the upper bound of the absolute value has changed since the last propagation
+	abs_changed: bool,
+}
+
+struct IntAbsBoundsPoster {
+	origin: IntView,
+	abs: IntView,
+}
+
+impl IntAbsBounds {
+	pub(crate) fn prepare(origin: IntView, abs: IntView) -> impl Poster {
+		IntAbsBoundsPoster { origin, abs }
+	}
+}
+
+impl<P, E, T> Propagator<P, E, T> for IntAbsBounds
+where
+	P: PropagationActions,
+	E: ExplanationActions,
+	T: TrailingActions,
+{
+	fn notify_event(&mut self, data: u32, _: &IntEvent, _: &mut T) -> bool {
+		match data {
+			1 => self.orig_changed = true,
+			2 => self.abs_changed = true,
+			_ => unreachable!("unexpected event data"),
+		};
+		true
+	}
+
+	fn notify_backtrack(&mut self, _new_level: usize) {
+		self.orig_changed = false;
+		self.abs_changed = false;
+	}
+
+	#[tracing::instrument(name = "int_abs", level = "trace", skip(self, actions))]
+	fn propagate(&mut self, actions: &mut P) -> Result<(), Conflict> {
+		let (lb, ub) = actions.get_int_bounds(self.origin);
+
+		if self.orig_changed {
+			self.orig_changed = false;
+			// If we know that the origin is negative, then just negate the bounds
+			if ub < 0 {
+				actions.set_int_upper_bound(self.abs, -lb, |a: &mut P| {
+					vec![
+						a.get_int_lower_bound_lit(self.origin),
+						a.get_int_lit(self.origin, LitMeaning::Less(0)),
+					]
+				})?;
+				actions.set_int_lower_bound(self.abs, -ub, |a: &mut P| {
+					once(a.get_int_upper_bound_lit(self.origin))
+				})?;
+			} else if lb >= 0 {
+				// If we know that the origin is positive, then the bounds are the same
+				actions.set_int_lower_bound(self.abs, lb, |a: &mut P| {
+					once(a.get_int_lower_bound_lit(self.origin))
+				})?;
+				actions.set_int_upper_bound(self.abs, ub, |a: &mut P| {
+					vec![
+						a.get_int_upper_bound_lit(self.origin),
+						a.get_int_lit(self.origin, LitMeaning::GreaterEq(0)),
+					]
+				})?;
+			} else {
+				// If the origin can be either positive or negative, then the bounds are the maximum of the absolute values
+				let abs_max = ub.max(-lb);
+				actions.set_int_upper_bound(self.abs, abs_max, |a: &mut P| {
+					vec![
+						a.get_int_lit(self.origin, LitMeaning::GreaterEq(-abs_max)),
+						a.get_int_lit(self.origin, LitMeaning::Less(abs_max + 1)),
+					]
+				})?;
+			}
+		}
+
+		if self.abs_changed {
+			self.abs_changed = false;
+			let ub = actions.get_int_upper_bound(self.abs);
+			let ub_lit = actions.get_int_upper_bound_lit(self.abs);
+			actions.set_int_lower_bound(self.origin, -ub, ub_lit)?;
+			actions.set_int_upper_bound(self.origin, ub, ub_lit)?;
+		}
+
+		Ok(())
+	}
+}
+
+impl Poster for IntAbsBoundsPoster {
+	fn post<I: InitializationActions + ?Sized>(
+		self,
+		actions: &mut I,
+	) -> Result<(BoxedPropagator, QueuePreferences), ReformulationError> {
+		// Subscribe to both bounds of the origin variable
+		actions.subscribe_int(self.origin, IntEvent::Bounds, 1);
+		// Subscribe only to the upper bound of the absolute value variable
+		actions.subscribe_int(self.abs, IntEvent::UpperBound, 2);
+
+		Ok((
+			Box::new(IntAbsBounds {
+				origin: self.origin,
+				orig_changed: false,
+				abs: self.abs,
+				abs_changed: false,
+			}),
+			QueuePreferences {
+				enqueue_on_post: false,
+				priority: PriorityLevel::Highest,
+			},
+		))
+	}
+}
+
+#[cfg(test)]
+mod tests {
+	use expect_test::expect;
+	use pindakaas::{solver::cadical::Cadical, Cnf};
+	use rangelist::RangeList;
+	use tracing_test::traced_test;
+
+	use crate::{
+		propagator::int_abs::IntAbsBounds,
+		solver::engine::int_var::{EncodingType, IntVar},
+		Solver,
+	};
+
+	#[test]
+	#[traced_test]
+	fn test_int_abs_sat() {
+		let mut slv: Solver<Cadical> = Cnf::default().into();
+		let a = IntVar::new_in(
+			&mut slv,
+			(-3..=3).into(),
+			EncodingType::Eager,
+			EncodingType::Lazy,
+		);
+		let b = IntVar::new_in(
+			&mut slv,
+			RangeList::from_iter([-3..=3]),
+			EncodingType::Eager,
+			EncodingType::Lazy,
+		);
+		slv.add_propagator(IntAbsBounds::prepare(a, b)).unwrap();
+		slv.expect_solutions(
+			&[a, b],
+			expect![[r#"
+    -3, 3
+    -2, 2
+    -1, 1
+    0, 0
+    1, 1
+    2, 2
+    3, 3"#]],
+		);
+	}
+}

share/minizinc/huub/redefinitions.mzn

@@ -4,8 +4,6 @@ predicate bool_lt(var bool: a, var bool: b) = not a /\ b;
 predicate bool_lt_imp(var bool: a, var bool: b, var bool: r) = r -> (not a /\ b);
 predicate bool_lt_reif(var bool: a, var bool: b, var bool: r) = r = (not a /\ b);
 
-predicate int_abs(var int: a, var int: b) = b = [a,-a][1 + (a < 0)];
-
 predicate int_eq_imp(var int: a, var int: b, var bool: r);
 predicate int_le_imp(var int: a, var int: b, var bool: r);
 predicate int_ne_imp(var int: a, var int: b, var bool: r);