update to output propagator name

crates/huub/src/model.rs

@@ -86,6 +86,7 @@ impl Model {
 		if let Some(r) = any_slv.downcast_mut::<Cadical>() {
 			r.set_option("restart", config.restart() as i32);
 			r.set_option("vivify", config.vivification() as i32);
+			r.set_option("chrono", false as i32);
 		} else {
 			warn!("unknown solver: vivification and restart options are ignored");
 		}

crates/huub/src/propagator/all_different_int.rs

@@ -79,6 +79,10 @@ impl Poster for AllDifferentIntValuePoster {
 			},
 		))
 	}
+
+	fn name(&self) -> &'static str {
+		"AllDifferentIntValue"
+	}
 }
 
 #[cfg(test)]

crates/huub/src/propagator/array_int_minimum.rs

@@ -102,6 +102,10 @@ impl Poster for ArrayIntMinimumBoundsPoster {
 			},
 		))
 	}
+
+	fn name(&self) -> &'static str {
+		"ArrayIntMinimumBounds"
+	}
 }
 
 #[cfg(test)]

crates/huub/src/propagator/array_var_int_element.rs

@@ -234,6 +234,10 @@ impl Poster for ArrayVarIntElementBoundsPoster {
 			},
 		))
 	}
+
+	fn name(&self) -> &'static str {
+		"ArrayVarIntElementBounds"
+	}
 }
 
 #[cfg(test)]

crates/huub/src/propagator/disjunctive_strict.rs

@@ -564,6 +564,10 @@ impl Poster for DisjunctiveEdgeFindingPoster {
 			},
 		))
 	}
+
+	fn name(&self) -> &'static str {
+		"DisjunctiveStrictEdgeFinding"
+	}
 }
 
 #[cfg(test)]

crates/huub/src/propagator/int_abs.rs

@@ -105,6 +105,10 @@ impl Poster for IntAbsBoundsPoster {
 			},
 		))
 	}
+
+	fn name(&self) -> &'static str {
+		"IntAbsBounds"
+	}
 }
 
 #[cfg(test)]

crates/huub/src/propagator/int_div.rs

@@ -247,6 +247,10 @@ impl Poster for IntDivBoundsPoster {
 			},
 		))
 	}
+
+	fn name(&self) -> &'static str {
+		"IntDivBounds"
+	}
 }
 
 #[cfg(test)]

crates/huub/src/propagator/int_lin_le.rs

@@ -179,6 +179,10 @@ impl<const R: usize> Poster for IntLinearLessEqBoundsPoster<R> {
 			},
 		))
 	}
+
+	fn name(&self) -> &'static str {
+		"IntLinearLessEqBounds"
+	}
 }
 
 #[cfg(test)]

crates/huub/src/propagator/int_lin_ne.rs

@@ -177,6 +177,10 @@ impl<const R: usize> Poster for IntLinearNotEqValuePoster<R> {
 			},
 		))
 	}
+
+	fn name(&self) -> &'static str {
+		"IntLinearNotEqValue"
+	}
 }
 
 #[cfg(test)]

crates/huub/src/propagator/int_pow.rs

@@ -289,6 +289,10 @@ impl Poster for IntPowBoundsPoster {
 			},
 		))
 	}
+
+	fn name(&self) -> &'static str {
+		"IntPowBounds"
+	}
 }
 
 fn pow(base: IntVal, exponent: IntVal) -> Option<IntVal> {

crates/huub/src/propagator/int_times.rs

@@ -138,6 +138,10 @@ impl Poster for IntTimesBoundsPoster {
 			},
 		))
 	}
+
+	fn name(&self) -> &'static str {
+		"IntTimesBounds"
+	}
 }
 
 #[cfg(test)]

crates/huub/src/solver.rs

