feat: Impement State API #319
Open
Conversation
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
maartenflippo
previously requested changes
Nov 19, 2025
Comment on lines
17
to
25
| impl From<Conflict> for Inconsistency { | ||
| fn from(value: Conflict) -> Self { | ||
| match value { | ||
| Conflict::Propagator(propagator_conflict) => { | ||
| Inconsistency::Conflict(propagator_conflict) | ||
| } | ||
| Conflict::EmptyDomain(_) => Inconsistency::EmptyDomain, | ||
| } | ||
| } |
Contributor
There was a problem hiding this comment.
Where is this necessary? It seems counterintuitive as Inconsistency is more toward the core than Conflict .
| /// A conflict because a domain became empty. | ||
| #[derive(Clone, Copy, Debug, PartialEq, Eq)] | ||
| pub(crate) struct EmptyDomainConflict { | ||
| pub struct EmptyDomainConflict { |
Contributor
There was a problem hiding this comment.
We can move this alongside the defintion of Conflict
Comment on lines
49
to
52
| #[cfg(test)] | ||
| pub(crate) fn next_key(&self) -> Key { | ||
| Key::create_from_index(self.len()) | ||
| } |
Contributor
Author
There was a problem hiding this comment.
Change in test solver to generate a new key
Comment on lines
101
to
126
| pub(crate) fn new() -> Self { | ||
| let mut result = Self { | ||
| assignments: Default::default(), | ||
| trailed_values: TrailedValues::default(), | ||
| variable_names: VariableNames::default(), | ||
| propagator_queue: PropagatorQueue::default(), | ||
| propagators: PropagatorStore::default(), | ||
| reason_store: ReasonStore::default(), | ||
| notification_engine: NotificationEngine::default(), | ||
| inference_codes: None, | ||
| statistics: StateStatistics::default(), | ||
| }; | ||
| // As a convention, the assignments contain a dummy domain_id=0, which represents a 0-1 | ||
| // variable that is assigned to one. We use it to represent predicates that are | ||
| // trivially true. We need to adjust other data structures to take this into account. | ||
| let dummy_id = Predicate::trivially_true().get_domain(); | ||
|
|
||
| result | ||
| .variable_names | ||
| .add_integer(dummy_id, "Dummy".to_owned()); | ||
| assert!(dummy_id.id() == 0); | ||
| assert!(result.assignments.get_lower_bound(dummy_id) == 1); | ||
| assert!(result.assignments.get_upper_bound(dummy_id) == 1); | ||
|
|
||
| result | ||
| } |
Contributor
There was a problem hiding this comment.
This should probably be a Default::default() implementation
| /// Component responsible for providing notifications for changes to the domains of variables | ||
| /// and/or the polarity [Predicate]s | ||
| pub(crate) notification_engine: NotificationEngine, | ||
| pub(crate) inference_codes: Option<KeyedVec<InferenceCode, (ConstraintTag, Arc<str>)>>, |
Contributor
There was a problem hiding this comment.
No need for this to be an Option
| /// let mut state = State::default(); | ||
| /// let variable = state.new_interval_variable(1, 10, Some("x1".to_string())); | ||
| /// | ||
| /// state.new_checkpoint(); |
Contributor
There was a problem hiding this comment.
Let's clarify the interaction with get_decision_level() and add an assert that the DL equals 1.
Comment on lines
530
to
545
| /// This method should only be called when an empty domain is encountered during propagation. | ||
| /// It removes the final trail element and returns the [`Conflict`]. | ||
| pub(crate) fn prepare_for_conflict_resolution(&mut self) -> Conflict { | ||
| // TODO: As a temporary solution, we remove the last trail element. | ||
| // This way we guarantee that the assignment is consistent, which is needed | ||
| // for the conflict analysis data structures. The proper alternative would | ||
| // be to forbid the assignments from getting into an inconsistent state. | ||
| let (trigger_predicate, trigger_reason, trigger_inference_code) = | ||
| self.assignments.remove_last_trail_element(); | ||
|
|
||
| Conflict::EmptyDomain(EmptyDomainConflict { | ||
| trigger_predicate, | ||
| trigger_reason, | ||
| trigger_inference_code, | ||
| }) | ||
| } |
Contributor
There was a problem hiding this comment.
Does this need to be pub(crate)? It seems like we are leaking implementation details unnecessarily.
Contributor
Author
There was a problem hiding this comment.
Do the prepare_for_confict when posting predicates in PropagationContextMut
Comment on lines
547
to
629
| /// Performs a single call to [`Propagator::propagate`] for the propagator with the provided | ||
| /// [`PropagatorId`]. | ||
| /// | ||
| /// Other propagators could be enqueued as a result of the changes made by the propagated | ||
| /// propagator but a call to [`State::fixed_point_propagate`] is | ||
| /// required for further propagation to occur. | ||
| /// | ||
| /// It could be that the current [`State`] implies a conflict by propagation. In that case, an | ||
| /// [`Err`] with [`Conflict`] is returned. | ||
| /// | ||
| /// Once the [`State`] is conflicting, then the only operation that is defined is | ||
| /// [`State::restore_to`]. All other operations and queries on the state are undetermined. | ||
| pub(crate) fn propagate(&mut self, propagator_id: PropagatorId) -> Result<(), Conflict> { | ||
| self.statistics.num_propagators_called += 1; | ||
|
|
||
| let num_trail_entries_before = self.assignments.num_trail_entries(); | ||
|
|
||
| let propagation_status = { | ||
| let propagator = &mut self.propagators[propagator_id]; | ||
| let context = PropagationContextMut::new( | ||
| &mut self.trailed_values, | ||
| &mut self.assignments, | ||
| &mut self.reason_store, | ||
| &mut self.notification_engine, | ||
| propagator_id, | ||
| ); | ||
| propagator.propagate(context) | ||
| }; | ||
|
|
||
| match propagation_status { | ||
| Ok(_) => { | ||
| // Notify other propagators of the propagations and continue. | ||
| self.notification_engine | ||
| .notify_propagators_about_domain_events( | ||
| &mut self.assignments, | ||
| &mut self.trailed_values, | ||
| &mut self.propagators, | ||
| PropagatorHandle { | ||
| id: PropagatorId(0), | ||
| propagator: std::marker::PhantomData, | ||
| }, | ||
| &mut self.propagator_queue, | ||
| ); | ||
| } | ||
| Err(inconsistency) => { | ||
| self.statistics.num_conflicts += 1; | ||
| match inconsistency { | ||
| // A propagator did a change that resulted in an empty domain. | ||
| Inconsistency::EmptyDomain => { | ||
| let info = self.prepare_for_conflict_resolution(); | ||
| return Err(info); | ||
| } | ||
| // A propagator-specific reason for the current conflict. | ||
| Inconsistency::Conflict(conflict) => { | ||
| pumpkin_assert_advanced!(DebugHelper::debug_reported_failure( | ||
| &self.trailed_values, | ||
| &self.assignments, | ||
| &conflict.conjunction, | ||
| &self.propagators[propagator_id], | ||
| propagator_id, | ||
| &self.notification_engine | ||
| )); | ||
|
|
||
| let stored_conflict_info = Conflict::Propagator(conflict); | ||
| return Err(stored_conflict_info); | ||
| } | ||
| } | ||
| } | ||
| } | ||
| pumpkin_assert_extreme!( | ||
| DebugHelper::debug_check_propagations( | ||
| num_trail_entries_before, | ||
| propagator_id, | ||
| &self.trailed_values, | ||
| &self.assignments, | ||
| &mut self.reason_store, | ||
| &mut self.propagators, | ||
| &self.notification_engine | ||
| ), | ||
| "Checking the propagations performed by the propagator led to inconsistencies!" | ||
| ); | ||
| Ok(()) | ||
| } |
Contributor
There was a problem hiding this comment.
Didn't we discuss this was unnecessary?
Contributor
Author
There was a problem hiding this comment.
Can indeed be private
Comment on lines
718
to
722
| pub fn get_propagation_reason( | ||
| &mut self, | ||
| predicate: Predicate, | ||
| reason_buffer: &mut (impl Extend<Predicate> + AsRef<[Predicate]>), | ||
| ) { |
Contributor
There was a problem hiding this comment.
This should return the inference code if the explanation comes from a propagator. Otherwise proof logging cannot easily extract that information.
Contributor
Author
There was a problem hiding this comment.
Return Option of inference code when it is on the trail; use the get reason method in State in conflict analysis context
Contributor
Author
There was a problem hiding this comment.
I now return the trail position; one problem is that the ExplanationContext takes as input a CurrentNogood, I have now added this to the interface
Comment on lines
22
to
23
| pub(crate) id: PropagatorId, | ||
| pub(crate) propagator: PhantomData<P>, |
Contributor
There was a problem hiding this comment.
Shouldn't be public at all
…t return to a consistent state
github-actions
bot
dismissed
maartenflippo’s stale review
Review re-requested
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
In our efforts to modularise the solver, this PR implements the extraction of
Statefrom the solver. This structure contains the variables and the propagators (in addition to the notification engine, and the propagation queue).TODO