Add integer equality constraint for when unification is impossible

Resolves #149

Author: Dekker1

crates/huub/src/constraints/int_linear.rs

@@ -21,6 +21,15 @@ use crate::{
 	BoolDecision, BoolFormula, Conjunction, IntDecision, IntVal,
 };
 
+/// Representation of an integer equality constraint that cannot be unified.
+///
+/// This constraint enforces that two integer decisions take the same value.
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub(crate) struct IntEq {
+	/// The two integer decisions that must be equal.
+	pub(crate) vars: [IntDecision; 2],
+}
+
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
 /// Representation of an integer linear constraint within a model.
 ///
@@ -43,7 +52,7 @@ pub struct IntLinear {
 pub type IntLinearLessEqBounds = IntLinearLessEqBoundsImpl<0>;
 
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
-/// Value consistent propagator for the `int_lin_le` or `int_lin_le_imp`
+/// Bounds consistent propagator for the `int_lin_le` or `int_lin_le_imp`
 /// constraint.
 ///
 /// `R` should be `0` if the propagator is not refied, or `1` if it is. Other
@@ -104,6 +113,45 @@ pub(crate) enum Reification {
 	ReifiedBy(BoolDecision),
 }
 
+impl<S: SimplificationActions> Constraint<S> for IntEq {
+	fn simplify(&mut self, actions: &mut S) -> Result<SimplificationStatus, ReformulationError> {
+		let (lb_0, ub_0) = actions.get_int_bounds(self.vars[0]);
+		let (lb_1, ub_1) = actions.get_int_bounds(self.vars[1]);
+
+		if lb_0 == ub_0 {
+			actions.set_int_val(self.vars[1], lb_0)?;
+			return Ok(SimplificationStatus::Subsumed);
+		}
+		if lb_1 == ub_1 {
+			actions.set_int_val(self.vars[0], lb_1)?;
+			return Ok(SimplificationStatus::Subsumed);
+		}
+		if lb_0 >= lb_1 {
+			actions.set_int_lower_bound(self.vars[1], lb_0)?;
+		}
+		if lb_1 >= lb_0 {
+			actions.set_int_lower_bound(self.vars[0], lb_1)?;
+		}
+		if ub_0 <= ub_1 {
+			actions.set_int_upper_bound(self.vars[1], ub_0)?;
+		}
+		if ub_1 <= ub_0 {
+			actions.set_int_upper_bound(self.vars[0], ub_1)?;
+		}
+		Ok(SimplificationStatus::Fixpoint)
+	}
+
+	fn to_solver(&self, actions: &mut dyn ReformulationActions) -> Result<(), ReformulationError> {
+		let lin = IntLinear {
+			terms: vec![self.vars[0], -self.vars[1]],
+			operator: LinOperator::Equal,
+			rhs: 0,
+			reif: None,
+		};
+		<IntLinear as Constraint<S>>::to_solver(&lin, actions)
+	}
+}
+
 impl IntLinear {
 	/// Change the integer linear constraint to be implied by the given Boolean
 	/// decision variable.

crates/huub/src/lib.rs

@@ -54,7 +54,7 @@ use crate::{
 		int_array_minimum::IntArrayMinimum,
 		int_div::IntDiv,
 		int_in_set::IntInSetReif,
-		int_linear::{IntLinear, LinOperator},
+		int_linear::{IntEq, IntLinear, LinOperator},
 		int_pow::IntPow,
 		int_table::IntTable,
 		int_times::IntTimes,
@@ -971,6 +971,7 @@ impl Model {
 			ConstraintStore::DisjunctiveStrict(c) => c.simplify(self),
 			ConstraintStore::IntAbs(c) => c.simplify(self),
 			ConstraintStore::IntDiv(c) => c.simplify(self),
+			ConstraintStore::IntEq(c) => c.simplify(self),
 			ConstraintStore::IntLinear(c) => c.simplify(self),
 			ConstraintStore::IntPow(c) => c.simplify(self),
 			ConstraintStore::IntTimes(c) => c.simplify(self),
@@ -1055,6 +1056,9 @@ impl Model {
 			ConstraintStore::IntDiv(con) => {
 				<IntDiv as Constraint<Model>>::initialize(con, &mut ctx);
 			}
+			ConstraintStore::IntEq(con) => {
+				<IntEq as Constraint<Model>>::initialize(con, &mut ctx);
+			}
 			ConstraintStore::IntLinear(con) => {
 				<IntLinear as Constraint<Model>>::initialize(con, &mut ctx);
 			}
@@ -1256,6 +1260,12 @@ impl AddAssign<IntDiv> for Model {
 	}
 }
 
+impl AddAssign<IntEq> for Model {
+	fn add_assign(&mut self, constraint: IntEq) {
+		self.add_constraint(ConstraintStore::IntEq(constraint));
+	}
+}
+
 impl AddAssign<IntInSetReif> for Model {
 	fn add_assign(&mut self, constraint: IntInSetReif) {
 		self.add_constraint(ConstraintStore::IntInSetReif(constraint));
@@ -1853,7 +1863,8 @@ impl SimplificationActions for Model {
 				} else if can_define_x {
 					((x_t, x_i), (y_t, y_i))
 				} else {
-					todo!()
+					*self += IntEq { vars: [x, y] };
+					return Ok(());
 				};
 
 				// Perform the transformation and add the aliasing domain to x:

crates/huub/src/reformulate.rs

@@ -42,8 +42,8 @@ use crate::{
 		trail::TrailedInt,
 		BoolView, BoolViewInner, IntView, IntViewInner, View,
 	},
-	BoolDecision, BoolFormula, Decision, IntDecision, IntLitMeaning, IntSetVal, IntVal, Model,
-	Solver,
+	BoolDecision, BoolFormula, Decision, IntDecision, IntEq, IntLitMeaning, IntSetVal, IntVal,
+	Model, Solver,
 };
 
 #[derive(Clone, Debug, Eq, Hash, PartialEq)]
@@ -99,6 +99,7 @@ pub(crate) enum ConstraintStore {
 	IntArrayMinimum(IntArrayMinimum),
 	IntDecisionArrayElement(IntDecisionArrayElement),
 	IntDiv(IntDiv),
+	IntEq(IntEq),
 	IntInSetReif(IntInSetReif),
 	IntLinear(IntLinear),
 	IntPow(IntPow),
@@ -266,6 +267,9 @@ impl ConstraintStore {
 			ConstraintStore::IntDiv(con) => {
 				<IntDiv as Constraint<Model>>::to_solver(con, &mut actions)
 			}
+			ConstraintStore::IntEq(con) => {
+				<IntEq as Constraint<Model>>::to_solver(con, &mut actions)
+			}
 			ConstraintStore::IntInSetReif(con) => {
 				<IntInSetReif as Constraint<Model>>::to_solver(con, &mut actions)
 			}

crates/huub/src/tests.rs

@@ -28,6 +28,28 @@ fn it_works() {
 	);
 }
 
+#[test]
+fn unification_impossible() {
+	let mut prb = Model::default();
+	let a = prb.new_int_var((1..=5).into());
+	let b = prb.new_int_var((1..=2).into());
+
+	let lin = (a * 2 - b * 5).eq(0);
+	prb += lin;
+
+	let (mut slv, map): (Solver, _) = prb.to_solver(&InitConfig::default()).unwrap();
+	let a = map.get_int(&mut slv, a);
+	let b = map.get_int(&mut slv, b);
+
+	assert_eq!(
+		slv.solve(|value| {
+			assert_eq!(value(a.into()), Value::Int(5));
+			assert_eq!(value(b.into()), Value::Int(2));
+		}),
+		SolveResult::Satisfied
+	);
+}
+
 impl Model {
 	pub(crate) fn assert_unsatisfiable(&mut self) {
 		let err: Result<(Solver, _), _> = self.to_solver(&InitConfig::default());