pumpkin_core/constraints/
mod.rs

1//! Defines the constraints that Pumpkin provides out of the box which can be added to the
2//! [`Solver`].
3//!
4//! A constraint is a relation over variables. In the solver, constraints are enforced through
5//! propagators, and therefore constraints can be viewed as a collection of propagators.
6//!
7//! # Example
8//! ```
9//! # use pumpkin_core::constraints;
10//! # use pumpkin_core::Solver;
11//! let mut solver = Solver::default();
12//!
13//! let a = solver.new_bounded_integer(0, 3);
14//! let b = solver.new_bounded_integer(0, 3);
15//!
16//! // All constraints require a constraint tag.
17//! let constraint_tag = solver.new_constraint_tag();
18//!
19//! solver
20//!     .add_constraint(constraints::equals([a, b], 0, constraint_tag))
21//!     .post();
22//! ```
23//!
24//! # Note
25//! At the moment, the API for posting propagators is not yet publicly accessible as it is
26//! unstable. Consumers of the Pumpkin library can therefore only define constraints by
27//! decomposing them into the constraints that are predefined in the library. Once the
28//! propagator API is stabilized, it will become part of the public API.
29
30mod all_different;
31mod arithmetic;
32mod boolean;
33mod clause;
34mod constraint_poster;
35mod cumulative;
36mod disjunctive_strict;
37mod element;
38mod table;
39
40pub use all_different::*;
41pub use arithmetic::*;
42pub use boolean::*;
43pub use clause::*;
44pub use constraint_poster::*;
45pub use cumulative::*;
46pub use disjunctive_strict::*;
47pub use element::*;
48pub use table::*;
49
50use crate::engine::propagation::constructor::PropagatorConstructor;
51use crate::propagators::ReifiedPropagatorArgs;
52use crate::variables::Literal;
53use crate::ConstraintOperationError;
54use crate::Solver;
55
56/// A [`Constraint`] is a relation over variables. It disqualifies certain partial assignments of
57/// making it into a solution of the problem.
58///
59/// For example, the constraint `a = b` over two variables `a` and `b` only allows assignments to
60/// `a` and `b` of the same value, and rejects any assignment where `a` and `b` differ.
61pub trait Constraint {
62    /// Add the [`Constraint`] to the [`Solver`].
63    ///
64    /// This method returns a [`ConstraintOperationError`] if the addition of the [`Constraint`] led
65    /// to a root-level conflict.
66    ///
67    /// The `tag` allows inferences to be traced to the constraint that implies them. They will
68    /// show up in the proof log.
69    fn post(self, solver: &mut Solver) -> Result<(), ConstraintOperationError>;
70
71    /// Add the half-reified version of the [`Constraint`] to the [`Solver`]; i.e. post the
72    /// constraint `r -> constraint` where `r` is a reification literal.
73    ///
74    /// This method returns a [`ConstraintOperationError`] if the addition of the [`Constraint`] led
75    /// to a root-level conflict.
76    ///
77    /// The `tag` allows inferences to be traced to the constraint that implies them. They will
78    /// show up in the proof log.
79    fn implied_by(
80        self,
81        solver: &mut Solver,
82        reification_literal: Literal,
83    ) -> Result<(), ConstraintOperationError>;
84}
85
86impl<ConcretePropagator> Constraint for ConcretePropagator
87where
88    ConcretePropagator: PropagatorConstructor + 'static,
89{
90    fn post(self, solver: &mut Solver) -> Result<(), ConstraintOperationError> {
91        let _ = solver.add_propagator(self)?;
92        Ok(())
93    }
94
95    fn implied_by(
96        self,
97        solver: &mut Solver,
98        reification_literal: Literal,
99    ) -> Result<(), ConstraintOperationError> {
100        let _ = solver.add_propagator(ReifiedPropagatorArgs {
101            propagator: self,
102            reification_literal,
103        })?;
104        Ok(())
105    }
106}
107
108impl<C: Constraint> Constraint for Vec<C> {
109    fn post(self, solver: &mut Solver) -> Result<(), ConstraintOperationError> {
110        self.into_iter().try_for_each(|c| c.post(solver))
111    }
112
113    fn implied_by(
114        self,
115        solver: &mut Solver,
116        reification_literal: Literal,
117    ) -> Result<(), ConstraintOperationError> {
118        self.into_iter()
119            .try_for_each(|c| c.implied_by(solver, reification_literal))
120    }
121}
122
123/// A [`Constraint`] which has a well-defined negation.
124///
125/// Having a negation means the [`Constraint`] can be fully reified; i.e., a constraint `C` can be
126/// turned into `r <-> C` where `r` is a reification literal.
127///
128/// For example, the negation of the [`Constraint`] `a = b` is (well-)defined as `a != b`.
129pub trait NegatableConstraint: Constraint {
130    type NegatedConstraint: NegatableConstraint + 'static;
131
132    fn negation(&self) -> Self::NegatedConstraint;
133
134    /// Add the reified version of the [`Constraint`] to the [`Solver`]; i.e. post the constraint
135    /// `r <-> constraint` where `r` is a reification literal.
136    ///
137    /// This method returns a [`ConstraintOperationError`] if the addition of the [`Constraint`] led
138    /// to a root-level conflict.
139    ///
140    /// The `tag` allows inferences to be traced to the constraint that implies them. They will
141    /// show up in the proof log.
142    fn reify(
143        self,
144        solver: &mut Solver,
145        reification_literal: Literal,
146    ) -> Result<(), ConstraintOperationError>
147    where
148        Self: Sized,
149    {
150        let negation = self.negation();
151
152        self.implied_by(solver, reification_literal)?;
153        negation.implied_by(solver, !reification_literal)
154    }
155}
pumpkin_core/constraints/mod.rs

pumpkin_core/constraints/
mod.rs
