pumpkin_checking/
atomic_constraint.rs

1use std::fmt::Debug;
2use std::fmt::Display;
3use std::hash::Hash;
4
5/// Captures the data associated with an atomic constraint.
6///
7/// An atomic constraint has the form `[identifier op value]`, where:
8/// - `identifier` identifies a variable,
9/// - `op` is a [`Comparison`],
10/// - and `value` is an integer.
11pub trait AtomicConstraint: Sized + Debug {
12    /// The type of identifier used for variables.
13    type Identifier: Hash + Eq;
14
15    /// The identifier of this atomic constraint.
16    fn identifier(&self) -> Self::Identifier;
17
18    /// The [`Comparison`] used for this atomic constraint.
19    fn comparison(&self) -> Comparison;
20
21    /// The value on the right-hand side of this atomic constraint.
22    fn value(&self) -> i32;
23
24    /// The strongest atomic constraint that is mutually exclusive with self.
25    fn negate(&self) -> Self;
26}
27
28/// An arithmetic comparison between two integers.
29#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
30pub enum Comparison {
31    GreaterEqual,
32    LessEqual,
33    Equal,
34    NotEqual,
35}
36
37impl Display for Comparison {
38    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
39        let s = match self {
40            Comparison::GreaterEqual => ">=",
41            Comparison::LessEqual => "<=",
42            Comparison::Equal => "==",
43            Comparison::NotEqual => "!=",
44        };
45
46        write!(f, "{s}")
47    }
48}
49
50/// A simple implementation of an [`AtomicConstraint`].
51#[derive(Clone, Copy, Debug, PartialEq)]
52pub struct TestAtomic {
53    pub name: &'static str,
54    pub comparison: Comparison,
55    pub value: i32,
56}
57
58impl AtomicConstraint for TestAtomic {
59    type Identifier = &'static str;
60
61    fn identifier(&self) -> Self::Identifier {
62        self.name
63    }
64
65    fn comparison(&self) -> Comparison {
66        self.comparison
67    }
68
69    fn value(&self) -> i32 {
70        self.value
71    }
72
73    fn negate(&self) -> Self {
74        TestAtomic {
75            name: self.name,
76            comparison: match self.comparison {
77                Comparison::GreaterEqual => Comparison::LessEqual,
78                Comparison::LessEqual => Comparison::GreaterEqual,
79                Comparison::Equal => Comparison::NotEqual,
80                Comparison::NotEqual => Comparison::Equal,
81            },
82            value: match self.comparison {
83                Comparison::GreaterEqual => self.value - 1,
84                Comparison::LessEqual => self.value + 1,
85                Comparison::NotEqual | Comparison::Equal => self.value,
86            },
87        }
88    }
89}
pumpkin_checking/atomic_constraint.rs

pumpkin_checking/
atomic_constraint.rs
