pumpkin_core/api/outputs/
mod.rs

1use self::unsatisfiable::UnsatisfiableUnderAssumptions;
2pub use crate::basic_types::ProblemSolution;
3use crate::basic_types::Solution;
4pub use crate::basic_types::SolutionReference;
5use crate::Solver;
6pub mod solution_iterator;
7pub mod unsatisfiable;
8use crate::branching::Brancher;
9#[cfg(doc)]
10use crate::termination::TerminationCondition;
11
12/// The result of a call to [`Solver::satisfy`].
13#[derive(Debug)]
14pub enum SatisfactionResult<'solver, 'brancher, B: Brancher> {
15    /// Indicates that a solution was found.
16    ///
17    /// The solution can be obtained with [`Satisfiable::solution`], as well as the solver and
18    /// brancher. The solver and brancher may be of interest to e.g. log statistics. When the
19    /// result is dropped, the solver will be reset to the root, ready for further use.
20    Satisfiable(Satisfiable<'solver, 'brancher, B>),
21    /// Indicates that there is no solution to the satisfaction problem.
22    Unsatisfiable(&'solver Solver),
23    /// Indicates that it is not known whether a solution exists. This is likely due to a
24    /// [`TerminationCondition`] triggering.
25    Unknown(&'solver Solver),
26}
27
28/// The result of a call to [`Solver::satisfy_under_assumptions`].
29#[derive(Debug)]
30pub enum SatisfactionResultUnderAssumptions<'solver, 'brancher, B: Brancher> {
31    /// See documentation on [`SatisfactionResult::Satisfiable`].
32    Satisfiable(Satisfiable<'solver, 'brancher, B>),
33    /// Indicates that there is no solution to the satisfaction problem due to the provided
34    /// assumptions. It returns an [`UnsatisfiableUnderAssumptions`] which can be used to retrieve
35    /// an unsatisfiable core.
36    UnsatisfiableUnderAssumptions(UnsatisfiableUnderAssumptions<'solver, 'brancher, B>),
37    /// Indicates that there is no solution to the satisfaction problem.
38    Unsatisfiable(&'solver Solver),
39    /// Indicates that it is not known whether a solution exists. This is likely due to a
40    /// [`TerminationCondition`] triggering.
41    Unknown(&'solver Solver),
42}
43
44/// The result of a call to [`Solver::optimise`].
45#[derive(Debug)]
46pub enum OptimisationResult {
47    /// Indicates that an optimal solution has been found and proven to be optimal. It provides an
48    /// instance of [`Solution`] which contains the optimal solution.
49    Optimal(Solution),
50    /// Indicates that a solution was found and provides an instance of [`Solution`] which contains
51    /// best known solution by the solver.
52    Satisfiable(Solution),
53    /// Indicates that there is no solution to the problem.
54    Unsatisfiable,
55    /// Indicates that it is not known whether a solution exists. This is likely due to a
56    /// [`TerminationCondition`] triggering.
57    Unknown,
58}
59
60#[derive(Debug)]
61pub struct Satisfiable<'solver, 'brancher, B: Brancher> {
62    solver: &'solver mut Solver,
63    brancher: &'brancher mut B,
64}
65
66impl<'solver, 'brancher, B: Brancher> Satisfiable<'solver, 'brancher, B> {
67    pub(crate) fn new(solver: &'solver mut Solver, brancher: &'brancher mut B) -> Self {
68        Satisfiable { solver, brancher }
69    }
70
71    /// Get the solution that was discovered.
72    pub fn solution(&self) -> SolutionReference<'_> {
73        self.solver.get_solution_reference()
74    }
75
76    /// Get the solver instance.
77    pub fn solver(&self) -> &Solver {
78        self.solver
79    }
80
81    /// Get the brancher.
82    pub fn brancher(&self) -> &B {
83        self.brancher
84    }
85}
86
87impl<B: Brancher> Drop for Satisfiable<'_, '_, B> {
88    fn drop(&mut self) {
89        self.solver
90            .satisfaction_solver
91            .restore_state_at_root(self.brancher);
92    }
93}
pumpkin_core/api/outputs/mod.rs

pumpkin_core/api/outputs/
mod.rs
