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