Update tracing for propagators

crates/fzn-huub/src/tracing.rs

@@ -150,6 +150,26 @@ impl<'a, V: Visit> LitNames<'a, V> {
 		}
 		false
 	}
+
+	#[inline]
+	fn check_int_vars(&mut self, field: &Field, value: &dyn fmt::Debug) -> bool {
+		if matches!(field.name(), "int_vars") {
+			let res: Result<Vec<usize>, _> = serde_json::from_str(&format!("{:?}", value));
+			if let Ok(vars) = res {
+				let mut v: Vec<String> = Vec::with_capacity(vars.len());
+				for i in vars {
+					if let Some(name) = self.int_reverse_map.get(i) {
+						v.push(name.to_string());
+					} else {
+						v.push(format!("IntVar({})", i));
+					}
+				}
+				self.inner.record_str(field, &v.join(", "));
+				return true;
+			}
+		}
+		false
+	}
 }
 
 impl<'a, V: Visit> Visit for LitNames<'a, V> {
@@ -188,6 +208,9 @@ impl<'a, V: Visit> Visit for LitNames<'a, V> {
 		if self.check_clause(field, value) {
 			return;
 		}
+		if self.check_int_vars(field, value) {
+			return;
+		}
 		self.inner.record_debug(field, value)
 	}
 }

crates/huub/src/propagator/all_different.rs

