pumpkin_core/constraints/
constraint_poster.rs

1use log::warn;
2
3use super::Constraint;
4use super::NegatableConstraint;
5use crate::variables::Literal;
6use crate::ConstraintOperationError;
7use crate::Solver;
8
9/// A structure which is responsible for adding the created [`Constraint`]s to the
10/// [`Solver`]. For an example on how to use this, see [`crate::constraints`].
11#[derive(Debug)]
12pub struct ConstraintPoster<'solver, ConstraintImpl> {
13    solver: &'solver mut Solver,
14    constraint: Option<ConstraintImpl>,
15}
16
17impl<'a, ConstraintImpl> ConstraintPoster<'a, ConstraintImpl> {
18    pub(crate) fn new(solver: &'a mut Solver, constraint: ConstraintImpl) -> Self {
19        ConstraintPoster {
20            solver,
21            constraint: Some(constraint),
22        }
23    }
24}
25
26impl<ConstraintImpl: Constraint> ConstraintPoster<'_, ConstraintImpl> {
27    /// Add the [`Constraint`] to the [`Solver`].
28    ///
29    /// This method returns a [`ConstraintOperationError`] if the addition of the [`Constraint`] led
30    /// to a root-level conflict.
31    pub fn post(mut self) -> Result<(), ConstraintOperationError> {
32        self.constraint.take().unwrap().post(self.solver)
33    }
34
35    /// Add the half-reified version of the [`Constraint`] to the [`Solver`]; i.e. post the
36    /// constraint `r -> constraint` where `r` is a reification literal.
37    ///
38    /// This method returns a [`ConstraintOperationError`] if the addition of the [`Constraint`] led
39    /// to a root-level conflict.
40    pub fn implied_by(
41        mut self,
42        reification_literal: Literal,
43    ) -> Result<(), ConstraintOperationError> {
44        self.constraint
45            .take()
46            .unwrap()
47            .implied_by(self.solver, reification_literal)
48    }
49}
50
51impl<ConstraintImpl: NegatableConstraint> ConstraintPoster<'_, ConstraintImpl> {
52    /// Add the reified version of the [`Constraint`] to the [`Solver`]; i.e. post the constraint
53    /// `r <-> constraint` where `r` is a reification literal.
54    ///
55    /// This method returns a [`ConstraintOperationError`] if the addition of the [`Constraint`] led
56    /// to a root-level conflict.
57    pub fn reify(mut self, reification_literal: Literal) -> Result<(), ConstraintOperationError> {
58        self.constraint
59            .take()
60            .unwrap()
61            .reify(self.solver, reification_literal)
62    }
63}
64
65impl<ConstraintImpl> Drop for ConstraintPoster<'_, ConstraintImpl> {
66    fn drop(&mut self) {
67        if self.constraint.is_some() {
68            warn!("A constraint poster is never used, this is likely a mistake.");
69        }
70    }
71}
pumpkin_core/constraints/constraint_poster.rs

pumpkin_core/constraints/
constraint_poster.rs
