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

use pumpkin_core::ConstraintOperationError;
use pumpkin_core::Solver;
use pumpkin_core::constraints::Constraint;
use pumpkin_core::constraints::NegatableConstraint;
use pumpkin_core::proof::ConstraintTag;
use pumpkin_core::variables::Literal;

/// Creates the [`NegatableConstraint`] `\/ literal`
///
/// Its negation is `/\ !literal`
pub fn clause(
    literals: impl Into<Vec<Literal>>,
    constraint_tag: ConstraintTag,
) -> impl NegatableConstraint {
    Clause(literals.into(), constraint_tag)
}

/// Creates the [`NegatableConstraint`] `/\ literal`
///
/// Its negation is `\/ !literal`
pub fn conjunction(
    literals: impl Into<Vec<Literal>>,
    constraint_tag: ConstraintTag,
) -> impl NegatableConstraint {
    Conjunction(literals.into(), constraint_tag)
}

struct Clause(Vec<Literal>, ConstraintTag);

impl Constraint for Clause {
    fn post(self, solver: &mut Solver) -> Result<(), ConstraintOperationError> {
        let Clause(clause, constraint_tag) = self;

        solver.add_clause(
            clause.iter().map(|literal| literal.get_true_predicate()),
            constraint_tag,
        )
    }

    fn implied_by(
        self,
        solver: &mut Solver,
        reification_literal: Literal,
    ) -> Result<(), ConstraintOperationError> {
        let Clause(clause, constraint_tag) = self;

        solver.add_clause(
            clause
                .into_iter()
                .chain(std::iter::once(!reification_literal))
                .map(|literal| literal.get_true_predicate()),
            constraint_tag,
        )
    }
}

impl NegatableConstraint for Clause {
    type NegatedConstraint = Conjunction;

    fn negation(&self) -> Self::NegatedConstraint {
        let Clause(clause, constraint_tag) = self;

        Conjunction(clause.iter().map(|&lit| !lit).collect(), *constraint_tag)
    }
}

struct Conjunction(Vec<Literal>, ConstraintTag);

impl Constraint for Conjunction {
    fn post(self, solver: &mut Solver) -> Result<(), ConstraintOperationError> {
        let Conjunction(conjunction, constraint_tag) = self;

        conjunction
            .into_iter()
            .try_for_each(|lit| solver.add_clause([lit.get_true_predicate()], constraint_tag))
    }

    fn implied_by(
        self,
        solver: &mut Solver,
        reification_literal: Literal,
    ) -> Result<(), ConstraintOperationError> {
        let Conjunction(conjunction, constraint_tag) = self;

        conjunction.into_iter().try_for_each(|lit| {
            solver.add_clause(
                [
                    (!(reification_literal)).get_true_predicate(),
                    lit.get_true_predicate(),
                ],
                constraint_tag,
            )
        })
    }
}

impl NegatableConstraint for Conjunction {
    type NegatedConstraint = Clause;

    fn negation(&self) -> Self::NegatedConstraint {
        let Conjunction(conjunction, constraint_tag) = self;

        Clause(
            conjunction.iter().map(|&lit| !lit).collect(),
            *constraint_tag,
        )
    }
}