Add IntView::Const as initial way to deal with constants in constraints

crates/fzn-huub/src/tracing.rs

@@ -129,7 +129,7 @@ impl<'a, V: Visit> LitNames<'a, V> {
 
 	#[inline]
 	fn check_clause(&mut self, field: &Field, value: &dyn fmt::Debug) -> bool {
-		if matches!(field.name(), "clause") {
+		if matches!(field.name(), "clause" | "lits") {
 			let res: Result<Vec<i32>, _> = serde_json::from_str(&format!("{:?}", value));
 			if let Ok(clause) = res {
 				let mut v: Vec<String> = Vec::with_capacity(clause.len());
@@ -140,7 +140,11 @@ impl<'a, V: Visit> LitNames<'a, V> {
 						v.push(format!("Lit({})", i));
 					}
 				}
-				self.inner.record_str(field, &v.join(" ∨ "));
+				if field.name() == "clause" {
+					self.inner.record_str(field, &v.join(" ∨ "));
+				} else {
+					self.inner.record_str(field, &v.join(", "));
+				}
 				return true;
 			}
 		}

crates/huub/src/model.rs

@@ -16,8 +16,8 @@ pub use self::{
 use crate::{
 	model::int::IntVarDef,
 	propagator::all_different::AllDifferentValue,
-	solver::{engine::int_var::IntVar as SlvIntVar, BoolView, SatSolver},
-	Solver,
+	solver::{engine::int_var::IntVar as SlvIntVar, view::IntViewInner, BoolView, SatSolver},
+	IntView, Solver,
 };
 
 #[derive(Debug, Default)]
@@ -108,18 +108,13 @@ impl Constraint {
 				}
 			}
 			Constraint::AllDifferent(v) => {
-				let (vars, vals): (Vec<_>, _) = v
+				let vars: Vec<_> = v
 					.iter()
 					.map(|v| v.to_arg(ReifContext::Mixed, slv, map))
-					.partition(|x| matches!(x, SimplifiedInt::Var(_)));
-				if !vals.is_empty() {
-					todo!()
-				}
-				slv.add_propagator(AllDifferentValue::new(vars.into_iter().map(|v| {
-					let SimplifiedInt::Var(v) = v else {
-						unreachable!()
-					};
-					v
+					.collect();
+				slv.add_propagator(AllDifferentValue::new(vars.into_iter().map(|v| match v {
+					SimplifiedInt::Val(i) => IntView(IntViewInner::Const(i)),
+					SimplifiedInt::Var(v) => v,
 				})))
 			}
 		}

crates/huub/src/propagator.rs

@@ -19,14 +19,20 @@ use crate::{
 
 pub trait Propagator: Debug {
 	/// The method called by the solver to notify the propagator of a variable
-	/// event to which it has subscribed. The propagator can choose a priority
-	/// level if it wants to be placed in the propagation queue.
+	/// event to which it has subscribed. The method returns true if the
+	/// propagator should be placed in the propagation queue.
 	///
 	/// The [`data`] argument will contain the data that the propagater has set
 	/// when subscribing to an event.
-	fn notify_event(&mut self, data: u32) -> Option<PriorityLevel> {
+	fn notify_event(&mut self, data: u32) -> bool {
 		let _ = data;
-		Some(PriorityLevel::Medium)
+		false
+	}
+
+	/// The method called by the solver to request at what priority level the
+	/// propagator should be placed in the propagation queue.œ
+	fn queue_priority_level(&self) -> PriorityLevel {
+		PriorityLevel::Medium
 	}
 
 	/// This method is called when the solver backtracks to a previous decision
@@ -59,10 +65,13 @@ pub trait Propagator: Debug {
 }
 
 pub trait Initialize {
-	/// The method called when registering a propagator with the solver. This
-	/// method is generally used to register variable event subscriptions with the
-	/// solver.
-	fn initialize<Sat: SatSolver>(&mut self, actions: &mut InitializationActions<'_, Sat>) {
+	/// The method called when registering a propagator with the solver, the method
+	/// returns true when the propagator needs to be enqued immediately.œ
+	///
+	/// This method is generally used to register variable event
+	/// subscriptions with the solver.
+	fn initialize<Sat: SatSolver>(&mut self, actions: &mut InitializationActions<'_, Sat>) -> bool {
 		let _ = actions;
+		false
 	}
 }

crates/huub/src/propagator/all_different.rs

@@ -5,6 +5,7 @@ use crate::{
 	},
 	solver::{
 		engine::{int_var::LitMeaning, queue::PriorityLevel},
+		view::IntViewInner,
 		IntView, SatSolver,
 	},
 };
@@ -17,17 +18,30 @@ pub struct AllDifferentValue {
 
 impl AllDifferentValue {
 	pub fn new<V: Into<IntView>, I: IntoIterator<Item = V>>(vars: I) -> Self {
-		Self {
-			vars: vars.into_iter().map(Into::into).collect(),
-			action_list: Vec::new(),
-		}
+		let vars: Vec<IntView> = vars.into_iter().map(Into::into).collect();
+		let action_list = vars
+			.iter()
+			.enumerate()
+			.filter_map(|(i, v)| {
+				if matches!(v.0, IntViewInner::Const(_)) {
+					Some(i as u32)
+				} else {
+					None
+				}
+			})
+			.collect();
+		Self { vars, action_list }
 	}
 }
 
 impl Propagator for AllDifferentValue {
-	fn notify_event(&mut self, data: u32) -> Option<PriorityLevel> {
+	fn notify_event(&mut self, data: u32) -> bool {
 		self.action_list.push(data);
-		Some(PriorityLevel::Low)
+		true
+	}
+
+	fn queue_priority_level(&self) -> PriorityLevel {
+		PriorityLevel::Low
 	}
 
 	fn notify_backtrack(&mut self, _new_level: usize) {
@@ -38,11 +52,13 @@ impl Propagator for AllDifferentValue {
 		while let Some(i) = self.action_list.pop() {
 			let var = self.vars[i as usize];
 			let val = actions.get_int_val(var).unwrap();
-			let lit = actions.get_int_lit(var, LitMeaning::Eq(val));
+			let r = actions
+				.get_int_lit(var, LitMeaning::Eq(val))
+				.map(Reason::Simple);
 			for (j, &v) in self.vars.iter().enumerate() {
 				let j_val = actions.get_int_val(v);
 				if (j as u32) != i && (j_val.is_none() || j_val.unwrap() == val) {
-					actions.set_int_not_eq(v, val, Reason::Simple(lit))?
+					actions.set_int_not_eq(v, val, r.clone())?
 				}
 			}
 		}
@@ -51,10 +67,11 @@ impl Propagator for AllDifferentValue {
 }
 
 impl Initialize for AllDifferentValue {
-	fn initialize<Sat: SatSolver>(&mut self, actions: &mut InitializationActions<'_, Sat>) {
+	fn initialize<Sat: SatSolver>(&mut self, actions: &mut InitializationActions<'_, Sat>) -> bool {
 		for (i, v) in self.vars.iter().enumerate() {
 			actions.subscribe_int(*v, IntEvent::Fixed, i as u32)
 		}
+		!self.action_list.is_empty()
 	}
 }
 
@@ -95,6 +112,6 @@ mod tests {
 		let c = IntVar::new_in(&mut slv, RangeList::from_iter([1..=2]), true);
 
 		slv.add_propagator(AllDifferentValue::new(vec![a, b, c]));
-		assert_eq!(slv.solve(|_| { assert!(false) }), SolveResult::Unsat)
+		assert_eq!(slv.solve(|_| { unreachable!() }), SolveResult::Unsat)
 	}
 }

crates/huub/src/propagator/init_action.rs

@@ -35,6 +35,7 @@ impl<Sat: SatSolver> InitializationActions<'_, Sat> {
 				.entry(var)
 				.or_default()
 				.push((self.prop_ref, event, data)),
+			Const(_) => {}
 		}
 	}
 }

crates/huub/src/propagator/propagation_action.rs

@@ -30,27 +30,27 @@ pub struct PropagationActions<'a> {
 impl PropagationActions<'_> {
 	#[allow(dead_code)] // TODO
 	pub fn get_bool_val(&self, lit: RawLit) -> Option<bool> {
-		let is_neg = lit.is_negated();
-		self.sat_trail
-			.get(lit.var())
-			.map(|v| if is_neg { !v } else { v })
+		self.sat_trail.get(lit)
 	}
 
-	pub fn get_int_lit(&mut self, var: IntView, bv: LitMeaning) -> RawLit {
+	pub fn get_int_lit(&mut self, var: IntView, bv: LitMeaning) -> Option<RawLit> {
 		match var.0 {
-			IntViewInner::VarRef(iv) => self.int_vars[iv].get_bool_var(bv),
+			IntViewInner::VarRef(iv) => Some(self.int_vars[iv].get_bool_var(bv)),
+			IntViewInner::Const(_) => None,
 		}
 	}
 
 	pub fn get_int_lower_bound(&self, var: IntView) -> IntVal {
 		match var.0 {
 			IntViewInner::VarRef(iv) => self.int_trail[self.int_vars[iv].lower_bound],
+			IntViewInner::Const(i) => i,
 		}
 	}
 
 	pub fn get_int_upper_bound(&self, var: IntView) -> IntVal {
 		match var.0 {
 			IntViewInner::VarRef(iv) => self.int_trail[self.int_vars[iv].upper_bound],
+			IntViewInner::Const(i) => i,
 		}
 	}
 
@@ -64,15 +64,129 @@ impl PropagationActions<'_> {
 		}
 	}
 
-	pub fn set_int_not_eq(&mut self, var: IntView, val: i64, r: Reason) -> Result<(), Conflict> {
+	pub fn check_int_in_domain(&self, var: IntView, val: IntVal) -> bool {
 		match var.0 {
 			IntViewInner::VarRef(iv) => {
+				let lb = self.get_int_lower_bound(var);
+				let ub = self.get_int_upper_bound(var);
+				if (lb..=ub).contains(&val) {
+					let lit = self.int_vars[iv].get_bool_var(LitMeaning::Eq(val));
+					self.sat_trail.get(lit).unwrap_or(true)
+				} else {
+					false
+				}
+			}
+			IntViewInner::Const(i) => i == val,
+		}
+	}
+
+	#[allow(dead_code)]
+	pub fn set_int_lower_bound(
+		&mut self,
+		var: IntView,
+		val: IntVal,
+		r: Option<Reason>,
+	) -> Result<(), Conflict> {
+		match var.0 {
+			IntViewInner::VarRef(iv) => {
+				if self.get_int_lower_bound(var) >= val {
+					return Ok(());
+				}
+				let lit = self.int_vars[iv].get_bool_var(LitMeaning::GreaterEq(val));
+				if let Some(r) = r {
+					self.reason_map.insert(lit, r);
+				}
+				self.lit_queue.push(lit);
+			}
+			IntViewInner::Const(i) => {
+				if i < val {
+					todo!()
+				}
+			}
+		}
+		Ok(())
+	}
+
+	#[allow(dead_code)]
+	pub fn set_int_upper_bound(
+		&mut self,
+		var: IntView,
+		val: IntVal,
+		r: Option<Reason>,
+	) -> Result<(), Conflict> {
+		match var.0 {
+			IntViewInner::VarRef(iv) => {
+				if self.get_int_upper_bound(var) <= val {
+					return Ok(());
+				}
+				let lit = self.int_vars[iv].get_bool_var(LitMeaning::Less(val + 1));
+				if let Some(r) = r {
+					self.reason_map.insert(lit, r);
+				}
+				self.lit_queue.push(lit);
+			}
+			IntViewInner::Const(i) => {
+				if i > val {
+					todo!()
+				}
+			}
+		}
+		Ok(())
+	}
+
+	#[allow(dead_code)]
+	pub fn set_int_val(
+		&mut self,
+		var: IntView,
+		val: IntVal,
+		r: Option<Reason>,
+	) -> Result<(), Conflict> {
+		match var.0 {
+			IntViewInner::VarRef(iv) => {
+				if self.get_int_val(var) == Some(val) {
+					return Ok(());
+				}
+				let lit = self.int_vars[iv].get_bool_var(LitMeaning::Eq(val));
+				if let Some(r) = r {
+					self.reason_map.insert(lit, r);
+				}
+				self.lit_queue.push(lit);
+				// TODO: Should this trigger notify?
+				// TODO: Check conflict
+			}
+			IntViewInner::Const(i) => {
+				if i != val {
+					todo!()
+				}
+			}
+		};
+		Ok(())
+	}
+
+	pub fn set_int_not_eq(
+		&mut self,
+		var: IntView,
+		val: IntVal,
+		r: Option<Reason>,
+	) -> Result<(), Conflict> {
+		match var.0 {
+			IntViewInner::VarRef(iv) => {
+				if !self.check_int_in_domain(var, val) {
+					return Ok(());
+				}
 				let lit = self.int_vars[iv].get_bool_var(LitMeaning::NotEq(val));
-				self.reason_map.insert(lit, r);
+				if let Some(r) = r {
+					self.reason_map.insert(lit, r);
+				}
 				self.lit_queue.push(lit);
 				// TODO: Should this trigger notify?
 				// TODO: Check conflict
 			}
+			IntViewInner::Const(i) => {
+				if i == val {
+					todo!()
+				}
+			}
 		};
 		Ok(())
 	}

crates/huub/src/propagator/reason.rs

@@ -2,6 +2,7 @@ use pindakaas::Lit;
 
 use crate::solver::engine::PropRef;
 
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub enum Reason {
 	/// A promise that a given propagator will compute a causation of the change
 	/// when given the attached data

crates/huub/src/solver.rs

@@ -47,6 +47,7 @@ impl<Sat: SatSolver> Solver<Sat> {
 				SolverView::Bool(lit) => sat_value(lit.0).map(Value::Bool),
 				SolverView::Int(var) => match var.0 {
 					IntViewInner::VarRef(iv) => Some(Value::Int(int_vars[iv].get_value(sat_value))),
+					IntViewInner::Const(i) => Some(Value::Int(i)),
 				},
 			};
 			on_sol(wrapper);
@@ -78,8 +79,13 @@ impl<Sat: SatSolver> Solver<Sat> {
 			prop_ref,
 			slv: self,
 		};
-		prop.initialize(&mut actions);
+		let enqueue = prop.initialize(&mut actions);
+		if enqueue {
+			let level = prop.queue_priority_level();
+			self.engine_mut().prop_queue.insert(level, prop_ref);
+		}
 		self.engine_mut().propagators.push(Box::new(prop));
+		self.engine_mut().enqueued.push(enqueue);
 	}
 }