Add support for the table_int constraint

crates/huub/src/model.rs

@@ -96,7 +96,7 @@ impl Model {
 	pub fn new_int_vars(&mut self, len: usize, domain: RangeList<i64>) -> Vec<IntVar> {
 		let iv = IntVar(self.int_vars.len() as u32);
 		self.int_vars
-			.extend(repeat(IntVarDef::with_domain(domain)).take(len - 1));
+			.extend(repeat(IntVarDef::with_domain(domain)).take(len));
 		(0..len).map(|i| IntVar(iv.0 + i as u32)).collect()
 	}
 
@@ -153,6 +153,13 @@ impl Model {
 				Constraint::ArrayVarIntElement(_, IntView::Var(iv) | IntView::Linear(_, iv), _) => {
 					let _ = eager_direct.insert(*iv);
 				}
+				Constraint::TableInt(vars, _) => {
+					for v in vars {
+						if let IntView::Var(iv) | IntView::Linear(_, iv) = v {
+							let _ = eager_direct.insert(*iv);
+						}
+					}
+				}
 				_ => {}
 			}
 		}

crates/huub/src/model/constraint.rs

@@ -21,6 +21,7 @@ use crate::{
 		int_lin_ne::{IntLinearNotEqImpValue, IntLinearNotEqValue},
 		int_pow::IntPowBounds,
 		int_times::IntTimesBounds,
+		table_int::encode_table_int_gac,
 	},
 	solver::{
 		engine::Engine,
@@ -119,6 +120,10 @@ pub enum Constraint {
 	/// takes the value `true` if-and-only-if an integer variable is in a given
 	/// set.
 	SetInReif(IntView, IntSetVal, BoolExpr),
+	/// `table_int` constraint, which enforces that the given list of integer
+	/// views take their values according to one of the given list of integer
+	/// values.
+	TableInt(Vec<IntView>, Vec<Vec<IntVal>>),
 }
 
 impl Constraint {
@@ -448,6 +453,7 @@ impl Constraint {
 					BoolExpr::Equiv(vec![r.clone(), BoolExpr::Or(eq_lits)]).constrain(slv, map)
 				}
 			}
+			Constraint::TableInt(vars, vals) => encode_table_int_gac(slv, map, vars, vals),
 		}
 	}
 }
@@ -682,6 +688,47 @@ impl Model {
 
 				Some(Constraint::IntTimes(x, y, z))
 			}
+			Constraint::TableInt(vars, table) => {
+				debug_assert!(!vars.is_empty());
+				if vars.len() == 1 {
+					let dom = table.into_iter().map(|v| v[0]..=v[0]).collect();
+					self.intersect_int_domain(&vars[0], &dom, con)?;
+					None
+				} else {
+					// Remove any tuples that contain values outside of the domain of the
+					// variables.
+					let table = table
+						.into_iter()
+						.filter(|tup| {
+							tup.iter()
+								.enumerate()
+								.all(|(j, val)| self.check_int_in_domain(&vars[j], *val))
+						})
+						.collect_vec();
+
+					// If no tuples remain, then the problem is trivially unsatisfiable.
+					if table.is_empty() {
+						return Err(ReformulationError::TrivialUnsatisfiable);
+					}
+
+					// Restrict the domain of the variables to the values it can take in the
+					// tuple.
+					if table.len() == 1 {
+						for (j, var) in vars.iter().enumerate() {
+							self.set_int_value(var, table[0][j], con)?;
+						}
+						None
+					} else {
+						for (j, var) in vars.iter().enumerate() {
+							let dom = (0..table.len())
+								.map(|i| table[i][j]..=table[i][j])
+								.collect();
+							self.intersect_int_domain(var, &dom, con)?;
+						}
+						Some(Constraint::TableInt(vars, table))
+					}
+				}
+			}
 			con => Some(con),
 		};
 		match simplified {

crates/huub/src/model/flatzinc.rs

@@ -1117,6 +1117,36 @@ where
 						});
 					}
 				}
