feat: stateful integer

pumpkin-solver/src/basic_types/solution.rs

@@ -1,4 +1,4 @@
-use crate::engine::propagation::propagation_context::HasAssignments;
+use crate::engine::propagation::contexts::HasAssignments;
 use crate::engine::variables::DomainGeneratorIterator;
 use crate::engine::variables::DomainId;
 use crate::engine::variables::Literal;

pumpkin-solver/src/engine/conflict_analysis/conflict_analysis_context.rs

@@ -18,6 +18,7 @@ use crate::engine::Assignments;
 use crate::engine::ConstraintSatisfactionSolver;
 use crate::engine::IntDomainEvent;
 use crate::engine::PropagatorQueue;
+use crate::engine::StatefulAssignments;
 use crate::engine::WatchListCP;
 use crate::predicate;
 use crate::proof::ProofLog;
@@ -48,6 +49,7 @@ pub(crate) struct ConflictAnalysisContext<'a> {
 
     pub(crate) is_completing_proof: bool,
     pub(crate) unit_nogood_step_ids: &'a HashMap<Predicate, StepId>,
+    pub(crate) stateful_assignments: &'a mut StatefulAssignments,
 }
 
 impl Debug for ConflictAnalysisContext<'_> {
@@ -82,6 +84,7 @@ impl<'a> ConflictAnalysisContext<'a> {
             self.backtrack_event_drain,
             backtrack_level,
             self.brancher,
+            self.stateful_assignments,
         )
     }
 

pumpkin-solver/src/engine/constraint_satisfaction_solver.rs

@@ -16,13 +16,15 @@ use super::conflict_analysis::LearnedNogood;
 use super::conflict_analysis::NoLearningResolver;
 use super::conflict_analysis::SemanticMinimiser;
 use super::nogoods::Lbd;
+use super::propagation::contexts::StatefulPropagationContext;
 use super::propagation::store::PropagatorStore;
 use super::propagation::PropagatorId;
 use super::solver_statistics::SolverStatistics;
 use super::termination::TerminationCondition;
 use super::variables::IntegerVariable;
 use super::variables::Literal;
 use super::ResolutionResolver;
+use super::StatefulAssignments;
 use crate::basic_types::moving_averages::MovingAverage;
 use crate::basic_types::CSPSolverExecutionFlag;
 use crate::basic_types::ConstraintOperationError;
@@ -142,6 +144,8 @@ pub struct ConstraintSatisfactionSolver {
     unit_nogood_step_ids: HashMap<Predicate, StepId>,
     /// The resolver which is used upon a conflict.
     conflict_resolver: Box<dyn Resolver>,
+
+    pub(crate) stateful_assignments: StatefulAssignments,
 }
 
 impl Default for ConstraintSatisfactionSolver {
@@ -250,6 +254,7 @@ impl ConstraintSatisfactionSolver {
         propagators: &mut PropagatorStore,
         propagator_queue: &mut PropagatorQueue,
         assignments: &mut Assignments,
+        stateful_assignments: &mut StatefulAssignments,
     ) {
         pumpkin_assert_moderate!(
             propagators[Self::get_nogood_propagator_id()].name() == "NogoodPropagator"
@@ -266,6 +271,7 @@ impl ConstraintSatisfactionSolver {
             propagators,
             propagator_queue,
             assignments,
+            stateful_assignments,
         );
     }
 
@@ -276,8 +282,9 @@ impl ConstraintSatisfactionSolver {
         propagators: &mut PropagatorStore,
         propagator_queue: &mut PropagatorQueue,
         assignments: &mut Assignments,
+        stateful_assignments: &mut StatefulAssignments,
     ) {
-        let context = PropagationContext::new(assignments);
+        let context = StatefulPropagationContext::new(stateful_assignments, assignments);
 
         let enqueue_decision = propagators[propagator_id].notify(context, local_id, event.into());
 
@@ -306,6 +313,7 @@ impl ConstraintSatisfactionSolver {
                 &mut self.propagators,
                 &mut self.propagator_queue,
                 &mut self.assignments,
+                &mut self.stateful_assignments,
             );
             // Now notify other propagators subscribed to this event.
             for propagator_var in self.watch_list_cp.get_affected_propagators(event, domain) {
@@ -318,6 +326,7 @@ impl ConstraintSatisfactionSolver {
                     &mut self.propagators,
                     &mut self.propagator_queue,
                     &mut self.assignments,
+                    &mut self.stateful_assignments,
                 );
             }
         }
@@ -371,6 +380,7 @@ impl ConstraintSatisfactionSolver {
             proof_log: &mut self.internal_parameters.proof_log,
             is_completing_proof: true,
             unit_nogood_step_ids: &self.unit_nogood_step_ids,
+            stateful_assignments: &mut self.stateful_assignments,
         };
 
         let result = self
@@ -410,6 +420,7 @@ impl ConstraintSatisfactionSolver {
                 ConflictResolver::UIP => Box::new(ResolutionResolver::default()),
             },
             internal_parameters: solver_options,
+            stateful_assignments: StatefulAssignments::default(),
         };
 
         // As a convention, the assignments contain a dummy domain_id=0, which represents a 0-1
@@ -654,6 +665,7 @@ impl ConstraintSatisfactionSolver {
                     proof_log: &mut self.internal_parameters.proof_log,
                     is_completing_proof: false,
                     unit_nogood_step_ids: &self.unit_nogood_step_ids,
+                    stateful_assignments: &mut self.stateful_assignments,
                 };
 
                 let mut resolver = ResolutionResolver::with_mode(AnalysisMode::AllDecision);
@@ -724,6 +736,7 @@ impl ConstraintSatisfactionSolver {
                 &mut self.backtrack_event_drain,
                 0,
                 brancher,
+                &mut self.stateful_assignments,
             );
             self.state.declare_ready();
         }
