pumpkin_constraints/constraints/
clause.rs

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

pumpkin_constraints/constraints/
clause.rs