+				"huub_table_int" => {
+					if let [args, table] = c.args.as_slice() {
+						let args = self.arg_array(args)?;
+						let args: Vec<_> = args.iter().map(|l| self.lit_int(l)).try_collect()?;
+						let table = self.arg_array(table)?;
+						let table: Vec<_> = table.iter().map(|l| self.par_int(l)).try_collect()?;
+						if args.is_empty() || (table.len() % args.len()) != 0 {
+							return Err(FlatZincError::InvalidArgumentType {
+								expected: "array of n integers, where n is divisible by the number of variables",
+								found: format!("array of {} integers, to give values to {} variables", table.len(), args.len()),
+							});
+						}
+						if table.is_empty() {
+							return Err(ReformulationError::TrivialUnsatisfiable.into());
+						}
+						let table: Vec<Vec<_>> = table
+							.into_iter()
+							.chunks(args.len())
+							.into_iter()
+							.map(|c| c.collect())
+							.collect();
+						self.prb += Constraint::TableInt(args, table);
+					} else {
+						return Err(FlatZincError::InvalidNumArgs {
+							name: "huub_table_int",
+							found: c.args.len(),
+							expected: 2,
+						});
+					}
+				}
 				"int_abs" => {
 					if let [origin, abs] = c.args.as_slice() {
 						let origin = self.arg_int(origin)?;

crates/huub/src/model/int.rs

@@ -84,6 +84,12 @@ impl From<BoolView> for IntView {
 	}
 }
 
+impl From<IntVar> for IntView {
+	fn from(value: IntVar) -> Self {
+		Self::Var(value)
+	}
+}
+
 impl Mul<IntVal> for IntView {
 	type Output = Self;
 
@@ -125,6 +131,25 @@ impl Neg for IntView {
 }
 
 impl Model {
+	/// Check whether a given integer is within the set of possible values that a
+	/// given integer view can take.
+	pub(crate) fn check_int_in_domain(&self, iv: &IntView, val: IntVal) -> bool {
+		match iv {
+			IntView::Var(v) => self.int_vars[v.0 as usize].domain.contains(&val),
+			IntView::Const(v) => *v == val,
+			IntView::Linear(t, v) => match t.rev_transform_lit(LitMeaning::Eq(val)) {
+				Ok(LitMeaning::Eq(val)) => self.int_vars[v.0 as usize].domain.contains(&val),
+				Err(false) => false,
+				_ => unreachable!(),
+			},
+			IntView::Bool(t, _) => match t.rev_transform_lit(LitMeaning::Eq(val)) {
+				Ok(LitMeaning::Eq(val)) => val == 0 || val == 1,
+				Err(false) => false,
+				_ => unreachable!(),
+			},
+		}
+	}
+
 	/// Ensure that a given integer view cannot take any of the values in the
 	/// given set.
 	pub(crate) fn diff_int_domain(

crates/huub/src/propagator.rs

@@ -10,6 +10,7 @@ pub(crate) mod int_lin_le;
 pub(crate) mod int_lin_ne;
 pub(crate) mod int_pow;
 pub(crate) mod int_times;
+pub(crate) mod table_int;
 
 use std::{
 	error::Error,

crates/huub/src/propagator/table_int.rs

@@ -0,0 +1,182 @@
+//! Propagation methods for the `table_int` constraint, which constraints a
+//! sequence of integer decision variable to be assigned to a set of possible
+//! sequences of integer values.
+
+use itertools::Itertools;
+use pindakaas::{solver::propagation::PropagatingSolver, VarRange};
+
+use crate::{
+	actions::InspectionActions,
+	model::{int::IntView, reformulate::VariableMap},
+	solver::engine::Engine,
+	BoolView, IntVal, LitMeaning, ReformulationError, Solver,
+};
+
+/// Encode a [`Constraint::TableInt`] constraint into clauses in the solver such
+/// that using clausal propagation will enforce global arc consistency.
+pub(crate) fn encode_table_int_gac<Oracle: PropagatingSolver<Engine>>(
+	slv: &mut Solver<Oracle>,
+	map: &mut VariableMap,
+	vars: &[IntView],
+	vals: &[Vec<IntVal>],
+) -> Result<(), ReformulationError> {
+	assert!(vars.len() >= 2);
+
+	let selector = if vars.len() != 2 {
+		slv.oracle.new_var_range(vals.len())
+	} else {
+		VarRange::empty()
+	};
+	let vars = vars.iter().map(|iv| map.get_int(slv, iv)).collect_vec();
+
+	// Create clauses that say foreach tuple i, if `selector[i]` is true, then the
+	// variable `j` equals `vals[i][j]`.
+	if vars.len() != 2 {
+		for (i, tup) in vals.iter().enumerate() {
+			assert!(tup.len() == vars.len());
+			let lit: BoolView = selector.index(i).into();
+			for (j, var) in vars.iter().enumerate() {
+				let clause = [!lit, slv.get_int_lit(*var, LitMeaning::Eq(tup[j]))];
+				slv.add_clause(clause)?;
+			}
+		}
+	}
+
+	// Create clauses that map from the value taken by the variables back to the
+	// possible selectors that can be active.
+	for (j, var) in vars.iter().enumerate() {
+		let (lb, ub) = slv.get_int_bounds(*var);
+		let mut support_clauses: Vec<Vec<BoolView>> = vec![Vec::new(); (ub - lb + 1) as usize];
+		for (i, tup) in vals.iter().enumerate() {
+			let k = tup[j] - lb;
+			if !(0..support_clauses.len() as IntVal).contains(&k) {
+				// Value is not in the domain of the variable, so this tuple should not
+				// be considered.
+				continue;
+			}
+			// Add tuple i to be in support of value `k`.
+			if vars.len() == 2 {
+				// Special case where we can use the values of the other variables as
+				// the selection variables directly.
+				support_clauses[k as usize]
+					.push(slv.get_int_lit(vars[1 - j], LitMeaning::Eq(tup[1 - j])));
+			} else {
+				support_clauses[k as usize].push(selector.index(i).into());
+			}
+		}
+		for (i, mut clause) in support_clauses.into_iter().enumerate() {
+			if slv.check_int_in_domain(*var, lb + i as IntVal) {
+				clause.push(slv.get_int_lit(vars[j], LitMeaning::NotEq(lb + i as IntVal)));
+				slv.add_clause(clause)?;
+			}
+		}
+	}
+
+	Ok(())
+}
+
+#[cfg(test)]
+mod tests {
+	use expect_test::expect;
+	use itertools::Itertools;
+
+	use crate::{model::ModelView, Constraint, InitConfig, Model};
+
+	#[test]
+	fn test_binary_table_sat() {
+		let mut prb = Model::default();
+		let vars = prb.new_int_vars(3, (1..=5).into());
+		let table = vec![
+			vec![1, 3],
+			vec![1, 4],
+			vec![2, 4],
+			vec![2, 5],
+			vec![3, 1],
+			vec![3, 5],
+			vec![4, 1],
+			vec![4, 2],
+			vec![5, 2],
+			vec![5, 3],
+		];
+		prb += Constraint::TableInt(vec![vars[0].into(), vars[1].into()], table.clone());
+		prb += Constraint::TableInt(vec![vars[1].into(), vars[2].into()], table.clone());
+
+		let (mut slv, map) = prb.to_solver(&InitConfig::default()).unwrap();
+		let vars = vars
+			.into_iter()
+			.map(|x| map.get(&mut slv, &ModelView::Int(x.into())))
+			.collect_vec();
+		slv.expect_solutions(
+			&vars,
+			expect![[r#"
+    1, 3, 1
+    1, 3, 5
+    1, 4, 1
+    1, 4, 2
+    2, 4, 1
+    2, 4, 2
+    2, 5, 2
+    2, 5, 3
+    3, 1, 3
+    3, 1, 4
+    3, 5, 2
+    3, 5, 3
+    4, 1, 3
+    4, 1, 4
+    4, 2, 4
+    4, 2, 5
+    5, 2, 4
+    5, 2, 5
+    5, 3, 1
+    5, 3, 5"#]],
+		);
+	}
+
+	#[test]
+	fn test_tertiary_table_sat() {
+		let mut prb = Model::default();
+		let vars = prb.new_int_vars(5, (1..=5).into());
+		let table = vec![
+			vec![1, 3, 1],
+			vec![1, 3, 5],
+			vec![2, 4, 2],
+			vec![3, 1, 3],
+			vec![3, 5, 3],
+			vec![4, 2, 4],
+			vec![5, 3, 1],
+			vec![5, 3, 5],
+		];
+		prb += Constraint::TableInt(
+			vars[0..3].iter().cloned().map_into().collect_vec(),
+			table.clone(),
+		);
+		prb += Constraint::TableInt(
+			vars[2..5].iter().cloned().map_into().collect_vec(),
+			table.clone(),
+		);
+
+		let (mut slv, map) = prb.to_solver(&InitConfig::default()).unwrap();
+		let vars = vars
+			.into_iter()
+			.map(|x| map.get(&mut slv, &ModelView::Int(x.into())))
+			.collect_vec();
+		slv.expect_solutions(
+			&vars,
+			expect![[r#"
+    1, 3, 1, 3, 1
+    1, 3, 1, 3, 5
+    1, 3, 5, 3, 1
+    1, 3, 5, 3, 5
+    2, 4, 2, 4, 2
+    3, 1, 3, 1, 3
+    3, 1, 3, 5, 3
+    3, 5, 3, 1, 3
+    3, 5, 3, 5, 3
+    4, 2, 4, 2, 4
+    5, 3, 1, 3, 1
+    5, 3, 1, 3, 5
+    5, 3, 5, 3, 1
+    5, 3, 5, 3, 5"#]],
+		);
+	}
+}

crates/huub/src/solver/view.rs

@@ -7,7 +7,7 @@ use std::{
 	ops::{Add, Mul, Neg, Not},
 };
 
-use pindakaas::{solver::propagation::PropagatingSolver, Lit as RawLit};
+use pindakaas::{solver::propagation::PropagatingSolver, Lit as RawLit, Var as RawVar};
 
 use crate::{
 	helpers::linear_transform::LinearTransform,
@@ -96,6 +96,18 @@ impl From<bool> for BoolView {
 	}
 }
 
+impl From<RawLit> for BoolView {
+	fn from(value: RawLit) -> Self {
+		BoolView(BoolViewInner::Lit(value))
+	}
+}
+
+impl From<RawVar> for BoolView {
+	fn from(value: RawVar) -> Self {
+		BoolView(BoolViewInner::Lit(value.into()))
+	}
+}
+
 impl Not for BoolView {
 	type Output = Self;
 

share/minizinc/huub/fzn_table_int.mzn

@@ -0,0 +1,4 @@
+predicate fzn_table_int(array[int] of var int: x, array[int, int] of int: t) =
+	huub_table_int(x, array1d(t));
+
+predicate huub_table_int(array[int] of var int: x, array[int] of int: t);