pumpkin_core/constraints/arithmetic/
mod.rs

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

pumpkin_core/constraints/arithmetic/
mod.rs