@@ -860,6 +873,7 @@ impl ConstraintSatisfactionSolver {
 
     pub(crate) fn declare_new_decision_level(&mut self) {
         self.assignments.increase_decision_level();
+        self.stateful_assignments.increase_decision_level();
         self.reason_store.increase_decision_level();
     }
 
@@ -895,6 +909,7 @@ impl ConstraintSatisfactionSolver {
             proof_log: &mut self.internal_parameters.proof_log,
             is_completing_proof: false,
             unit_nogood_step_ids: &self.unit_nogood_step_ids,
+            stateful_assignments: &mut self.stateful_assignments,
         };
 
         let learned_nogood = self
@@ -963,6 +978,7 @@ impl ConstraintSatisfactionSolver {
 
     fn add_learned_nogood(&mut self, learned_nogood: LearnedNogood) {
         let mut context = PropagationContextMut::new(
+            &mut self.stateful_assignments,
             &mut self.assignments,
             &mut self.reason_store,
             &mut self.semantic_minimiser,
@@ -1030,6 +1046,7 @@ impl ConstraintSatisfactionSolver {
             &mut self.backtrack_event_drain,
             0,
             brancher,
+            &mut self.stateful_assignments,
         );
 
         self.restart_strategy.notify_restart();
@@ -1050,6 +1067,7 @@ impl ConstraintSatisfactionSolver {
         backtrack_event_drain: &mut Vec<(IntDomainEvent, DomainId)>,
         backtrack_level: usize,
         brancher: &mut BrancherType,
+        stateful_assignments: &mut StatefulAssignments,
     ) {
         pumpkin_assert_simple!(backtrack_level < assignments.get_decision_level());
 
@@ -1065,6 +1083,9 @@ impl ConstraintSatisfactionSolver {
             .for_each(|(domain_id, previous_value)| {
                 brancher.on_unassign_integer(*domain_id, *previous_value)
             });
+
+        stateful_assignments.synchronise(backtrack_level);
+
         *last_notified_cp_trail_index = assignments.num_trail_entries();
 
         reason_store.synchronise(backtrack_level);
@@ -1146,6 +1167,7 @@ impl ConstraintSatisfactionSolver {
             let propagation_status = {
                 let propagator = &mut self.propagators[propagator_id];
                 let context = PropagationContextMut::new(
+                    &mut self.stateful_assignments,
                     &mut self.assignments,
                     &mut self.reason_store,
                     &mut self.semantic_minimiser,
@@ -1188,6 +1210,7 @@ impl ConstraintSatisfactionSolver {
                     // A propagator-specific reason for the current conflict.
                     Inconsistency::Conflict(conflict_nogood) => {
                         pumpkin_assert_advanced!(DebugHelper::debug_reported_failure(
+                            &self.stateful_assignments,
                             &self.assignments,
                             &conflict_nogood,
                             &self.propagators[propagator_id],
@@ -1207,6 +1230,7 @@ impl ConstraintSatisfactionSolver {
                 DebugHelper::debug_check_propagations(
                     num_trail_entries_before,
                     propagator_id,
+                    &self.stateful_assignments,
                     &self.assignments,
                     &mut self.reason_store,
                     &mut self.propagators
@@ -1223,7 +1247,11 @@ impl ConstraintSatisfactionSolver {
         // since otherwise the state may be inconsistent.
         pumpkin_assert_extreme!(
             self.state.is_conflicting()
-                || DebugHelper::debug_fixed_point_propagation(&self.assignments, &self.propagators,)
+                || DebugHelper::debug_fixed_point_propagation(
+                    &self.stateful_assignments,
+                    &self.assignments,
+                    &self.propagators,
+                )
         );
     }
 
@@ -1349,8 +1377,9 @@ impl ConstraintSatisfactionSolver {
 
         let mut initialisation_context = PropagatorInitialisationContext::new(
             &mut self.watch_list_cp,
+            &mut self.stateful_assignments,
             new_propagator_id,
-            &self.assignments,
+            &mut self.assignments,
         );
 
         let initialisation_status = new_propagator.initialise_at_root(&mut initialisation_context);
@@ -1398,6 +1427,7 @@ impl ConstraintSatisfactionSolver {
 
     pub fn add_nogood(&mut self, nogood: Vec<Predicate>) -> Result<(), ConstraintOperationError> {
         let mut propagation_context = PropagationContextMut::new(
+            &mut self.stateful_assignments,
             &mut self.assignments,
             &mut self.reason_store,
             &mut self.semantic_minimiser,

pumpkin-solver/src/engine/cp/assignments.rs

@@ -734,23 +734,17 @@ impl Assignments {
                 }
             }
         });
+
         // Drain does not remove the events from the internal data structure. Elements are removed
         // lazily, as the iterator gets executed. For this reason we go through the entire iterator.
         let iter = self.events.drain();
         let _ = iter.count();
-        // println!("ASSIGN AFTER SYNC PRESENT: {:?}", self.events.present);
-        // println!("others: {:?}", self.events.events);
         unfixed_variables
     }
 
     /// todo: This is a temporary hack, not to be used in general.
     pub(crate) fn remove_last_trail_element(&mut self) {
         let entry = self.trail.pop().unwrap();
-        // println!(
-        // "\tHacky remova: {} {}",
-        // entry.predicate,
-        // entry.reason.is_none()
-        // );
         let domain_id = entry.predicate.get_domain();
         self.domains[domain_id].undo_trail_entry(&entry);
     }

pumpkin-solver/src/engine/cp/mod.rs

@@ -5,13 +5,15 @@ pub(crate) mod opaque_domain_event;
 pub(crate) mod propagation;
 mod propagator_queue;
 pub(crate) mod reason;
+mod stateful;
 pub(crate) mod test_solver;
 mod watch_list_cp;
 
 pub(crate) use assignments::Assignments;
 pub(crate) use assignments::EmptyDomain;
 pub(crate) use event_sink::*;
 pub(crate) use propagator_queue::PropagatorQueue;
+pub(crate) use stateful::*;
 pub(crate) use watch_list_cp::IntDomainEvent;
 pub(crate) use watch_list_cp::WatchListCP;
 pub(crate) use watch_list_cp::Watchers;
@@ -26,17 +28,20 @@ mod tests {
     use crate::engine::propagation::PropagationContextMut;
     use crate::engine::propagation::PropagatorId;
     use crate::engine::reason::ReasonStore;
+    use crate::engine::StatefulAssignments;
 
     #[test]
     fn test_no_update_reason_store_if_no_update_lower_bound() {
         let mut assignments = Assignments::default();
+        let mut stateful_assignments = StatefulAssignments::default();
         let domain = assignments.grow(5, 10);
 
         let mut reason_store = ReasonStore::default();
         assert_eq!(reason_store.len(), 0);
         {
             let mut semantic_miniser = SemanticMinimiser::default();
             let mut context = PropagationContextMut::new(
+                &mut stateful_assignments,
                 &mut assignments,
                 &mut reason_store,
                 &mut semantic_miniser,
@@ -52,6 +57,7 @@ mod tests {
     #[test]
     fn test_no_update_reason_store_if_no_update_upper_bound() {
         let mut assignments = Assignments::default();
+        let mut stateful_assignments = StatefulAssignments::default();
         let domain = assignments.grow(5, 10);
 
         let mut reason_store = ReasonStore::default();
@@ -60,6 +66,7 @@ mod tests {
         {
             let mut semantic_miniser = SemanticMinimiser::default();
             let mut context = PropagationContextMut::new(
+                &mut stateful_assignments,
                 &mut assignments,
                 &mut reason_store,
                 &mut semantic_miniser,
@@ -75,6 +82,7 @@ mod tests {
     #[test]
     fn test_no_update_reason_store_if_no_update_remove() {
         let mut assignments = Assignments::default();
+        let mut stateful_assignments = StatefulAssignments::default();
         let domain = assignments.grow(5, 10);
 
         let mut reason_store = ReasonStore::default();
@@ -83,6 +91,7 @@ mod tests {
         {
             let mut semantic_miniser = SemanticMinimiser::default();
             let mut context = PropagationContextMut::new(
+                &mut stateful_assignments,
                 &mut assignments,
                 &mut reason_store,
                 &mut semantic_miniser,

pumpkin-solver/src/engine/cp/propagation/contexts/mod.rs

@@ -0,0 +1,5 @@
+pub(crate) mod explanation_context;
+pub(crate) mod propagation_context;
+pub(crate) mod propagator_initialisation_context;
+
+pub(crate) use propagation_context::*;