output propagator tracing logs to stdout

huub-solver · Oct 16, 2024 · e527aad · e527aad
1 parent 27637f1
commit e527aad
Show file tree

Hide file tree

Showing 18 changed files with 278 additions and 84 deletions.
diff --git a/crates/fzn-huub/src/lib.rs b/crates/fzn-huub/src/lib.rs
@@ -86,6 +86,9 @@ pub struct Cli<Stdout, Stderr> {
 	/// Threshold for propagator activation
 	propagator_activity_threshold: f64,
 
+	/// Interval in milliseconds to trace propagator activities
+	trace_propagations: Option<u128>,
+
 	// --- Output configuration ---
 	/// Output stream for (intermediate) solutions and statistics
 	///
@@ -264,6 +267,7 @@ where
 			self.propagator_activity_threshold,
 			self.propagator_additive_factor,
 			self.propagator_multiplicative_factor,
+			self.trace_propagations,
 		);
 
 		// Determine Goal and Objective
@@ -513,6 +517,7 @@ where
 			propagator_additive_factor: self.propagator_additive_factor,
 			propagator_multiplicative_factor: self.propagator_multiplicative_factor,
 			propagator_activity_threshold: self.propagator_activity_threshold,
+			trace_propagations: self.trace_propagations,
 			stdout: self.stdout,
 		}
 	}
@@ -538,6 +543,7 @@ where
 			propagator_additive_factor: self.propagator_additive_factor,
 			propagator_multiplicative_factor: self.propagator_multiplicative_factor,
 			propagator_activity_threshold: self.propagator_activity_threshold,
+			trace_propagations: self.trace_propagations,
 			stderr: self.stderr,
 			ansi_color: self.ansi_color,
 		}
@@ -605,6 +611,9 @@ impl TryFrom<Arguments> for Cli<io::Stdout, fn() -> io::Stderr> {
 				.opt_value_from_fn("--propagator-threshold", parse_float_arg)
 				.map(|x| x.unwrap_or(0.5))
 				.map_err(|e| e.to_string())?,
+			trace_propagations: args
+				.opt_value_from_str("--trace-propagations")
+				.map_err(|e| e.to_string())?,
 
 			verbose,
 			path: args
@@ -614,7 +623,7 @@ impl TryFrom<Arguments> for Cli<io::Stdout, fn() -> io::Stderr> {
 			stdout: io::stdout(),
 			#[expect(trivial_casts, reason = "doesn't compile without the case")]
 			stderr: io::stderr as fn() -> io::Stderr,
-			ansi_color: true,
+			ansi_color: args.contains("--ansi-color"),
 		};
 
 		let remaining = args.finish();

diff --git a/crates/huub/src/model.rs b/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");
 		}

diff --git a/crates/huub/src/model/constraint.rs b/crates/huub/src/model/constraint.rs
@@ -116,7 +116,10 @@ impl Constraint {
 				let y = y.to_arg(slv, map);
 				let idx = idx.to_arg(slv, map);
 				// tranform 1-based index into 0-based index array
-				slv.add_propagator(ArrayVarIntElementBounds::prepare(vars, y, idx + (-1)), functional)?;
+				slv.add_propagator(
+					ArrayVarIntElementBounds::prepare(vars, y, idx + (-1)),
+					functional,
+				)?;
 				Ok(())
 			}
 			Constraint::ArrayVarBoolElement(vars, idx, y) => {
@@ -163,10 +166,10 @@ impl Constraint {
 					})
 					.collect_vec();
 				// Add propagator for lower bound propagation
-				slv.add_propagator(DisjunctiveStrictEdgeFinding::prepare(
-					vars.clone(),
-					durs.clone(),
-				), functional)?;
+				slv.add_propagator(
+					DisjunctiveStrictEdgeFinding::prepare(vars.clone(), durs.clone()),
+					functional,
+				)?;
 
 				// Add symmetric propagator for upper bound propagation
 				let horizon = vars
