Merge branch 'develop' into feat/brancher-statistics

.github/workflows/ci.yml

@@ -28,6 +28,22 @@ jobs:
     - uses: dtolnay/rust-toolchain@stable
     - run: cargo test --release --no-fail-fast
 
+  pumpkin-py:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: 3.x
+      - name: Install pytest
+        run: pip install pytest
+      - name: Install pumpkin-py
+        run: pip install -e .
+        working-directory: pumpkin-py
+      - name: Run tests
+        run: pytest
+        working-directory: pumpkin-py
+
   docs:
     name: Documentation
     runs-on: ubuntu-latest

drcp-format/src/writer/mod.rs

@@ -293,9 +293,7 @@ impl WritableProofStep for Deletion {
 mod tests {
     use super::*;
 
-    // Safety: Unwrapping an option is not stable, so we cannot get a NonZero<T> safely in a const
-    // context.
-    const TEST_ID: NonZeroU64 = unsafe { NonZeroU64::new_unchecked(1) };
+    const TEST_ID: NonZeroU64 = NonZeroU64::new(1).unwrap();
 
     #[test]
     fn write_basic_inference() {

pumpkin-py/src/lib.rs

@@ -1,5 +1,6 @@
 mod constraints;
 mod model;
+mod optimisation;
 mod result;
 mod variables;
 
@@ -27,12 +28,15 @@ macro_rules! submodule {
 fn pumpkin_py(python: Python, m: &Bound<'_, PyModule>) -> PyResult<()> {
     m.add_class::<variables::IntExpression>()?;
     m.add_class::<variables::BoolExpression>()?;
-    m.add_class::<model::Comparator>()?;
+    m.add_class::<variables::Comparator>()?;
+    m.add_class::<variables::Predicate>()?;
     m.add_class::<model::Model>()?;
     m.add_class::<result::SatisfactionResult>()?;
+    m.add_class::<result::SatisfactionUnderAssumptionsResult>()?;
     m.add_class::<result::Solution>()?;
 
     submodule!(constraints, python, m);
+    submodule!(optimisation, python, m);
 
     Ok(())
 }

pumpkin-py/src/model.rs

@@ -2,6 +2,9 @@ use std::num::NonZero;
 use std::path::PathBuf;
 
 use pumpkin_solver::containers::KeyedVec;
+use pumpkin_solver::optimisation::linear_sat_unsat::LinearSatUnsat;
+use pumpkin_solver::optimisation::linear_unsat_sat::LinearUnsatSat;
+use pumpkin_solver::optimisation::OptimisationDirection;
 use pumpkin_solver::options::SolverOptions;
 use pumpkin_solver::predicate;
 use pumpkin_solver::proof::Format;
@@ -14,12 +17,17 @@ use pumpkin_solver::Solver;
 use pyo3::prelude::*;
 
 use crate::constraints::Constraint;
+use crate::optimisation::Direction;
+use crate::optimisation::OptimisationResult;
+use crate::optimisation::Optimiser;
 use crate::result::SatisfactionResult;
+use crate::result::SatisfactionUnderAssumptionsResult;
 use crate::result::Solution;
 use crate::variables::BoolExpression;
 use crate::variables::BoolVariable;
 use crate::variables::IntExpression;
 use crate::variables::IntVariable;
+use crate::variables::Predicate;
 use crate::variables::VariableMap;
 
 #[pyclass]
@@ -30,15 +38,6 @@ pub struct Model {
     constraints: Vec<ModelConstraint>,
 }
 
-#[pyclass(eq, eq_int)]
-#[derive(Clone, Copy, PartialEq, Eq)]
-pub enum Comparator {
-    NotEqual,
-    Equal,
-    LessThanOrEqual,
-    GreaterThanOrEqual,
-}
-
 #[pymethods]
 impl Model {
     #[new]
@@ -115,23 +114,13 @@ impl Model {
         }
     }
 
-    #[pyo3(signature = (integer, comparator, value, name=None))]
-    fn predicate_as_boolean(
-        &mut self,
-        integer: IntExpression,
-        comparator: Comparator,
-        value: i32,
-        name: Option<&str>,
-    ) -> BoolExpression {
+    #[pyo3(signature = (predicate, name=None))]
+    fn predicate_as_boolean(&mut self, predicate: Predicate, name: Option<&str>) -> BoolExpression {
         self.boolean_variables
             .push(ModelBoolVar {
                 name: name.map(|n| n.to_owned()),
                 integer_equivalent: None,
-                predicate: Some(Predicate {
-                    integer,
-                    comparator,
-                    value,
-                }),
+                predicate: Some(predicate),
             })
             .into()
     }
@@ -163,27 +152,9 @@ impl Model {
 
     #[pyo3(signature = (proof=None))]
     fn satisfy(&self, proof: Option<PathBuf>) -> SatisfactionResult {
-        let proof_log = proof
-            .map(|path| ProofLog::cp(&path, Format::Text, true, true))
-            .transpose()
-            .map(|proof| proof.unwrap_or_default())
-            .expect("failed to create proof file");
+        let solver_setup = self.create_solver(proof);
 
-        let options = SolverOptions {
-            proof_log,
-            ..Default::default()
-        };
-
-        let mut solver = Solver::with_options(options);
-
-        let solver_setup = self
-            .create_variable_map(&mut solver)
-            .and_then(|variable_map| {
-                self.post_constraints(&mut solver, &variable_map)?;
-                Ok(variable_map)
-            });
-
-        let Ok(variable_map) = solver_setup else {
+        let Ok((mut solver, variable_map)) = solver_setup else {
             return SatisfactionResult::Unsatisfiable();
         };
 
@@ -202,6 +173,126 @@ impl Model {
             pumpkin_solver::results::SatisfactionResult::Unknown => SatisfactionResult::Unknown(),
         }
     }
+
+    #[pyo3(signature = (assumptions))]
+    fn satisfy_under_assumptions(
+        &self,
+        assumptions: Vec<Predicate>,
+    ) -> SatisfactionUnderAssumptionsResult {
+        let solver_setup = self.create_solver(None);
+
+        let Ok((mut solver, variable_map)) = solver_setup else {
+            return SatisfactionUnderAssumptionsResult::Unsatisfiable();
+        };
+
+        let mut brancher = solver.default_brancher();
+
+        let solver_assumptions = assumptions
+            .iter()
+            .map(|pred| pred.to_solver_predicate(&variable_map))
+            .collect::<Vec<_>>();
+
+        // Maarten: I do not understand why it is necessary, but we have to create a local variable
+        // here     that is the result of the `match` statement. Otherwise the compiler
+        // complains that     `solver` and `brancher` potentially do not live long enough.
+        //
+        //     Ideally this would not be necessary, but perhaps it is unavoidable with the setup we
+        //     currently have. Either way, we take the suggestion by the compiler.
+        let result = match solver.satisfy_under_assumptions(&mut brancher, &mut Indefinite, &solver_assumptions) {
+            pumpkin_solver::results::SatisfactionResultUnderAssumptions::Satisfiable(solution) => {
+                SatisfactionUnderAssumptionsResult::Satisfiable(Solution {
+                    solver_solution: solution,
+                    variable_map,
+                })
+            }
+            pumpkin_solver::results::SatisfactionResultUnderAssumptions::UnsatisfiableUnderAssumptions(mut result) => {
+                // Maarten: For now we assume that the core _must_ consist of the predicates that
+                //     were the input to the solve call. In general this is not the case, e.g. when
+                //     the assumptions can be semantically minized (the assumptions [y <= 1],
+                //     [y >= 0] and [y != 0] will be compressed to [y == 1] which would end up in
+                //     the core).
+                //
+                //     In the future, perhaps we should make the distinction between predicates and
+                //     literals in the python wrapper as well. For now, this is the simplest way
+                //     forward. I expect that the situation above almost never happens in practice.
+                let core = result
+                    .extract_core()
+                    .iter()
+                    .map(|predicate| assumptions
+                         .iter()
+                         .find(|pred| pred.to_solver_predicate(&variable_map) == *predicate)
+                         .copied()
+                         .expect("predicates in core must be part of the assumptions"))
+                    .collect();
+
+                SatisfactionUnderAssumptionsResult::UnsatisfiableUnderAssumptions(core)
+            }
+            pumpkin_solver::results::SatisfactionResultUnderAssumptions::Unsatisfiable => {
+                SatisfactionUnderAssumptionsResult::Unsatisfiable()
+            }
+            pumpkin_solver::results::SatisfactionResultUnderAssumptions::Unknown => {
+                SatisfactionUnderAssumptionsResult::Unknown()
+            }
+        };
+
+        result
+    }
+
+    #[pyo3(signature = (objective, optimiser=Optimiser::LinearSatUnsat, direction=Direction::Minimise, proof=None))]
+    fn optimise(
+        &self,
+        objective: IntExpression,
+        optimiser: Optimiser,
+        direction: Direction,
+        proof: Option<PathBuf>,
+    ) -> OptimisationResult {
+        let solver_setup = self.create_solver(proof);
+
+        let Ok((mut solver, variable_map)) = solver_setup else {
+            return OptimisationResult::Unsatisfiable();
+        };
+
+        let mut brancher = solver.default_brancher();
+
+        let direction = match direction {
+            Direction::Minimise => OptimisationDirection::Minimise,
+            Direction::Maximise => OptimisationDirection::Maximise,
+        };
+
+        let objective = objective.to_affine_view(&variable_map);
+
+        let result = match optimiser {
+            Optimiser::LinearSatUnsat => solver.optimise(
+                &mut brancher,
+                &mut Indefinite,
+                LinearSatUnsat::new(direction, objective, |_, _, _| {}),
+            ),
+            Optimiser::LinearUnsatSat => solver.optimise(
+                &mut brancher,
+                &mut Indefinite,
+                LinearUnsatSat::new(direction, objective, |_, _, _| {}),
+            ),
+        };
+
+        match result {
+            pumpkin_solver::results::OptimisationResult::Satisfiable(solution) => {
+                OptimisationResult::Satisfiable(Solution {
+                    solver_solution: solution,
+                    variable_map,
+                })
+            }
+            pumpkin_solver::results::OptimisationResult::Optimal(solution) => {
+                OptimisationResult::Optimal(Solution {
+                    solver_solution: solution,
+                    variable_map,
+                })
+            }
+            pumpkin_solver::results::OptimisationResult::Unsatisfiable => {
+                OptimisationResult::Unsatisfiable()
+            }
+            pumpkin_solver::results::OptimisationResult::Unknown => OptimisationResult::Unknown(),
+        }
+    }
 }
 
 impl Model {
@@ -252,6 +343,33 @@ impl Model {
 
         Ok(())
     }
+
+    fn create_solver(
+        &self,
+        proof: Option<PathBuf>,
+    ) -> Result<(Solver, VariableMap), ConstraintOperationError> {
+        let proof_log = proof
+            .map(|path| ProofLog::cp(&path, Format::Text, true, true))
+            .transpose()
+            .map(|proof| proof.unwrap_or_default())
+            .expect("failed to create proof file");
+
+        let options = SolverOptions {
+            proof_log,
+            ..Default::default()
+        };
+
+        let mut solver = Solver::with_options(options);
+
+        let variable_map = self
+            .create_variable_map(&mut solver)
+            .and_then(|variable_map| {
+                self.post_constraints(&mut solver, &variable_map)?;
+                Ok(variable_map)
+            })?;
+
+        Ok((solver, variable_map))
+    }
 }
 
 #[derive(Clone)]
@@ -340,26 +458,3 @@ impl ModelBoolVar {
         Ok(literal)
     }
 }
-
-struct Predicate {
-    integer: IntExpression,
-    comparator: Comparator,
-    value: i32,
-}
-
-impl Predicate {
-    /// Convert the predicate in the model domain to a predicate in the solver domain.
-    fn to_solver_predicate(
-        &self,
-        variable_map: &VariableMap,
-    ) -> pumpkin_solver::predicates::Predicate {
-        let affine_view = self.integer.to_affine_view(variable_map);
-
-        match self.comparator {
-            Comparator::NotEqual => predicate![affine_view != self.value],
-            Comparator::Equal => predicate![affine_view == self.value],
-            Comparator::LessThanOrEqual => predicate![affine_view <= self.value],
-            Comparator::GreaterThanOrEqual => predicate![affine_view >= self.value],
-        }
-    }
-}