@@ -153,6 +153,8 @@ where
 		functional: bool,
 	) -> Result<(), ReformulationError> {
 		let prop_ref = PropRef::from(self.engine().propagators.len());
+		let p = self.engine_mut().state.propagator_types.push(poster.name());
+		debug_assert_eq!(prop_ref, p);
 		let mut actions = InitializationContext {
 			slv: self,
 			init_ref: InitRef::Propagator(prop_ref),

crates/huub/src/solver/engine.rs

@@ -140,6 +140,8 @@ pub(crate) struct State {
 	pub(crate) activity_scores: IndexVec<PropRef, f64>,
 	/// Whether the propagator is functional
 	pub(crate) functional: IndexVec<PropRef, bool>,
+	/// Name of the propagator
+	pub(crate) propagator_types: IndexVec<PropRef, &'static str>,
 }
 
 impl IpasirPropagator for Engine {
@@ -434,7 +436,7 @@ impl State {
 						return None;
 					}
 					if i < lb || i > ub {
-						// Notified of invalid assignment, do nothing.
+						// TODO: Notification of an invalid assignment, do nothing.
 						//
 						// Although we do not expect this to happen, it seems that Cadical
 						// chronological backtracking might send notifications before
@@ -458,8 +460,12 @@ impl State {
 					if new_lb <= lb {
 						return None;
 					}
+					if new_lb > ub {
+						// TODO: Notification of an invalid assignment, do nothing.
+						trace!(lit = i32::from(lit), lb, ub, "invalid geq notification");
+						return None;
+					}
 					let prev = self.int_vars[iv].notify_lower_bound(&mut self.trail, new_lb);
-					debug_assert!(new_lb <= ub);
 					debug_assert!(prev < new_lb);
 					if new_lb == ub {
 						IntEvent::Fixed
@@ -472,8 +478,12 @@ impl State {
 					if new_ub >= ub {
 						return None;
 					}
+					if new_ub < lb {
+						// TODO: Notification of an invalid assignment, do nothing.
+						trace!(lit = i32::from(lit), lb, ub, "invalid less notification");
+						return None;
+					}
 					let prev = self.int_vars[iv].notify_upper_bound(&mut self.trail, new_ub);
-					debug_assert!(new_ub >= lb);
 					debug_assert!(new_ub < prev);
 					if new_ub == lb {
 						IntEvent::Fixed

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

@@ -1,7 +1,7 @@
 use delegate::delegate;
 use index_vec::IndexVec;
 use pindakaas::{solver::SolvingActions, Lit as RawLit};
-use tracing::trace;
+use tracing::{debug, trace};
 
 use crate::{
 	actions::{
@@ -77,17 +77,17 @@ impl<'a> SolvingContext<'a> {
 				self.state.conflict = Some(clause);
 				if !self.state.functional[p] {
 					self.state.activity_scores[p] += self.state.config.propagtor_additive_factor;
-					trace!(prop =? p, score =? self.state.activity_scores[p], "conflict detected");
 				}
+				debug!(prop =? self.state.propagator_types[p], score =? self.state.activity_scores[p], "conflict detected");
 			} else if propagation_before != self.state.propagation_queue.len() {
 				if !self.state.functional[p] {
 					self.state.activity_scores[p] += self.state.config.propagtor_additive_factor;
-					trace!(prop =? p, score =? self.state.activity_scores[p], "literal propagated");
 				}
+				debug!(prop =? self.state.propagator_types[p], propagated_literals =? self.state.propagation_queue.len() - propagation_before, score =? self.state.activity_scores[p], "literal propagated");
 			} else if !self.state.functional[p] {
 				// After wake-up, multiplicatively decay the activity score of the propagator if no propagations
 				self.state.activity_scores[p] *= self.state.config.propagtor_multiplicative_factor;
-				trace!(prop =? p, score =? self.state.activity_scores[p], "decay activity score");
+				debug!(prop =? self.state.propagator_types[p], score =? self.state.activity_scores[p], "no propagation, decay activity score");
 			}
 
 			if self.state.conflict.is_some() || !self.state.propagation_queue.is_empty() {

crates/huub/src/solver/poster.rs

@@ -24,6 +24,8 @@ pub(crate) trait Poster {
 		self,
 		actions: &mut I,
 	) -> Result<(BoxedPropagator, QueuePreferences), ReformulationError>;
+
+	fn name(&self) -> &'static str;
 }
 
 pub(crate) struct QueuePreferences {