@@ -179,10 +182,10 @@ impl Constraint {
 					.iter()
 					.zip(durs.iter())
 					.map(|(v, d)| -*v + (horizon - d));
-				slv.add_propagator(DisjunctiveStrictEdgeFinding::prepare(
-					symmetric_vars,
-					durs.clone(),
-				), functional)?;
+				slv.add_propagator(
+					DisjunctiveStrictEdgeFinding::prepare(symmetric_vars, durs.clone()),
+					functional,
+				)?;
 				Ok(())
 			}
 			Constraint::IntAbs(origin, abs) => {
@@ -195,39 +198,47 @@ impl Constraint {
 				let numerator = numerator.to_arg(slv, map);
 				let denominator = denominator.to_arg(slv, map);
 				let result = result.to_arg(slv, map);
-				slv.add_propagator(IntDivBounds::prepare(numerator, denominator, result), functional)?;
+				slv.add_propagator(
+					IntDivBounds::prepare(numerator, denominator, result),
+					functional,
+				)?;
 				Ok(())
 			}
 			Constraint::IntLinEq(vars, c) => {
 				let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect();
 				// coeffs * vars <= c
 				slv.add_propagator(IntLinearLessEqBounds::prepare(vars.clone(), *c), functional)?;
 				// coeffs * vars >= c <=> -coeffs * vars <= -c
-				slv.add_propagator(IntLinearLessEqBounds::prepare(
-					vars.into_iter().map(|v| -v),
-					-c,
-				), functional)?;
+				slv.add_propagator(
+					IntLinearLessEqBounds::prepare(vars.into_iter().map(|v| -v), -c),
+					functional,
+				)?;
 				Ok(())
 			}
 			Constraint::IntLinEqImp(vars, c, r) => {
 				let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect();
 				let r = r.to_arg(slv, map, None)?;
 				match r.0 {
 					BoolViewInner::Const(true) => {
-						slv.add_propagator(IntLinearLessEqBounds::prepare(vars.clone(), *c), functional)?;
-						slv.add_propagator(IntLinearLessEqBounds::prepare(
-							vars.into_iter().map(|v| -v),
-							-c,
-						), functional)?;
+						slv.add_propagator(
+							IntLinearLessEqBounds::prepare(vars.clone(), *c),
+							functional,
+						)?;
+						slv.add_propagator(
+							IntLinearLessEqBounds::prepare(vars.into_iter().map(|v| -v), -c),
+							functional,
+						)?;
 					}
 					BoolViewInner::Const(false) => {}
 					BoolViewInner::Lit(r) => {
-						slv.add_propagator(IntLinearLessEqImpBounds::prepare(vars.clone(), *c, r), functional)?;
-						slv.add_propagator(IntLinearLessEqImpBounds::prepare(
-							vars.into_iter().map(|v| -v),
-							-c,
-							r,
-						), functional)?;
+						slv.add_propagator(
+							IntLinearLessEqImpBounds::prepare(vars.clone(), *c, r),
+							functional,
+						)?;
+						slv.add_propagator(
+							IntLinearLessEqImpBounds::prepare(vars.into_iter().map(|v| -v), -c, r),
+							functional,
+						)?;
 					}
 				}
 				Ok(())
@@ -237,23 +248,31 @@ impl Constraint {
 				let r = r.to_arg(slv, map, None)?;
 				match r.0 {
 					BoolViewInner::Const(true) => {
-						slv.add_propagator(IntLinearLessEqBounds::prepare(vars.clone(), *c), functional)?;
-						slv.add_propagator(IntLinearLessEqBounds::prepare(
-							vars.into_iter().map(|v| -v),
-							-c,
-						), functional)?;
+						slv.add_propagator(
+							IntLinearLessEqBounds::prepare(vars.clone(), *c),
+							functional,
+						)?;
+						slv.add_propagator(
+							IntLinearLessEqBounds::prepare(vars.into_iter().map(|v| -v), -c),
+							functional,
+						)?;
 					}
 					BoolViewInner::Const(false) => {
 						slv.add_propagator(IntLinearNotEqValue::prepare(vars, *c), functional)?;
 					}
 					BoolViewInner::Lit(r) => {
-						slv.add_propagator(IntLinearLessEqImpBounds::prepare(vars.clone(), *c, r), functional)?;
-						slv.add_propagator(IntLinearLessEqImpBounds::prepare(
-							vars.iter().map(|v| -(*v)),
-							-c,
-							r,
-						), functional)?;
-						slv.add_propagator(IntLinearNotEqImpValue::prepare(vars, *c, !r), functional)?;
+						slv.add_propagator(
+							IntLinearLessEqImpBounds::prepare(vars.clone(), *c, r),
+							functional,
+						)?;
+						slv.add_propagator(
+							IntLinearLessEqImpBounds::prepare(vars.iter().map(|v| -(*v)), -c, r),
+							functional,
+						)?;
+						slv.add_propagator(
+							IntLinearNotEqImpValue::prepare(vars, *c, !r),
+							functional,
+						)?;
 					}
 				}
 				Ok(())
@@ -272,7 +291,10 @@ impl Constraint {
 					}
 					BoolViewInner::Const(false) => {}
 					BoolViewInner::Lit(r) => {
-						slv.add_propagator(IntLinearLessEqImpBounds::prepare(vars, *c, r), functional)?;
+						slv.add_propagator(
+							IntLinearLessEqImpBounds::prepare(vars, *c, r),
+							functional,
+						)?;
 					}
 				}
 				Ok(())
@@ -285,18 +307,24 @@ impl Constraint {
 						slv.add_propagator(IntLinearLessEqBounds::prepare(vars, *c), functional)?;
 					}
 					BoolViewInner::Const(false) => {
-						slv.add_propagator(IntLinearLessEqBounds::prepare(
-							vars.into_iter().map(|v| -v),
-							-(c + 1),
-						), functional)?;
+						slv.add_propagator(
+							IntLinearLessEqBounds::prepare(vars.into_iter().map(|v| -v), -(c + 1)),
+							functional,
+						)?;
 					}
 					BoolViewInner::Lit(r) => {
-						slv.add_propagator(IntLinearLessEqImpBounds::prepare(vars.clone(), *c, r), functional)?;
-						slv.add_propagator(IntLinearLessEqImpBounds::prepare(
-							vars.into_iter().map(|v| -v),
-							-(c + 1),
-							!r,
-						), functional)?;
+						slv.add_propagator(
+							IntLinearLessEqImpBounds::prepare(vars.clone(), *c, r),
+							functional,
+						)?;
+						slv.add_propagator(
+							IntLinearLessEqImpBounds::prepare(
+								vars.into_iter().map(|v| -v),
+								-(c + 1),
+								!r,
+							),
+							functional,
+						)?;
 					}
 				}
 				Ok(())
@@ -315,7 +343,10 @@ impl Constraint {
 					}
 					BoolViewInner::Const(false) => {}
 					BoolViewInner::Lit(r) => {
-						slv.add_propagator(IntLinearNotEqImpValue::prepare(vars, *c, r), functional)?;
+						slv.add_propagator(
+							IntLinearNotEqImpValue::prepare(vars, *c, r),
+							functional,
+						)?;
 					}
 				}
 				Ok(())
