pumpkin_constraints/constraints/arithmetic/
mod.rs

1mod equality;
2mod inequality;
3
4pub use equality::*;
5pub use inequality::*;
6use pumpkin_core::constraints::Constraint;
7use pumpkin_core::proof::ConstraintTag;
8use pumpkin_core::variables::IntegerVariable;
9use pumpkin_propagators::arithmetic::AbsoluteValueArgs;
10use pumpkin_propagators::arithmetic::DivisionArgs;
11use pumpkin_propagators::arithmetic::IntegerMultiplicationArgs;
12use pumpkin_propagators::arithmetic::MaximumArgs;
13
14/// Creates the [`Constraint`] `a + b = c`.
15pub fn plus<Var: IntegerVariable + 'static>(
16    a: Var,
17    b: Var,
18    c: Var,
19    constraint_tag: ConstraintTag,
20) -> impl Constraint {
21    equals([a.scaled(1), b.scaled(1), c.scaled(-1)], 0, constraint_tag)
22}
23
24/// Creates the [`Constraint`] `a * b = c`.
25pub fn times(
26    a: impl IntegerVariable + 'static,
27    b: impl IntegerVariable + 'static,
28    c: impl IntegerVariable + 'static,
29    constraint_tag: ConstraintTag,
30) -> impl Constraint {
31    IntegerMultiplicationArgs {
32        a,
33        b,
34        c,
35        constraint_tag,
36    }
37}
38
39/// Creates the [`Constraint`] `numerator / denominator = rhs`.
40///
41/// Note that this [`Constraint`] models truncating division (i.e. rounding towards 0).
42///
43/// The `denominator` should not contain the value 0 in its domain; if this is the case then the
44/// solver will panic.
45pub fn division(
46    numerator: impl IntegerVariable + 'static,
47    denominator: impl IntegerVariable + 'static,
48    rhs: impl IntegerVariable + 'static,
49    constraint_tag: ConstraintTag,
50) -> impl Constraint {
51    DivisionArgs {
52        numerator,
53        denominator,
54        rhs,
55        constraint_tag,
56    }
57}
58
59/// Creates the [`Constraint`] `|signed| = absolute`.
60pub fn absolute(
61    signed: impl IntegerVariable + 'static,
62    absolute: impl IntegerVariable + 'static,
63    constraint_tag: ConstraintTag,
64) -> impl Constraint {
65    AbsoluteValueArgs {
66        signed,
67        absolute,
68        constraint_tag,
69    }
70}
71
72/// Creates the [`Constraint`] `max(array) = m`.
73pub fn maximum<Var: IntegerVariable + 'static>(
74    array: impl IntoIterator<Item = Var>,
75    rhs: impl IntegerVariable + 'static,
76    constraint_tag: ConstraintTag,
77) -> impl Constraint {
78    MaximumArgs {
79        array: array.into_iter().collect(),
80        rhs,
81        constraint_tag,
82    }
83}
84
85/// Creates the [`Constraint`] `min(array) = m`.
86pub fn minimum<Var: IntegerVariable + 'static>(
87    array: impl IntoIterator<Item = Var>,
88    rhs: impl IntegerVariable + 'static,
89    constraint_tag: ConstraintTag,
90) -> impl Constraint {
91    let array = array.into_iter().map(|var| var.scaled(-1));
92    maximum(array, rhs.scaled(-1), constraint_tag)
93}
pumpkin_constraints/constraints/arithmetic/mod.rs

pumpkin_constraints/constraints/arithmetic/
mod.rs
