pumpkin_core/constraints/
mod.rs

1//! Defines the main building blocks of constraints.
2use crate::Solver;
3use crate::propagation::PropagatorConstructor;
4use crate::propagators::reified_propagator::ReifiedPropagatorArgs;
5use crate::variables::Literal;
6
7mod constraint_poster;
8pub use constraint_poster::ConstraintPoster;
9
10/// A [`Constraint`] is a relation over variables. It disqualifies certain partial assignments of
11/// making it into a solution of the problem.
12///
13/// For example, the constraint `a = b` over two variables `a` and `b` only allows assignments to
14/// `a` and `b` of the same value, and rejects any assignment where `a` and `b` differ.
15pub trait Constraint {
16    /// Add the [`Constraint`] to the [`Solver`].
17    ///
18    /// The `tag` allows inferences to be traced to the constraint that implies them. They will
19    /// show up in the proof log.
20    fn post(self, solver: &mut Solver);
21
22    /// Add the half-reified version of the [`Constraint`] to the [`Solver`]; i.e. post the
23    /// constraint `r -> constraint` where `r` is a reification literal.
24    ///
25    /// The `tag` allows inferences to be traced to the constraint that implies them. They will
26    /// show up in the proof log.
27    fn implied_by(self, solver: &mut Solver, reification_literal: Literal);
28}
29
30impl<ConcretePropagator> Constraint for ConcretePropagator
31where
32    ConcretePropagator: PropagatorConstructor + 'static,
33{
34    fn post(self, solver: &mut Solver) {
35        let _ = solver.add_propagator(self);
36    }
37
38    fn implied_by(self, solver: &mut Solver, reification_literal: Literal) {
39        let _ = solver.add_propagator(ReifiedPropagatorArgs {
40            propagator: self,
41            reification_literal,
42        });
43    }
44}
45
46impl<C: Constraint> Constraint for Vec<C> {
47    fn post(self, solver: &mut Solver) {
48        self.into_iter().for_each(|c| c.post(solver))
49    }
50
51    fn implied_by(self, solver: &mut Solver, reification_literal: Literal) {
52        self.into_iter()
53            .for_each(|c| c.implied_by(solver, reification_literal))
54    }
55}
56
57/// A [`Constraint`] which has a well-defined negation.
58///
59/// Having a negation means the [`Constraint`] can be fully reified; i.e., a constraint `C` can be
60/// turned into `r <-> C` where `r` is a reification literal.
61///
62/// For example, the negation of the [`Constraint`] `a = b` is (well-)defined as `a != b`.
63pub trait NegatableConstraint: Constraint {
64    type NegatedConstraint: NegatableConstraint + 'static;
65
66    fn negation(&self) -> Self::NegatedConstraint;
67
68    /// Add the reified version of the [`Constraint`] to the [`Solver`]; i.e. post the constraint
69    /// `r <-> constraint` where `r` is a reification literal.
70    ///
71    /// The `tag` allows inferences to be traced to the constraint that implies them. They will
72    /// show up in the proof log.
73    fn reify(self, solver: &mut Solver, reification_literal: Literal)
74    where
75        Self: Sized,
76    {
77        let negation = self.negation();
78
79        self.implied_by(solver, reification_literal);
80        negation.implied_by(solver, !reification_literal)
81    }
82}
pumpkin_core/constraints/mod.rs

pumpkin_core/constraints/
mod.rs