@@ -328,24 +359,28 @@ impl Constraint {
 						slv.add_propagator(IntLinearNotEqValue::prepare(vars, *c), functional)?;
 					}
 					BoolViewInner::Const(false) => {
-						slv.add_propagator(IntLinearLessEqBounds::prepare(vars.clone(), *c), functional)?;
-						slv.add_propagator(IntLinearLessEqBounds::prepare(
-							vars.into_iter().map(|v| -v),
-							-c,
-						), functional)?;
+						slv.add_propagator(
+							IntLinearLessEqBounds::prepare(vars.clone(), *c),
+							functional,
+						)?;
+						slv.add_propagator(
+							IntLinearLessEqBounds::prepare(vars.into_iter().map(|v| -v), -c),
+							functional,
+						)?;
 					}
 					BoolViewInner::Lit(r) => {
-						slv.add_propagator(IntLinearNotEqImpValue::prepare(vars.clone(), *c, r), functional)?;
-						slv.add_propagator(IntLinearLessEqImpBounds::prepare(
-							vars.clone(),
-							*c,
-							!r,
-						), functional)?;
-						slv.add_propagator(IntLinearLessEqImpBounds::prepare(
-							vars.iter().map(|v| -(*v)),
-							-c,
-							!r,
-						), functional)?;
+						slv.add_propagator(
+							IntLinearNotEqImpValue::prepare(vars.clone(), *c, r),
+							functional,
+						)?;
+						slv.add_propagator(
+							IntLinearLessEqImpBounds::prepare(vars.clone(), *c, !r),
+							functional,
+						)?;
+						slv.add_propagator(
+							IntLinearLessEqImpBounds::prepare(vars.iter().map(|v| -(*v)), -c, !r),
+							functional,
+						)?;
 					}
 				}
 				Ok(())

