allow always enqueue functional constraints

crates/fzn-huub/src/lib.rs

@@ -87,6 +87,8 @@ pub struct Cli<Stdout, Stderr> {
 	propagator_activity_threshold: f64,
 	/// Enable multiple conflict in checking
 	check_multiple_conflicts: bool,
+	/// Always allow functional constraints to be enqueued.
+	enqueue_functional: bool,
 
 	/// Interval in milliseconds to trace propagator activities
 	trace_propagations: Option<u128>,
@@ -274,6 +276,7 @@ where
 		);
 
 		slv.set_check_multiple_conflicts(self.check_multiple_conflicts);
+		slv.set_enqueue_functional(self.enqueue_functional);
 
 		// Determine Goal and Objective
 		let start_solve = Instant::now();
@@ -524,6 +527,7 @@ where
 			propagator_activity_threshold: self.propagator_activity_threshold,
 			trace_propagations: self.trace_propagations,
 			check_multiple_conflicts: self.check_multiple_conflicts,
+			enqueue_functional: self.enqueue_functional,
 			stdout: self.stdout,
 		}
 	}
@@ -551,6 +555,7 @@ where
 			propagator_activity_threshold: self.propagator_activity_threshold,
 			trace_propagations: self.trace_propagations,
 			check_multiple_conflicts: self.check_multiple_conflicts,
+			enqueue_functional: self.enqueue_functional,
 			stderr: self.stderr,
 			ansi_color: self.ansi_color,
 		}
@@ -622,6 +627,7 @@ impl TryFrom<Arguments> for Cli<io::Stdout, fn() -> io::Stderr> {
 				.opt_value_from_str("--trace-propagations")
 				.map_err(|e| e.to_string())?,
 			check_multiple_conflicts: args.contains("--check-multiple-conflicts"),
+			enqueue_functional: args.contains("--enqueue-functional"),
 
 			verbose,
 			path: args

crates/huub/src/solver.rs

@@ -407,6 +407,7 @@ impl<Oracle: PropagatingSolver<Engine>> Solver<Oracle> {
 			pub fn set_toggle_vsids(&mut self, enable: bool);
 			pub fn set_propagator_activity_factors(&mut self, threshold: f64, additive: f64, multiplicative: f64, trace_propagations: Option<u128>);
 			pub fn set_check_multiple_conflicts(&mut self, enable: bool);
+			pub fn set_enqueue_functional(&mut self, enable: bool);
 		}
 	}
 

crates/huub/src/solver/engine.rs

@@ -636,6 +636,7 @@ impl State {
 			if Some(prop) != skip && !self.enqueued[prop] {
 				if !self.vsids
 					|| self.activity_scores[prop] >= self.config.propagator_activity_threshold
+					|| (self.config.enqueue_functional && self.functional[prop])
 				{
 					self.propagator_queue
 						.insert(self.propagator_priority[prop], prop);
@@ -653,6 +654,7 @@ impl State {
 			if Some(prop) != skip && !self.enqueued[prop] {
 				if !self.vsids
 					|| self.activity_scores[prop] >= self.config.propagator_activity_threshold
+					|| (self.config.enqueue_functional && self.functional[prop])
 				{
 					self.propagator_queue
 						.insert(self.propagator_priority[prop], prop);
@@ -713,6 +715,10 @@ impl State {
 	pub(crate) fn set_check_multiple_conflicts(&mut self, enable: bool) {
 		self.config.check_multiple_conflicts = enable;
 	}
+
+	pub(crate) fn set_enqueue_functional(&mut self, enable: bool) {
+		self.config.enqueue_functional = enable;
+	}
 }
 
 impl ExplanationActions for State {