Skip to main content

pumpkin_core/api/
mod.rs

1mod outputs;
2
3pub(crate) mod solver;
4
5pub mod results {
6    //! Contains the outputs of solving using the [`Solver`].
7    //!
8    //! We differentiate between 3 different types of results:
9    //! - For a **satisfaction** problem ([`SatisfactionResult`])
10    //! - For a **satisfaction** problem using **assumptions**
11    //!   ([`SatisfactionResultUnderAssumptions`])
12    //! - For an **optimisation** problem ([`OptimisationResult`])
13    //!
14    //! On these results, different methods can be called which ensure that the solver is in the
15    //! right state for these operations. For example,
16    //! [`SatisfactionResultUnderAssumptions::UnsatisfiableUnderAssumptions`] allows you to extract
17    //! a core consisting of the assumptions using [`UnsatisfiableUnderAssumptions::extract_core`].
18    #[cfg(doc)]
19    use crate::Solver;
20    pub use crate::api::outputs::OptimisationResult;
21    pub use crate::api::outputs::ProblemSolution;
22    pub use crate::api::outputs::SatisfactionResult;
23    pub use crate::api::outputs::SatisfactionResultUnderAssumptions;
24    pub use crate::api::outputs::Satisfiable;
25    pub use crate::api::outputs::SolutionReference;
26    pub use crate::api::outputs::solution_iterator;
27    pub use crate::api::outputs::unsatisfiable;
28    pub use crate::basic_types::Solution;
29    #[cfg(doc)]
30    use crate::results::unsatisfiable::UnsatisfiableUnderAssumptions;
31}
32
33pub mod variables {
34    //! Contains the variables which are used by the [`Solver`].
35    //!
36    //! A variable, in the context of the solver, is a view onto a domain. It may forward domain
37    //! information unaltered, or apply transformations which can be performed without the need of
38    //! constraints.
39    //!
40    //! We define 2 types of variables:
41    //! - Integer Variables ([`IntegerVariable`]) - These are represented by [`DomainId`]s when
42    //!   interacting with the [`Solver`]. These variables can be created using
43    //!   [`Solver::new_bounded_integer`] when creating a variable with the domain between a
44    //!   lower-bound and an upper-bound or using [`Solver::new_sparse_integer`] when creating a
45    //!   variable with holes in the domain. These variables can be transformed (according to the
46    //!   trait [`TransformableVariable`]) to create an [`AffineView`].
47    //! - Literals ([`Literal`]) - These specify booleans that can be used when interacting with the
48    //!   [`Solver`]. A [`Literal`] can be created using [`Solver::new_literal`].
49    #[cfg(doc)]
50    use crate::Solver;
51    pub use crate::engine::Reason;
52    pub use crate::engine::variables::AffineView;
53    pub use crate::engine::variables::DomainId;
54    pub use crate::engine::variables::IntegerVariable;
55    pub use crate::engine::variables::Literal;
56    pub use crate::engine::variables::TransformableVariable;
57}
58
59pub mod options {
60    //! Contains the options which can be passed to the [`Solver`].
61    //!
62    //! These influence the following aspects:
63    //! - The restart strategy of the solver
64    //! - The learned clause database management approach
65    //! - The proof logging
66    #[cfg(doc)]
67    use crate::Solver;
68    pub use crate::basic_types::sequence_generators::SequenceGeneratorType;
69    pub use crate::engine::ConflictResolverType;
70    pub use crate::engine::RestartOptions;
71    pub use crate::engine::SatisfactionSolverOptions as SolverOptions;
72    pub use crate::propagators::nogoods::LearningOptions;
73    pub use crate::propagators::reified_propagator::ReifiedPropagatorArgs;
74}
75
76pub mod termination {
77    //! Contains the conditions which are used to determine when the [`Solver`] should terminate
78    //! even when the state of the satisfaction/optimization problem is unknown.
79    //!
80    //! The main [`TerminationCondition`] is a condition which is polled by the [`Solver`] during
81    //! the search process. It indicates when the [`Solver`] should stop, even if no definitive
82    //! conclusions have been made.
83    //!
84    //! The most common example would be [`TimeBudget`], which terminates the [`Solver`] whenever
85    //! the time budget is exceeded.
86    #[cfg(doc)]
87    use crate::Solver;
88    pub use crate::basic_types::time::*;
89    pub use crate::engine::termination::TerminationCondition;
90    pub use crate::engine::termination::combinator::*;
91    pub use crate::engine::termination::indefinite::*;
92    pub use crate::engine::termination::time_budget::*;
93}
94
95pub mod predicates {
96    //! Contains structures which represent certain [predicates](https://en.wikipedia.org/wiki/Predicate_(mathematical_logic)).
97    //!
98    //! The solver only utilizes the following types of predicates:
99    //! - A predicate of the form `[x >= v]`
100    //! - A predicate of the form `[x <= v]`
101    //! - A predicate of the form `[x = v]`
102    //! - A predicate of the form `[x != v]`
103    //!
104    //! In general, these [`Predicate`]s are used to represent propagations, explanations or
105    //! decisions.
106    pub use crate::basic_types::PredicateIdGenerator;
107    pub use crate::basic_types::PropositionalConjunction;
108    pub use crate::engine::Lbd;
109    pub use crate::engine::predicates::predicate::Predicate;
110    pub use crate::engine::predicates::predicate::PredicateType;
111    pub use crate::engine::predicates::predicate_constructor::PredicateConstructor;
112    #[cfg(doc)]
113    use crate::variables::Literal;
114}
115
116pub mod state {
117    //! Contains structures for the state containing the propagators and variables.
118    //!
119    //! See [`State`] for more information.
120    pub use crate::api::solver::PropagatorHandle;
121    pub use crate::engine::Conflict;
122    pub use crate::engine::EmptyDomain;
123    pub use crate::engine::EmptyDomainConflict;
124    pub use crate::engine::PredicateHeap;
125    pub use crate::engine::PropagationStatusCP;
126    pub use crate::engine::PropagatorConflict;
127    pub use crate::engine::State;
128    pub use crate::engine::propagator_conflict;
129    pub use crate::propagation::CurrentNogood;
130    pub use crate::propagation::PropagatorId;
131}
132
133pub use crate::basic_types::Function;
134
135#[doc(hidden)]
136pub mod asserts {
137    pub use crate::pumpkin_assert_advanced;
138    pub use crate::pumpkin_assert_eq_simple;
139    pub use crate::pumpkin_assert_extreme;
140    pub use crate::pumpkin_assert_moderate;
141    pub use crate::pumpkin_assert_ne_moderate;
142    pub use crate::pumpkin_assert_ne_simple;
143    pub use crate::pumpkin_assert_simple;
144    pub use crate::pumpkin_asserts::PUMPKIN_ASSERT_ADVANCED;
145    pub use crate::pumpkin_asserts::PUMPKIN_ASSERT_EXTREME;
146    pub use crate::pumpkin_asserts::PUMPKIN_ASSERT_LEVEL_DEFINITION;
147    pub use crate::pumpkin_asserts::PUMPKIN_ASSERT_MODERATE;
148    pub use crate::pumpkin_asserts::PUMPKIN_ASSERT_SIMPLE;
149}