diff --git a/pumpkin-solver-py/examples/optimisation.py b/pumpkin-solver-py/examples/optimisation.py new file mode 100644 index 000000000..2f80b0455 --- /dev/null +++ b/pumpkin-solver-py/examples/optimisation.py @@ -0,0 +1,41 @@ +from argparse import ArgumentParser +from pathlib import Path + +from pumpkin_solver import constraints, Model +from pumpkin_solver.optimisation import OptimisationResult + + +def main(proof: Path | None): + model = Model(proof=proof) + + objective = model.new_integer_variable(10, 20, name="objective") + + # .. build the model here + + def on_solution(solution): + objective_value = solution.int_value(objective) + print(f"objective_value={objective_value}") + + status = model.optimise(objective, on_solution=on_solution) + match status: + case OptimisationResult.Optimal(_solution): + print("OPTIMAL") + + case OptimisationResult.Satisfiable(_solution): + print("SATISFIABLE") + + case OptimisationResult.Unsatisfiable(): + print("UNSATISFIABLE") + + case OptimisationResult.Unknown(): + print("UNKNOWN") + + +if __name__ == "__main__": + arg_parser = ArgumentParser() + + arg_parser.add_argument("--proof", type=Path, help="The proof file.", default=None) + + args = arg_parser.parse_args() + + main(args.proof) diff --git a/pumpkin-solver-py/src/model.rs b/pumpkin-solver-py/src/model.rs index 31199bdc7..1aa863a10 100644 --- a/pumpkin-solver-py/src/model.rs +++ b/pumpkin-solver-py/src/model.rs @@ -246,13 +246,15 @@ impl Model { } } - #[pyo3(signature = (objective, optimiser=Optimiser::LinearSatUnsat, direction=Direction::Minimise, timeout=None))] + #[pyo3(signature = (objective, optimiser=Optimiser::LinearSatUnsat, direction=Direction::Minimise, timeout=None, on_solution=None))] fn optimise( &mut self, + py: Python<'_>, objective: IntExpression, optimiser: Optimiser, direction: Direction, timeout: Option, + on_solution: Option>, ) -> OptimisationResult { let mut termination = get_termination(timeout); @@ -263,7 +265,15 @@ impl Model { let objective = objective.0; - let callback: fn(&Solver, SolutionReference, &DefaultBrancher) = |_, _, _| {}; + let callback = move |_: &Solver, solution: SolutionReference<'_>, _: &DefaultBrancher| { + let python_solution = crate::result::Solution::from(solution); + + if let Some(on_solution_callback) = on_solution.as_ref() { + let _ = on_solution_callback + .call(py, (python_solution,), None) + .expect("failed to call solution callback"); + } + }; let result = match optimiser { Optimiser::LinearSatUnsat => self.solver.optimise(