diff --git a/crates/huub/src/propagator/all_different_int.rs b/crates/huub/src/propagator/all_different_int.rs
@@ -79,6 +79,10 @@ impl Poster for AllDifferentIntValuePoster {
 			},
 		))
 	}
+
+	fn name(&self) -> &'static str {
+		"AllDifferentIntValue"
+	}
 }
 
 #[cfg(test)]

diff --git a/crates/huub/src/propagator/array_int_minimum.rs b/crates/huub/src/propagator/array_int_minimum.rs
@@ -102,6 +102,10 @@ impl Poster for ArrayIntMinimumBoundsPoster {
 			},
 		))
 	}
+
+	fn name(&self) -> &'static str {
+		"ArrayIntMinimumBounds"
+	}
 }
 
 #[cfg(test)]

diff --git a/crates/huub/src/propagator/array_var_int_element.rs b/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)]
@@ -284,8 +288,11 @@ mod tests {
 			EncodingType::Lazy,
 		);
 
-		slv.add_propagator(ArrayVarIntElementBounds::prepare(vec![a, b, c], y, index), false)
-			.unwrap();
+		slv.add_propagator(
+			ArrayVarIntElementBounds::prepare(vec![a, b, c], y, index),
+			false,
+		)
+		.unwrap();
 		slv.expect_solutions(
 			&[index, y, a, b, c],
 			expect![[r#"
@@ -351,8 +358,11 @@ mod tests {
 			EncodingType::Lazy,
 		);
 
-		slv.add_propagator(ArrayVarIntElementBounds::prepare(vec![a, b], y, index), false)
-			.unwrap();
+		slv.add_propagator(
+			ArrayVarIntElementBounds::prepare(vec![a, b], y, index),
+			false,
+		)
+		.unwrap();
 		slv.expect_solutions(
 			&[index, y, a, b],
 			expect![[r#"

diff --git a/crates/huub/src/propagator/disjunctive_strict.rs b/crates/huub/src/propagator/disjunctive_strict.rs
@@ -564,6 +564,10 @@ impl Poster for DisjunctiveEdgeFindingPoster {
 			},
 		))
 	}
+
+	fn name(&self) -> &'static str {
+		"DisjunctiveStrictEdgeFinding"
+	}
 }
 
 #[cfg(test)]

diff --git a/crates/huub/src/propagator/int_abs.rs b/crates/huub/src/propagator/int_abs.rs
@@ -105,6 +105,10 @@ impl Poster for IntAbsBoundsPoster {
 			},
 		))
 	}
+
+	fn name(&self) -> &'static str {
+		"IntAbsBounds"
+	}
 }
 
 #[cfg(test)]
-Original file line number
+Diff line change
@@ Expand Up / @@ -79,6 +79,10 @@ impl Poster for AllDifferentIntValuePoster { @@
     			},
     		))
     	}
+    	fn name(&self) -> &'static str {
+    		"AllDifferentIntValue"
+    	}
     }
     #[cfg(test)]
@@ Expand Down @@