pumpkin_constraints/constraints/arithmetic/
inequality.rs

1use pumpkin_core::ConstraintOperationError;
2use pumpkin_core::Solver;
3use pumpkin_core::constraints::Constraint;
4use pumpkin_core::constraints::NegatableConstraint;
5use pumpkin_core::proof::ConstraintTag;
6use pumpkin_core::variables::IntegerVariable;
7use pumpkin_core::variables::Literal;
8use pumpkin_propagators::arithmetic::LinearLessOrEqualPropagatorArgs;
9
10/// Create the [`NegatableConstraint`] `∑ terms_i <= rhs`.
11///
12/// Its negation is `∑ terms_i > rhs`
13pub fn less_than_or_equals<Var: IntegerVariable + 'static>(
14    terms: impl Into<Box<[Var]>>,
15    rhs: i32,
16    constraint_tag: ConstraintTag,
17) -> impl NegatableConstraint {
18    Inequality {
19        terms: terms.into(),
20        rhs,
21        constraint_tag,
22    }
23}
24
25/// Create the [`NegatableConstraint`] `∑ terms_i < rhs`.
26///
27/// Its negation is `∑ terms_i <= rhs`
28pub fn less_than<Var: IntegerVariable + 'static>(
29    terms: impl Into<Box<[Var]>>,
30    rhs: i32,
31    constraint_tag: ConstraintTag,
32) -> impl NegatableConstraint {
33    less_than_or_equals(terms, rhs - 1, constraint_tag)
34}
35
36/// Create the [`NegatableConstraint`] `∑ terms_i > rhs`.
37///
38/// Its negation is `∑ terms_i <= rhs`
39pub fn greater_than<Var: IntegerVariable + 'static>(
40    terms: impl Into<Box<[Var]>>,
41    rhs: i32,
42    constraint_tag: ConstraintTag,
43) -> impl NegatableConstraint {
44    greater_than_or_equals(terms, rhs + 1, constraint_tag)
45}
46
47/// Create the [`NegatableConstraint`] `∑ terms_i >= rhs`.
48///
49/// Its negation is `∑ terms_i < rhs`
50pub fn greater_than_or_equals<Var: IntegerVariable + 'static>(
51    terms: impl Into<Box<[Var]>>,
52    rhs: i32,
53    constraint_tag: ConstraintTag,
54) -> impl NegatableConstraint {
55    let terms: Box<[_]> = terms.into().iter().map(|var| var.scaled(-1)).collect();
56    less_than_or_equals(terms, -rhs, constraint_tag)
57}
58
59/// Creates the [`NegatableConstraint`] `lhs <= rhs`.
60///
61/// Its negation is `lhs > rhs`.
62pub fn binary_less_than_or_equals<Var: IntegerVariable + 'static>(
63    lhs: Var,
64    rhs: Var,
65    constraint_tag: ConstraintTag,
66) -> impl NegatableConstraint {
67    less_than_or_equals([lhs.scaled(1), rhs.scaled(-1)], 0, constraint_tag)
68}
69
70/// Creates the [`NegatableConstraint`] `lhs < rhs`.
71///
72/// Its negation is `lhs >= rhs`.
73pub fn binary_less_than<Var: IntegerVariable + 'static>(
74    lhs: Var,
75    rhs: Var,
76    constraint_tag: ConstraintTag,
77) -> impl NegatableConstraint {
78    binary_less_than_or_equals(lhs.scaled(1), rhs.offset(-1), constraint_tag)
79}
80
81/// Creates the [`NegatableConstraint`] `lhs >= rhs`.
82///
83/// Its negation is `lhs < rhs`.
84pub fn binary_greater_than_or_equals<Var: IntegerVariable + 'static>(
85    lhs: Var,
86    rhs: Var,
87    constraint_tag: ConstraintTag,
88) -> impl NegatableConstraint {
89    binary_less_than_or_equals(lhs.scaled(-1), rhs.scaled(-1), constraint_tag)
90}
91
92/// Creates the [`NegatableConstraint`] `lhs > rhs`.
93///
94/// Its negation is `lhs <= rhs`.
95pub fn binary_greater_than<Var: IntegerVariable + 'static>(
96    lhs: Var,
97    rhs: Var,
98    constraint_tag: ConstraintTag,
99) -> impl NegatableConstraint {
100    binary_less_than(lhs.scaled(-1), rhs.scaled(-1), constraint_tag)
101}
102
103struct Inequality<Var> {
104    terms: Box<[Var]>,
105    rhs: i32,
106    constraint_tag: ConstraintTag,
107}
108
109impl<Var: IntegerVariable + 'static> Constraint for Inequality<Var> {
110    fn post(self, solver: &mut Solver) -> Result<(), ConstraintOperationError> {
111        LinearLessOrEqualPropagatorArgs {
112            x: self.terms,
113            c: self.rhs,
114            constraint_tag: self.constraint_tag,
115        }
116        .post(solver)
117    }
118
119    fn implied_by(
120        self,
121        solver: &mut Solver,
122        reification_literal: Literal,
123    ) -> Result<(), ConstraintOperationError> {
124        LinearLessOrEqualPropagatorArgs {
125            x: self.terms,
126            c: self.rhs,
127            constraint_tag: self.constraint_tag,
128        }
129        .implied_by(solver, reification_literal)
130    }
131}
132
133impl<Var: IntegerVariable + 'static> NegatableConstraint for Inequality<Var> {
134    type NegatedConstraint = Inequality<Var::AffineView>;
135
136    fn negation(&self) -> Self::NegatedConstraint {
137        Inequality {
138            terms: self.terms.iter().map(|term| term.scaled(-1)).collect(),
139            rhs: -self.rhs - 1,
140            constraint_tag: self.constraint_tag,
141        }
142    }
143}
144
145#[cfg(test)]
146mod tests {
147    use super::*;
148
149    #[test]
150    fn less_than_conflict() {
151        let mut solver = Solver::default();
152
153        let constraint_tag = solver.new_constraint_tag();
154        let x = solver.new_named_bounded_integer(0, 0, "x");
155
156        let result = less_than([x], 0, constraint_tag).post(&mut solver);
157        assert_eq!(
158            result,
159            Err(ConstraintOperationError::InfeasiblePropagator),
160            "Expected {result:?} to be an `InfeasiblePropagator` error"
161        );
162    }
163
164    #[test]
165    fn greater_than_conflict() {
166        let mut solver = Solver::default();
167
168        let constraint_tag = solver.new_constraint_tag();
169        let x = solver.new_named_bounded_integer(0, 0, "x");
170
171        let result = greater_than([x], 0, constraint_tag).post(&mut solver);
172        assert_eq!(
173            result,
174            Err(ConstraintOperationError::InfeasiblePropagator),
175            "Expected {result:?} to be an `InfeasiblePropagator` error"
176        );
177    }
178}
pumpkin_constraints/constraints/arithmetic/inequality.rs

pumpkin_constraints/constraints/arithmetic/
inequality.rs
