refactor(pumpkin-solver): Bulk create propagators before root propagation in FlatZinc reader#407
Closed
maartenflippo wants to merge 14 commits intomainfrom
Closed
refactor(pumpkin-solver): Bulk create propagators before root propagation in FlatZinc reader#407maartenflippo wants to merge 14 commits intomainfrom
maartenflippo wants to merge 14 commits intomainfrom
Conversation
ImkoMarijnissen
requested changes
Apr 9, 2026
Contributor
ImkoMarijnissen
left a comment
ImkoMarijnissen
left a comment
There was a problem hiding this comment.
My main gripe is that we now need to pass the nogood propagator when creating all of these constraints.
However, I do not see an easy way out of this.
Comment on lines
-144
to
-178
|
|
||
| #[cfg(test)] | ||
| mod tests { | ||
| use super::*; | ||
|
|
||
| #[test] | ||
| fn less_than_conflict() { | ||
| let mut solver = Solver::default(); | ||
|
|
||
| let constraint_tag = solver.new_constraint_tag(); | ||
| let x = solver.new_named_bounded_integer(0, 0, "x"); | ||
|
|
||
| let result = less_than([x], 0, constraint_tag).post(&mut solver); | ||
| assert_eq!( | ||
| result, | ||
| Err(ConstraintOperationError::InfeasiblePropagator), | ||
| "Expected {result:?} to be an `InfeasiblePropagator` error" | ||
| ); | ||
| } | ||
|
|
||
| #[test] | ||
| fn greater_than_conflict() { | ||
| let mut solver = Solver::default(); | ||
|
|
||
| let constraint_tag = solver.new_constraint_tag(); | ||
| let x = solver.new_named_bounded_integer(0, 0, "x"); | ||
|
|
||
| let result = greater_than([x], 0, constraint_tag).post(&mut solver); | ||
| assert_eq!( | ||
| result, | ||
| Err(ConstraintOperationError::InfeasiblePropagator), | ||
| "Expected {result:?} to be an `InfeasiblePropagator` error" | ||
| ); | ||
| } | ||
| } |
Contributor
There was a problem hiding this comment.
These should not be removed
| literals: impl Into<Vec<Literal>>, | ||
| literals: impl IntoIterator<Item = Predicate>, | ||
| constraint_tag: ConstraintTag, | ||
| propagator_handle: PropagatorHandle<NogoodPropagator>, |
Contributor
There was a problem hiding this comment.
Requires documentation; I would not find it clear why this is necessary as a user, or how to get this information
Comment on lines
+16
to
+25
| #[derive(Clone, Copy, Debug, PartialEq, Eq)] | ||
| pub enum EqualityConsistency { | ||
| /// Use bound consistent propagation. | ||
| Bound, | ||
| /// If the constraint is over two variables, use domain consistent propagation. | ||
| /// | ||
| /// This is only useful when variables are actually equal. In the future this will likely | ||
| /// become a preprocessing step to unify the variables. | ||
| Domain, | ||
| } |
Contributor
There was a problem hiding this comment.
I think that it would be better to create a separate binary_equals constraint for this behaviour, no? Now it is a lot of passing around in places where it does not make sense
Comment on lines
-565
to
-572
| /// Default brancher implementation | ||
| impl Solver { | ||
| /// Creates an instance of the [`DefaultBrancher`]. | ||
| pub fn default_brancher(&self) -> DefaultBrancher { | ||
| DefaultBrancher::default_over_all_variables(self.satisfaction_solver.assignments()) | ||
| } | ||
| } | ||
|
|
Comment on lines
+531
to
+540
| pub fn add_nogood( | ||
| &mut self, | ||
| nogood: Vec<Predicate>, | ||
| inference_code: InferenceCode, | ||
| context: &mut PropagationContext, | ||
| ) -> PropagationStatusCP { | ||
| self.add_permanent_nogood(nogood, inference_code, context) | ||
| nogood: impl IntoIterator<Item = Predicate>, | ||
| constraint_tag: ConstraintTag, | ||
| ) { | ||
| let nogood = nogood.into_iter().collect::<Vec<_>>(); | ||
|
|
||
| assert!(!nogood.is_empty(), "cannot add empty nogoods"); | ||
|
|
||
| self.newly_added_nogoods.push((constraint_tag, nogood)); |
Contributor
There was a problem hiding this comment.
Wouldn't this lead to issues with enqueuing?
Now you add a nogood but you do not register anything. It would be possible for every predicate in that nogood to become true (i.e., a conflict to occur) without the propagator being notified, no?
Contributor
Author
|
The interface we end up with is not ergonomic, so we'll close this in favor of more discovery |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
We change when we run root-level propagation. Previously, we ran propagation after every individual constraint was added. This is slightly slower than running all propagation at once, but more importantly, running the root-propagation once makes debugging a lot simpler :).
This PR encompasses the following change:
Constraint::postfunction takes aStateinstead of aSolverConstraint::postfunction does not return aResultanymore, since it cannot detect aConstraintOperationError.equalscan use domain propagation is now an argument of the various constraint functions, since it does not have access to whether the solver is proof logging or notconjunctionandclauseconstraintsSolver::from_stateto construct the solver from a preconfiguredState.Note that
Solver::add_constraintstill exists.Aside from these changes, there are various test cleanups to now use
Statedirectly, rather than constructAssignments,NotificationEngine, etc.