pumpkin_core/constraints/arithmetic/
inequality.rs

1use crate::constraints::Constraint;
2use crate::constraints::NegatableConstraint;
3use crate::proof::ConstraintTag;
4use crate::propagators::linear_less_or_equal::LinearLessOrEqualPropagatorArgs;
5use crate::variables::IntegerVariable;
6use crate::ConstraintOperationError;
7use crate::Solver;
8
9/// Create the [`NegatableConstraint`] `\sum terms_i <= rhs`.
10///
11/// Its negation is `\sum 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`] `\sum terms_i < rhs`.
25///
26/// Its negation is `\sum 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`] `\sum terms_i > rhs`.
36///
37/// Its negation is `\sum 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`] `\sum terms_i >= rhs`.
47///
48/// Its negation is `\sum 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) -> Result<(), ConstraintOperationError> {
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(
119        self,
120        solver: &mut Solver,
121        reification_literal: crate::variables::Literal,
122    ) -> Result<(), ConstraintOperationError> {
123        LinearLessOrEqualPropagatorArgs {
124            x: self.terms,
125            c: self.rhs,
126            constraint_tag: self.constraint_tag,
127        }
128        .implied_by(solver, reification_literal)
129    }
130}
131
132impl<Var: IntegerVariable + 'static> NegatableConstraint for Inequality<Var> {
133    type NegatedConstraint = Inequality<Var::AffineView>;
134
135    fn negation(&self) -> Self::NegatedConstraint {
136        Inequality {
137            terms: self.terms.iter().map(|term| term.scaled(-1)).collect(),
138            rhs: -self.rhs - 1,
139            constraint_tag: self.constraint_tag,
140        }
141    }
142}
pumpkin_core/constraints/arithmetic/inequality.rs

pumpkin_core/constraints/arithmetic/
inequality.rs
