pumpkin_constraints/constraints/
boolean.rs

1use pumpkin_core::ConstraintOperationError;
2use pumpkin_core::Solver;
3use pumpkin_core::constraints::Constraint;
4use pumpkin_core::proof::ConstraintTag;
5use pumpkin_core::variables::AffineView;
6use pumpkin_core::variables::DomainId;
7use pumpkin_core::variables::Literal;
8use pumpkin_core::variables::TransformableVariable;
9
10use super::equals;
11use super::less_than_or_equals;
12
13/// Creates the [`Constraint`] `∑ weights_i * bools_i <= rhs`.
14pub fn boolean_less_than_or_equals(
15    weights: impl Into<Box<[i32]>>,
16    bools: impl Into<Box<[Literal]>>,
17    rhs: i32,
18    constraint_tag: ConstraintTag,
19) -> impl Constraint {
20    BooleanLessThanOrEqual {
21        weights: weights.into(),
22        bools: bools.into(),
23        rhs,
24        constraint_tag,
25    }
26}
27
28/// Creates the [`Constraint`] `∑ weights_i * bools_i == rhs`.
29pub fn boolean_equals(
30    weights: impl Into<Box<[i32]>>,
31    bools: impl Into<Box<[Literal]>>,
32    rhs: DomainId,
33    constraint_tag: ConstraintTag,
34) -> impl Constraint {
35    BooleanEqual {
36        weights: weights.into(),
37        bools: bools.into(),
38        rhs,
39        constraint_tag,
40    }
41}
42
43struct BooleanLessThanOrEqual {
44    weights: Box<[i32]>,
45    bools: Box<[Literal]>,
46    rhs: i32,
47    constraint_tag: ConstraintTag,
48}
49
50impl Constraint for BooleanLessThanOrEqual {
51    fn post(self, solver: &mut Solver) -> Result<(), ConstraintOperationError> {
52        let domains = self.create_domains();
53
54        less_than_or_equals(domains, self.rhs, self.constraint_tag).post(solver)
55    }
56
57    fn implied_by(
58        self,
59        solver: &mut Solver,
60        reification_literal: Literal,
61    ) -> Result<(), ConstraintOperationError> {
62        let domains = self.create_domains();
63
64        less_than_or_equals(domains, self.rhs, self.constraint_tag)
65            .implied_by(solver, reification_literal)
66    }
67}
68
69impl BooleanLessThanOrEqual {
70    fn create_domains(&self) -> Vec<AffineView<DomainId>> {
71        self.bools
72            .iter()
73            .enumerate()
74            .map(|(index, bool)| bool.get_integer_variable().scaled(self.weights[index]))
75            .collect()
76    }
77}
78
79struct BooleanEqual {
80    weights: Box<[i32]>,
81    bools: Box<[Literal]>,
82    rhs: DomainId,
83    constraint_tag: ConstraintTag,
84}
85
86impl Constraint for BooleanEqual {
87    fn post(self, solver: &mut Solver) -> Result<(), ConstraintOperationError> {
88        let domains = self.create_domains();
89
90        equals(domains, 0, self.constraint_tag).post(solver)
91    }
92
93    fn implied_by(
94        self,
95        solver: &mut Solver,
96        reification_literal: Literal,
97    ) -> Result<(), ConstraintOperationError> {
98        let domains = self.create_domains();
99
100        equals(domains, 0, self.constraint_tag).implied_by(solver, reification_literal)
101    }
102}
103
104impl BooleanEqual {
105    fn create_domains(&self) -> Vec<AffineView<DomainId>> {
106        self.bools
107            .iter()
108            .enumerate()
109            .map(|(index, bool)| bool.get_integer_variable().scaled(self.weights[index]))
110            .chain(std::iter::once(self.rhs.scaled(-1)))
111            .collect()
112    }
113}
pumpkin_constraints/constraints/boolean.rs

pumpkin_constraints/constraints/
boolean.rs
