feat: Implement State API

pumpkin-crates/core/Cargo.toml

@@ -27,6 +27,7 @@ num = "0.4.3"
 enum-map = "2.7.3"
 clap = { version = "4.5.40", optional = true }
 indexmap = "2.10.0"
+dyn-clone = "1.0.20"
 flate2 = { version = "1.1.2" }
 
 [target.'cfg(target_arch = "wasm32")'.dependencies]

pumpkin-crates/core/src/api/mod.rs

@@ -118,6 +118,20 @@ pub mod predicates {
     use crate::variables::Literal;
 }
 
+pub mod state {
+    //! Contains structures for the state containing the propagators and variables.
+    //!
+    //! See [`State`] for more information.
+    pub use crate::api::solver::PropagatorHandle;
+    pub use crate::basic_types::PropagatorConflict;
+    pub use crate::engine::Conflict;
+    pub use crate::engine::EmptyDomain;
+    pub use crate::engine::EmptyDomainConflict;
+    pub use crate::engine::State;
+    pub use crate::engine::propagation::CurrentNogood;
+    pub use crate::engine::propagation::PropagatorId;
+}
+
 pub use crate::basic_types::Function;
 
 #[doc(hidden)]

pumpkin-crates/core/src/api/solver.rs

@@ -223,6 +223,7 @@ impl Solver {
     /// let named_literal = solver.new_named_literal("z");
     /// ```
     pub fn new_named_literal(&mut self, name: impl Into<String>) -> Literal {
+        let name = name.into();
         self.satisfaction_solver
             .create_new_literal(Some(name.into()))
     }
@@ -268,6 +269,7 @@ impl Solver {
         upper_bound: i32,
         name: impl Into<String>,
     ) -> DomainId {
+        let name = name.into();
         self.satisfaction_solver.create_new_integer_variable(
             lower_bound,
             upper_bound,
@@ -388,7 +390,7 @@ impl Solver {
             CSPSolverExecutionFlag::Infeasible => {
                 if self
                     .satisfaction_solver
-                    .state
+                    .solver_state
                     .is_infeasible_under_assumptions()
                 {
                     // The state is automatically reset when we return this result
@@ -509,7 +511,7 @@ impl Solver {
 impl Solver {
     /// Creates an instance of the [`DefaultBrancher`].
     pub fn default_brancher(&self) -> DefaultBrancher {
-        DefaultBrancher::default_over_all_variables(&self.satisfaction_solver.assignments)
+        DefaultBrancher::default_over_all_variables(self.satisfaction_solver.assignments())
     }
 }
 

pumpkin-crates/core/src/basic_types/mod.rs

@@ -18,7 +18,7 @@ pub use function::Function;
 pub(crate) use predicate_id_generators::DeletablePredicateIdGenerator;
 pub(crate) use predicate_id_generators::PredicateId;
 pub(crate) use predicate_id_generators::PredicateIdGenerator;
-pub(crate) use propagation_status_cp::*;
+pub use propagation_status_cp::*;
 pub use propositional_conjunction::PropositionalConjunction;
 pub use random::*;
 pub use solution::ProblemSolution;

pumpkin-crates/core/src/basic_types/propagation_status_cp.rs

@@ -1,36 +1,18 @@
 use super::PropositionalConjunction;
-use crate::engine::EmptyDomain;
 use crate::proof::InferenceCode;
+use crate::state::Conflict;
 
 /// The result of invoking a constraint programming propagator. The propagation can either succeed
 /// or identify a conflict. The necessary conditions for the conflict must be captured in the error
 /// variant, i.e. a propositional conjunction.
-pub(crate) type PropagationStatusCP = Result<(), Inconsistency>;
-
-#[derive(Debug, PartialEq, Eq)]
-pub(crate) enum Inconsistency {
-    EmptyDomain,
-    Conflict(PropagatorConflict),
-}
-
-impl From<EmptyDomain> for Inconsistency {
-    fn from(_: EmptyDomain) -> Self {
-        Inconsistency::EmptyDomain
-    }
-}
-
-impl From<PropagatorConflict> for Inconsistency {
-    fn from(conflict: PropagatorConflict) -> Self {
-        Inconsistency::Conflict(conflict)
-    }
-}
+pub(crate) type PropagationStatusCP = Result<(), Conflict>;
 
 /// A conflict stated by a propagator. A propagator that identifies a conflict that is _not_ an
 /// empty domain, describes that conflict with this type.
 #[derive(Clone, Debug, PartialEq, Eq)]
-pub(crate) struct PropagatorConflict {
+pub struct PropagatorConflict {
     /// The conjunction that describes the infeasible partial assignment.
-    pub(crate) conjunction: PropositionalConjunction,
+    pub conjunction: PropositionalConjunction,
     /// The inference code that identified the conflict.
-    pub(crate) inference_code: InferenceCode,
+    pub inference_code: InferenceCode,
 }

pumpkin-crates/core/src/basic_types/propositional_conjunction.rs

@@ -1,3 +1,4 @@
+use std::ops::Deref;
 use std::ops::Index;
 use std::ops::IndexMut;
 
@@ -12,45 +13,29 @@ pub struct PropositionalConjunction {
     predicates_in_conjunction: Vec<Predicate>,
 }
 
+impl Deref for PropositionalConjunction {
+    type Target = [Predicate];
+
+    fn deref(&self) -> &Self::Target {
+        &self.predicates_in_conjunction
+    }
+}
+
 impl PropositionalConjunction {
     pub fn new(predicates_in_conjunction: Vec<Predicate>) -> Self {
         PropositionalConjunction {
             predicates_in_conjunction,
         }
     }
 
-    pub fn len(&self) -> usize {
-        self.predicates_in_conjunction.len()
-    }
-
-    pub fn is_empty(&self) -> bool {
-        self.predicates_in_conjunction.is_empty()
-    }
-
-    pub fn contains(&self, predicate: Predicate) -> bool {
-        self.predicates_in_conjunction.contains(&predicate)
-    }
-
-    pub fn num_predicates(&self) -> u32 {
-        self.predicates_in_conjunction.len() as u32
-    }
-
-    pub fn add(&mut self, predicate: Predicate) {
-        self.predicates_in_conjunction.push(predicate);
-    }
-
-    pub fn iter(&self) -> impl Iterator<Item = &Predicate> + '_ {
-        self.predicates_in_conjunction.iter()
+    pub fn clear(&mut self) {
+        self.predicates_in_conjunction.clear();
     }
 
     pub fn as_slice(&self) -> &[Predicate] {
         self.predicates_in_conjunction.as_slice()
     }
 
-    pub fn clear(&mut self) {
-        self.predicates_in_conjunction.clear();
-    }
-
     pub fn push(&mut self, predicate: Predicate) {
         self.predicates_in_conjunction.push(predicate);
     }

pumpkin-crates/core/src/basic_types/stored_conflict_info.rs

@@ -2,17 +2,16 @@ use super::propagation_status_cp::PropagatorConflict;
 use crate::ConstraintOperationError;
 #[cfg(doc)]
 use crate::engine::ConstraintSatisfactionSolver;
+use crate::engine::EmptyDomainConflict;
 #[cfg(doc)]
 use crate::engine::propagation::Propagator;
-use crate::engine::reason::ReasonRef;
+use crate::engine::state::Conflict;
 use crate::predicates::Predicate;
-use crate::proof::InferenceCode;
-use crate::variables::DomainId;
 
-/// A conflict info which can be stored in the solver.
-/// Two (related) conflicts can happen:
-/// 1) A propagator explicitly detects a conflict.
-/// 2) A propagator post a domain change that results in a variable having an empty domain.
+/// a conflict info which can be stored in the solver.
+/// two (related) conflicts can happen:
+/// 1) a propagator explicitly detects a conflict.
+/// 2) a propagator post a domain change that results in a variable having an empty domain.
 #[derive(Debug, PartialEq, Eq, Clone)]
 pub(crate) enum StoredConflictInfo {
     Propagator(PropagatorConflict),
@@ -24,20 +23,15 @@ pub(crate) enum StoredConflictInfo {
     RootLevelConflict(ConstraintOperationError),
 }
 
-/// A conflict because a domain became empty.
-#[derive(Clone, Copy, Debug, PartialEq, Eq)]
-pub(crate) struct EmptyDomainConflict {
-    /// The predicate that caused a domain to become empty.
-    pub(crate) trigger_predicate: Predicate,
-    /// The reason for [`EmptyDomainConflict::trigger_predicate`] to be true.
-    pub(crate) trigger_reason: ReasonRef,
-    /// The [`InferenceCode`] that accompanies [`EmptyDomainConflict::trigger_reason`].
-    pub(crate) trigger_inference_code: InferenceCode,
-}
-
-impl EmptyDomainConflict {
-    /// The domain that became empty.
-    pub(crate) fn domain(&self) -> DomainId {
-        self.trigger_predicate.get_domain()
+impl From<Conflict> for StoredConflictInfo {
+    fn from(value: Conflict) -> Self {
+        match value {
+            Conflict::Propagator(propagator_conflict) => {
+                StoredConflictInfo::Propagator(propagator_conflict)
+            }
+            Conflict::EmptyDomain(empty_domain_conflict) => {
+                StoredConflictInfo::EmptyDomain(empty_domain_conflict)
+            }
+        }
     }
 }

pumpkin-crates/core/src/basic_types/trail.rs

@@ -6,7 +6,7 @@ use crate::pumpkin_assert_simple;
 
 #[derive(Clone, Debug)]
 pub(crate) struct Trail<T> {
-    current_decision_level: usize,
+    current_checkpoint: usize,
     /// At index i is the position where the i-th decision level ends (exclusive) on the trail
     trail_delimiter: Vec<usize>,
     trail: Vec<T>,
@@ -17,48 +17,48 @@ pub(crate) struct Trail<T> {
 impl<T> Default for Trail<T> {
     fn default() -> Self {
         Trail {
-            current_decision_level: Default::default(),
+            current_checkpoint: Default::default(),
             trail_delimiter: Default::default(),
             trail: Default::default(),
         }
     }
 }
 
 impl<T> Trail<T> {
-    pub(crate) fn increase_decision_level(&mut self) {
-        self.current_decision_level += 1;
+    pub(crate) fn new_checkpoint(&mut self) {
+        self.current_checkpoint += 1;
         self.trail_delimiter.push(self.trail.len());
     }
 
-    pub(crate) fn values_on_decision_level(&self, decision_level: usize) -> &[T] {
-        assert!(decision_level <= self.current_decision_level);
+    pub(crate) fn values_at_checkpoint(&self, checkpoint: usize) -> &[T] {
+        assert!(checkpoint <= self.current_checkpoint);
 
-        let start = if decision_level == 0 {
+        let start = if checkpoint == 0 {
             0
         } else {
-            self.trail_delimiter[decision_level - 1]
+            self.trail_delimiter[checkpoint - 1]
         };
 
-        let end = if decision_level == self.current_decision_level {
+        let end = if checkpoint == self.current_checkpoint {
             self.trail.len()
         } else {
-            self.trail_delimiter[decision_level]
+            self.trail_delimiter[checkpoint]
         };
 
         &self.trail[start..end]
     }
 
-    pub(crate) fn get_decision_level(&self) -> usize {
-        self.current_decision_level
+    pub(crate) fn get_checkpoint(&self) -> usize {
+        self.current_checkpoint
     }
 
-    pub(crate) fn synchronise(&mut self, new_decision_level: usize) -> Rev<Drain<'_, T>> {
-        pumpkin_assert_simple!(new_decision_level < self.current_decision_level);
+    pub(crate) fn synchronise(&mut self, new_checkpoint: usize) -> Rev<Drain<'_, T>> {
+        pumpkin_assert_simple!(new_checkpoint < self.current_checkpoint);
 
-        let new_trail_len = self.trail_delimiter[new_decision_level];
+        let new_trail_len = self.trail_delimiter[new_checkpoint];
 
-        self.current_decision_level = new_decision_level;
-        self.trail_delimiter.truncate(new_decision_level);
+        self.current_checkpoint = new_checkpoint;
+        self.trail_delimiter.truncate(new_checkpoint);
         self.trail.drain(new_trail_len..).rev()
     }
 
@@ -100,10 +100,10 @@ mod tests {
     }
 
     #[test]
-    fn backtracking_removes_elements_beyond_decision_level() {
+    fn backtracking_removes_elements_beyond_checkpoint() {
         let mut trail = Trail::default();
 
-        trail.increase_decision_level();
+        trail.new_checkpoint();
         trail.push(1);
         let _ = trail.synchronise(0);
 
@@ -115,11 +115,11 @@ mod tests {
         let mut trail = Trail::default();
         trail.push(1);
 
-        trail.increase_decision_level();
+        trail.new_checkpoint();
         trail.push(2);
-        trail.increase_decision_level();
+        trail.new_checkpoint();
         trail.push(3);
-        trail.increase_decision_level();
+        trail.new_checkpoint();
         trail.push(4);
 
         let _ = trail.synchronise(1);
@@ -132,31 +132,31 @@ mod tests {
         let mut trail = Trail::default();
         trail.push(1);
 
-        trail.increase_decision_level();
+        trail.new_checkpoint();
         trail.push(2);
-        trail.increase_decision_level();
+        trail.new_checkpoint();
         trail.push(3);
-        trail.increase_decision_level();
+        trail.new_checkpoint();
         trail.push(4);
 
         let popped = trail.synchronise(0).collect::<Vec<_>>();
         assert_eq!(vec![4, 3, 2], popped);
     }
 
     #[test]
-    fn elements_at_current_decision_level() {
+    fn elements_at_current_checkpoint() {
         let mut trail = Trail::default();
         trail.push(1);
         trail.push(2);
 
-        trail.increase_decision_level();
+        trail.new_checkpoint();
         trail.push(3);
-        trail.increase_decision_level();
+        trail.new_checkpoint();
         trail.push(4);
         trail.push(5);
 
-        assert_eq!(&[1, 2], trail.values_on_decision_level(0));
-        assert_eq!(&[3], trail.values_on_decision_level(1));
-        assert_eq!(&[4, 5], trail.values_on_decision_level(2));
+        assert_eq!(&[1, 2], trail.values_at_checkpoint(0));
+        assert_eq!(&[3], trail.values_at_checkpoint(1));
+        assert_eq!(&[4, 5], trail.values_at_checkpoint(2));
     }
 }