pumpkin-constraints 0.4.0

The constraints of the Pumpkin constraint programming solver.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113

use pumpkin_core::ConstraintOperationError;
use pumpkin_core::Solver;
use pumpkin_core::constraints::Constraint;
use pumpkin_core::proof::ConstraintTag;
use pumpkin_core::variables::AffineView;
use pumpkin_core::variables::DomainId;
use pumpkin_core::variables::Literal;
use pumpkin_core::variables::TransformableVariable;

use super::equals;
use super::less_than_or_equals;

/// Creates the [`Constraint`] `∑ weights_i * bools_i <= rhs`.
pub fn boolean_less_than_or_equals(
    weights: impl Into<Box<[i32]>>,
    bools: impl Into<Box<[Literal]>>,
    rhs: i32,
    constraint_tag: ConstraintTag,
) -> impl Constraint {
    BooleanLessThanOrEqual {
        weights: weights.into(),
        bools: bools.into(),
        rhs,
        constraint_tag,
    }
}

/// Creates the [`Constraint`] `∑ weights_i * bools_i == rhs`.
pub fn boolean_equals(
    weights: impl Into<Box<[i32]>>,
    bools: impl Into<Box<[Literal]>>,
    rhs: DomainId,
    constraint_tag: ConstraintTag,
) -> impl Constraint {
    BooleanEqual {
        weights: weights.into(),
        bools: bools.into(),
        rhs,
        constraint_tag,
    }
}

struct BooleanLessThanOrEqual {
    weights: Box<[i32]>,
    bools: Box<[Literal]>,
    rhs: i32,
    constraint_tag: ConstraintTag,
}

impl Constraint for BooleanLessThanOrEqual {
    fn post(self, solver: &mut Solver) -> Result<(), ConstraintOperationError> {
        let domains = self.create_domains();

        less_than_or_equals(domains, self.rhs, self.constraint_tag).post(solver)
    }

    fn implied_by(
        self,
        solver: &mut Solver,
        reification_literal: Literal,
    ) -> Result<(), ConstraintOperationError> {
        let domains = self.create_domains();

        less_than_or_equals(domains, self.rhs, self.constraint_tag)
            .implied_by(solver, reification_literal)
    }
}

impl BooleanLessThanOrEqual {
    fn create_domains(&self) -> Vec<AffineView<DomainId>> {
        self.bools
            .iter()
            .enumerate()
            .map(|(index, bool)| bool.get_integer_variable().scaled(self.weights[index]))
            .collect()
    }
}

struct BooleanEqual {
    weights: Box<[i32]>,
    bools: Box<[Literal]>,
    rhs: DomainId,
    constraint_tag: ConstraintTag,
}

impl Constraint for BooleanEqual {
    fn post(self, solver: &mut Solver) -> Result<(), ConstraintOperationError> {
        let domains = self.create_domains();

        equals(domains, 0, self.constraint_tag).post(solver)
    }

    fn implied_by(
        self,
        solver: &mut Solver,
        reification_literal: Literal,
    ) -> Result<(), ConstraintOperationError> {
        let domains = self.create_domains();

        equals(domains, 0, self.constraint_tag).implied_by(solver, reification_literal)
    }
}

impl BooleanEqual {
    fn create_domains(&self) -> Vec<AffineView<DomainId>> {
        self.bools
            .iter()
            .enumerate()
            .map(|(index, bool)| bool.get_integer_variable().scaled(self.weights[index]))
            .chain(std::iter::once(self.rhs.scaled(-1)))
            .collect()
    }
}