pumpkin_constraints/constraints/
clause.rs

1use pumpkin_core::ConstraintOperationError;
2use pumpkin_core::Solver;
3use pumpkin_core::constraints::Constraint;
4use pumpkin_core::constraints::NegatableConstraint;
5use pumpkin_core::proof::ConstraintTag;
6use pumpkin_core::variables::Literal;
7
8/// Creates the [`NegatableConstraint`] `\/ literal`
9///
10/// Its negation is `/\ !literal`
11pub fn clause(
12    literals: impl Into<Vec<Literal>>,
13    constraint_tag: ConstraintTag,
14) -> impl NegatableConstraint {
15    Clause(literals.into(), constraint_tag)
16}
17
18/// Creates the [`NegatableConstraint`] `/\ literal`
19///
20/// Its negation is `\/ !literal`
21pub fn conjunction(
22    literals: impl Into<Vec<Literal>>,
23    constraint_tag: ConstraintTag,
24) -> impl NegatableConstraint {
25    Conjunction(literals.into(), constraint_tag)
26}
27
28struct Clause(Vec<Literal>, ConstraintTag);
29
30impl Constraint for Clause {
31    fn post(self, solver: &mut Solver) -> Result<(), ConstraintOperationError> {
32        let Clause(clause, constraint_tag) = self;
33
34        solver.add_clause(
35            clause.iter().map(|literal| literal.get_true_predicate()),
36            constraint_tag,
37        )
38    }
39
40    fn implied_by(
41        self,
42        solver: &mut Solver,
43        reification_literal: Literal,
44    ) -> Result<(), ConstraintOperationError> {
45        let Clause(clause, constraint_tag) = self;
46
47        solver.add_clause(
48            clause
49                .into_iter()
50                .chain(std::iter::once(!reification_literal))
51                .map(|literal| literal.get_true_predicate()),
52            constraint_tag,
53        )
54    }
55}
56
57impl NegatableConstraint for Clause {
58    type NegatedConstraint = Conjunction;
59
60    fn negation(&self) -> Self::NegatedConstraint {
61        let Clause(clause, constraint_tag) = self;
62
63        Conjunction(clause.iter().map(|&lit| !lit).collect(), *constraint_tag)
64    }
65}
66
67struct Conjunction(Vec<Literal>, ConstraintTag);
68
69impl Constraint for Conjunction {
70    fn post(self, solver: &mut Solver) -> Result<(), ConstraintOperationError> {
71        let Conjunction(conjunction, constraint_tag) = self;
72
73        conjunction
74            .into_iter()
75            .try_for_each(|lit| solver.add_clause([lit.get_true_predicate()], constraint_tag))
76    }
77
78    fn implied_by(
79        self,
80        solver: &mut Solver,
81        reification_literal: Literal,
82    ) -> Result<(), ConstraintOperationError> {
83        let Conjunction(conjunction, constraint_tag) = self;
84
85        conjunction.into_iter().try_for_each(|lit| {
86            solver.add_clause(
87                [
88                    (!(reification_literal)).get_true_predicate(),
89                    lit.get_true_predicate(),
90                ],
91                constraint_tag,
92            )
93        })
94    }
95}
96
97impl NegatableConstraint for Conjunction {
98    type NegatedConstraint = Clause;
99
100    fn negation(&self) -> Self::NegatedConstraint {
101        let Conjunction(conjunction, constraint_tag) = self;
102
103        Clause(
104            conjunction.iter().map(|&lit| !lit).collect(),
105            *constraint_tag,
106        )
107    }
108}
pumpkin_constraints/constraints/clause.rs

pumpkin_constraints/constraints/
clause.rs
