pumpkin_constraints/constraints/arithmetic/
inequality.rs

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

pumpkin_constraints/constraints/arithmetic/
inequality.rs
