feat(pumpkin-solver-py): Add incrementality to python interface

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

@@ -211,6 +211,19 @@ impl Solver {
             .create_new_literal_for_predicate(predicate, None, constraint_tag)
     }
 
+    pub fn new_named_literal_for_predicate(
+        &mut self,
+        predicate: Predicate,
+        constraint_tag: ConstraintTag,
+        name: impl Into<String>,
+    ) -> Literal {
+        self.satisfaction_solver.create_new_literal_for_predicate(
+            predicate,
+            Some(name.into().into()),
+            constraint_tag,
+        )
+    }
+
     /// Create a fresh propositional variable with a given name and return the literal with positive
     /// polarity.
     ///

pumpkin-crates/core/src/branching/branchers/autonomous_search.rs

@@ -136,6 +136,10 @@ impl DefaultBrancher {
             statistics: Default::default(),
         }
     }
+
+    pub fn add_domain(&mut self, domain: DomainId) {
+        self.backup_brancher.variable_selector.add_domain(domain);
+    }
 }
 
 impl<BackupSelector> AutonomousSearch<BackupSelector> {

pumpkin-crates/core/src/branching/variable_selection/random.rs

@@ -20,6 +20,11 @@ impl RandomSelector {
             }),
         }
     }
+
+    /// Add a domain to consideration in the variable selection.
+    pub fn add_domain(&mut self, domain: DomainId) {
+        self.variables.insert(domain);
+    }
 }
 
 impl VariableSelector<DomainId> for RandomSelector {

pumpkin-solver-py/examples/nqueens.py

@@ -1,25 +1,27 @@
 from argparse import ArgumentParser
 from pathlib import Path
 
-from pumpkin_solver_py import constraints, SatisfactionResult, Model
+from pumpkin_solver import constraints, SatisfactionResult, Model
 
 
 def main(n: int, proof: Path | None):
     assert n > 0, "Please provide a positive non-zero 'n'"
 
-    model = Model()
+    model = Model(proof=proof)
 
     variables = [model.new_integer_variable(0, n - 1, name=f"q{i}") for i in range(n)]
 
-    model.add_constraint(constraints.AllDifferent(variables), tag=1)
+    model.add_constraint(
+        constraints.AllDifferent(variables, model.new_constraint_tag())
+    )
 
     diag1 = [var.offset(i) for (i, var) in enumerate(variables)]
     diag2 = [var.offset(-i) for (i, var) in enumerate(variables)]
 
-    model.add_constraint(constraints.AllDifferent(diag1), tag=2)
-    model.add_constraint(constraints.AllDifferent(diag2), tag=3)
+    model.add_constraint(constraints.AllDifferent(diag1, model.new_constraint_tag()))
+    model.add_constraint(constraints.AllDifferent(diag2, model.new_constraint_tag()))
 
-    status = model.satisfy(proof=proof)
+    status = model.satisfy()
     match status:
         case SatisfactionResult.Satisfiable(solution):
             row_separator = "+---" * n + "+"

pumpkin-solver-py/src/constraints/arguments.rs

@@ -4,45 +4,44 @@ use pumpkin_solver::variables::Literal;
 
 use crate::variables::BoolExpression;
 use crate::variables::IntExpression;
-use crate::variables::VariableMap;
 
 /// Trait which helps to convert Python API types to the solver types when creating constraints.
 pub trait PythonConstraintArg {
     type Output;
 
-    fn to_solver_constraint_argument(self, variable_map: &VariableMap) -> Self::Output;
+    fn to_solver_constraint_argument(self) -> Self::Output;
 }
 
 impl PythonConstraintArg for IntExpression {
     type Output = AffineView<DomainId>;
 
-    fn to_solver_constraint_argument(self, variable_map: &VariableMap) -> Self::Output {
-        self.to_affine_view(variable_map)
+    fn to_solver_constraint_argument(self) -> Self::Output {
+        self.0
     }
 }
 
 impl PythonConstraintArg for BoolExpression {
     type Output = Literal;
 
-    fn to_solver_constraint_argument(self, variable_map: &VariableMap) -> Self::Output {
-        self.to_literal(variable_map)
+    fn to_solver_constraint_argument(self) -> Self::Output {
+        self.0
     }
 }
 
 impl PythonConstraintArg for i32 {
     type Output = i32;
 
-    fn to_solver_constraint_argument(self, _: &VariableMap) -> Self::Output {
+    fn to_solver_constraint_argument(self) -> Self::Output {
         self
     }
 }
 
 impl<Arg: PythonConstraintArg> PythonConstraintArg for Vec<Arg> {
     type Output = Vec<Arg::Output>;
 
-    fn to_solver_constraint_argument(self, variable_map: &VariableMap) -> Self::Output {
+    fn to_solver_constraint_argument(self) -> Self::Output {
         self.into_iter()
-            .map(|arg| arg.to_solver_constraint_argument(variable_map))
+            .map(|arg| arg.to_solver_constraint_argument())
             .collect()
     }
 }

pumpkin-solver-py/src/constraints/globals.rs

@@ -29,10 +29,9 @@ macro_rules! python_constraint {
             pub fn post(
                 self,
                 solver: &mut pumpkin_solver::Solver,
-                variable_map: &VariableMap,
             ) -> Result<(), pumpkin_solver::ConstraintOperationError> {
                 pumpkin_constraints::$constraint_func(
-                    $(<$type as super::arguments::PythonConstraintArg>::to_solver_constraint_argument(self.$field, variable_map)),+ ,
+                    $(<$type as super::arguments::PythonConstraintArg>::to_solver_constraint_argument(self.$field)),+ ,
                     self.constraint_tag.0,
                 ).post(solver)
             }
@@ -41,10 +40,9 @@ macro_rules! python_constraint {
                 self,
                 solver: &mut pumpkin_solver::Solver,
                 reification_literal: pumpkin_solver::variables::Literal,
-                variable_map: &VariableMap,
             ) -> Result<(), pumpkin_solver::ConstraintOperationError> {
                 pumpkin_constraints::$constraint_func(
-                    $(<$type as super::arguments::PythonConstraintArg>::to_solver_constraint_argument(self.$field, variable_map)),+ ,
+                    $(<$type as super::arguments::PythonConstraintArg>::to_solver_constraint_argument(self.$field)),+ ,
                     self.constraint_tag.0,
                 ).implied_by(solver, reification_literal)
             }

pumpkin-solver-py/src/constraints/mod.rs

@@ -15,21 +15,19 @@ macro_rules! declare_constraints {
             pub fn post(
                 self,
                 solver: &mut pumpkin_solver::Solver,
-                variable_map: &$crate::variables::VariableMap,
             ) -> Result<(), pumpkin_solver::ConstraintOperationError> {
                 match self {
-                    $($name::$constraint(cns) => cns.post(solver, variable_map)),+
+                    $($name::$constraint(cns) => cns.post(solver)),+
                 }
             }
 
             pub fn implied_by(
                 self,
                 solver: &mut pumpkin_solver::Solver,
                 reification_literal: pumpkin_solver::variables::Literal,
-                variable_map: &$crate::variables::VariableMap,
             ) -> Result<(), pumpkin_solver::ConstraintOperationError> {
                 match self {
-                    $($name::$constraint(cns) => cns.implied_by(solver, reification_literal, variable_map)),+
+                    $($name::$constraint(cns) => cns.implied_by(solver, reification_literal)),+
                 }
             }
         }