@@ -1,5 +1,3 @@
-use tracing::trace;
-
 use super::{reason::ReasonBuilder, InitializationActions, PropagationActions};
 use crate::{
 	propagator::{conflict::Conflict, int_event::IntEvent, Propagator},
@@ -54,15 +52,11 @@ impl Propagator for AllDifferentValue {
 		self.action_list.clear()
 	}
 
+	#[tracing::instrument(name = "all_different", level = "trace", skip(self, actions))]
 	fn propagate(&mut self, actions: &mut dyn PropagationActions) -> Result<(), Conflict> {
 		while let Some(i) = self.action_list.pop() {
 			let var = self.vars[i as usize];
 			let val = actions.get_int_val(var).unwrap();
-			trace!(
-				int_var = ?var,
-				value = val,
-				"value propagation all_different",
-			);
 			let reason = ReasonBuilder::Simple(actions.get_int_lit(var, LitMeaning::Eq(val)));
 			for (j, &v) in self.vars.iter().enumerate() {
 				let j_val = actions.get_int_val(v);

crates/huub/src/propagator/int_lin_le.rs

@@ -1,5 +1,3 @@
-use tracing::trace;
-
 use super::{reason::ReasonBuilder, ExplainActions, InitializationActions, PropagationActions};
 use crate::{
 	propagator::{conflict::Conflict, int_event::IntEvent, Propagator},
@@ -68,6 +66,7 @@ impl Propagator for LinearLE {
 	}
 
 	// propagation rule: x[i] <= rhs - sum_{j != i} x[j].lower_bound
+	#[tracing::instrument(name = "int_lin_le", level = "trace", skip(self, actions))]
 	fn propagate(&mut self, actions: &mut dyn PropagationActions) -> Result<(), Conflict> {
 		// sum the coefficients x var.lower_bound
 		let max_sum = self
@@ -77,11 +76,6 @@ impl Propagator for LinearLE {
 			.fold(self.rhs, |sum, val| sum - val);
 		// propagate the upper bound of the variables
 		for (j, &v) in self.vars.iter().enumerate() {
-			trace!(
-				int_var = ?v,
-				value = max_sum + actions.get_int_lower_bound(v),
-				"bounds propagation linear_le",
-			);
 			let reason = ReasonBuilder::Lazy(j as u64);
 			actions.set_int_upper_bound(v, max_sum + actions.get_int_lower_bound(v), &reason)?
 		}

crates/huub/src/propagator/minimum.rs

@@ -54,6 +54,7 @@ impl Propagator for Minimum {
 		self.y_change = false;
 	}
 
+	#[tracing::instrument(name = "array_int_minimum", level = "trace", skip(self, actions))]
 	fn propagate(&mut self, actions: &mut dyn PropagationActions) -> Result<(), Conflict> {
 		if !self.action_list.is_empty() {
 			let min_lb = self

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

@@ -13,7 +13,7 @@ use crate::{
 		view::{BoolViewInner, IntViewInner},
 		IntView, SatSolver,
 	},
-	BoolView, IntVal, Solver,
+	BoolView, IntVal, LinearTransform, NonZeroIntVal, Solver,
 };
 
 index_vec::define_index_type! {
@@ -59,11 +59,26 @@ impl IntVar {
 		Sol: PropagatorAccess + SatValuation,
 		Sat: SatSolver + SolverTrait<ValueFn = Sol>,
 	{
-		let orig_domain_len = (&domain)
-			.into_iter()
-			.map(|x| (*x.end() - *x.start() + 1) as usize)
+		let orig_domain_len = domain
+			.iter()
+			.map(|x| (x.end() - x.start() + 1) as usize)
 			.sum();
-		debug_assert!(orig_domain_len >= 2, "Domain must have at least two values");
+		assert!(
+			orig_domain_len > 1,
+			"Unable to create integer variable with singular or empty domain"
+		);
+		if orig_domain_len == 2 {
+			let lit = slv.oracle.new_var().into();
+			let lb = *domain.lower_bound().unwrap();
+			let ub = *domain.upper_bound().unwrap();
+			return IntView(IntViewInner::Bool {
+				transformer: LinearTransform {
+					scale: NonZeroIntVal::new(ub - lb).unwrap(),
+					offset: lb,
+				},
+				lit,
+			});
+		}
 
 		let mut num_vars = orig_domain_len - 1;
 		if direct_encoding {
@@ -157,14 +172,14 @@ impl IntVar {
 				}
 				// Calculate the offset in the VarRange
 				let mut offset = -1; // -1 to account for the lower bound
-				for r in &self.orig_domain {
-					if i < **r.start() {
+				for r in self.orig_domain.iter() {
+					if i < *r.start() {
 						break;
-					} else if r.contains(&&i) {
-						offset += i - *r.start();
+					} else if r.contains(&i) {
+						offset += i - r.start();
 						break;
 					} else {
-						offset += *r.end() - *r.start() + 1;
+						offset += r.end() - r.start() + 1;
 					}
 				}
 				// Look up the corresponding variable
@@ -187,14 +202,14 @@ impl IntVar {
 				} else {
 					// Calculate the offset in the VarRange
 					let mut offset = -1; // -1 to account for the lower bound
-					for r in &self.orig_domain {
-						if i < **r.start() {
+					for r in self.orig_domain.iter() {
+						if i < *r.start() {
 							return ret_const(false);
-						} else if r.contains(&&i) {
-							offset += i - *r.start();
+						} else if r.contains(&i) {
+							offset += i - r.start();
 							break;
 						} else {
-							offset += *r.end() - *r.start() + 1;
+							offset += r.end() - r.start() + 1;
 						}
 					}
 					debug_assert!(

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

@@ -1,5 +1,6 @@
 use delegate::delegate;
 use pindakaas::Lit as RawLit;
+use tracing::trace;
 
 use super::{int_var::IntVarRef, PropRef, State};
 use crate::{
@@ -33,15 +34,17 @@ impl<'a> PropagationActions for PropagationContext<'a> {
 					self.prop,
 				)),
 				None => {
+					let propagated_lit = if val { lit } else { !lit };
+					trace!(lit = i32::from(propagated_lit), "propagate bool");
 					let change = self
 						.state
 						.sat_trail
 						.assign(lit.var(), if lit.is_negated() { !val } else { val });
 					debug_assert_eq!(change, HasChanged::Changed);
-					let propagated_lit = if val { lit } else { !lit };
 					self.state
 						.register_reason(propagated_lit, reason, self.prop);
 					self.prop_queue.push(propagated_lit);
+					// TODO: Trigger Propagators
 					Ok(())
 				}
 			},
@@ -224,6 +227,7 @@ impl PropagationContext<'_> {
 		if self.check_satisfied(iv, &lit_req) {
 			return Ok(());
 		}
+		trace!(int_var = usize::from(iv), effect = ?lit_req, "propagate int");
 		let lit = match self.state.int_vars[iv].get_bool_lit(lit_req) {
 			BoolView(BoolViewInner::Lit(lit)) => lit,
 			BoolView(BoolViewInner::Const(false)) => {
@@ -233,7 +237,8 @@ impl PropagationContext<'_> {
 		};
 		self.state.register_reason(lit, reason, self.prop);
 		self.prop_queue.push(lit);
-		// TODO: Should this trigger notify?
+		// TODO: Update domain
+		// TODO: Trigger Propagators
 		// TODO: Check conflict
 		Ok(())
 	}

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

@@ -84,8 +84,10 @@ impl SatTrail {
 	}
 
 	pub(crate) fn assign(&mut self, var: RawVar, val: bool) -> HasChanged {
-		if let Some(x) = self.value.insert(var, val) {
-			debug_assert_eq!(x, val);
+		if self.value.insert(var, val).is_some() {
+			// Variable was updated with a new value
+			// This might be a new (inconsistent) value if the SAT solver is still propagating given
+			// literals.
 			return HasChanged::NoChange;
 		}
 		if !self.prev_len.is_empty() {