pumpkin_core/api/outputs/
mod.rs

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

pumpkin_core/api/outputs/
mod.rs
