pumpkin_core/constraints/
mod.rs

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

pumpkin_core/constraints/
mod.rs
