pumpkin_constraints/constraints/
boolean.rs

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

pumpkin_constraints/constraints/
boolean.rs
