drcp_format/
lib.rs

1//! This crate handles the reading and writing of proofs produced by
2//! [Pumpkin](https://github.com/consol-lab/pumpkin).
3//!
4//! For reading/parsing of proofs, use the [`reader`] module. To write proofs to string use the
5//! [`writer`] module.
6
7pub mod reader;
8pub mod writer;
9
10use std::fmt::Display;
11use std::num::NonZero;
12use std::ops::Add;
13use std::ops::Mul;
14use std::ops::Not;
15
16#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
17pub enum IntComparison {
18    GreaterEqual,
19    LessEqual,
20    Equal,
21    NotEqual,
22}
23
24impl Display for IntComparison {
25    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
26        let s = match self {
27            IntComparison::GreaterEqual => ">=",
28            IntComparison::LessEqual => "<=",
29            IntComparison::Equal => "==",
30            IntComparison::NotEqual => "!=",
31        };
32
33        write!(f, "{s}")
34    }
35}
36
37/// A contract that must be observed for the value in an [`IntAtomic`].
38///
39/// Implementations are provided for signed machine integers.
40pub trait IntValue: Clone + Display + Ord + Mul<Output = Self> + Add<Output = Self> {
41    fn increment(&self) -> Self;
42    fn decrement(&self) -> Self;
43
44    /// Multiply self by the radix.
45    fn shift_left(&self) -> Self;
46
47    /// Create self from char. Can panic if not possible.
48    fn from_digit(byte: u8) -> Self;
49}
50
51pub trait SignedIntValue: IntValue {
52    /// Multiply self by -1.
53    fn negate(&self) -> Self;
54}
55
56macro_rules! impl_int_value {
57    ($type:ty) => {
58        impl IntValue for $type {
59            #[inline]
60            fn increment(&self) -> Self {
61                (*self) + 1
62            }
63
64            #[inline]
65            fn decrement(&self) -> Self {
66                (*self) - 1
67            }
68
69            #[inline]
70            fn shift_left(&self) -> Self {
71                (*self) * 10
72            }
73
74            #[allow(trivial_numeric_casts, reason = "inside macro")]
75            #[inline]
76            fn from_digit(byte: u8) -> Self {
77                assert!(byte.is_ascii_digit());
78                (byte - b'0') as Self
79            }
80        }
81    };
82}
83
84macro_rules! impl_signed_int_value {
85    ($type:ty) => {
86        impl SignedIntValue for $type {
87            #[inline]
88            fn negate(&self) -> Self {
89                (*self) * -1
90            }
91        }
92    };
93}
94
95impl_int_value!(u8);
96impl_int_value!(u16);
97impl_int_value!(u32);
98impl_int_value!(u64);
99impl_int_value!(i8);
100impl_int_value!(i16);
101impl_int_value!(i32);
102impl_int_value!(i64);
103impl_signed_int_value!(i8);
104impl_signed_int_value!(i16);
105impl_signed_int_value!(i32);
106impl_signed_int_value!(i64);
107
108/// An integer atomic constraint of the form `[name op value]`, where `op` is an [`IntComparison`].
109#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
110pub struct IntAtomic<Identifier, Int> {
111    pub name: Identifier,
112    pub comparison: IntComparison,
113    pub value: Int,
114}
115
116impl<Identifier, Int> IntAtomic<Identifier, Int> {
117    /// Create a new integer atomic.
118    pub fn new(name: Identifier, comparison: IntComparison, value: Int) -> Self {
119        IntAtomic {
120            name,
121            comparison,
122            value,
123        }
124    }
125}
126
127impl<Identifier: Display, Int: Display> Display for IntAtomic<Identifier, Int> {
128    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
129        let IntAtomic {
130            name,
131            comparison,
132            value,
133        } = self;
134
135        write!(f, "[{name} {comparison} {value}]")
136    }
137}
138
139impl<Identifier, Int> Not for IntAtomic<Identifier, Int>
140where
141    Int: IntValue,
142{
143    type Output = Self;
144
145    fn not(self) -> Self::Output {
146        IntAtomic {
147            name: self.name,
148            comparison: match self.comparison {
149                IntComparison::GreaterEqual => IntComparison::LessEqual,
150                IntComparison::LessEqual => IntComparison::GreaterEqual,
151                IntComparison::Equal => IntComparison::NotEqual,
152                IntComparison::NotEqual => IntComparison::Equal,
153            },
154            value: match self.comparison {
155                IntComparison::GreaterEqual => self.value.decrement(),
156                IntComparison::LessEqual => self.value.increment(),
157                IntComparison::Equal | IntComparison::NotEqual => self.value,
158            },
159        }
160    }
161}
162
163/// The ID of a proof step.
164pub type ConstraintId = NonZero<u32>;
165
166/// An inference step.
167#[derive(Clone, Debug, PartialEq, Eq, Hash)]
168pub struct Inference<Identifier, Int, Label> {
169    /// The ID of the step.
170    pub constraint_id: ConstraintId,
171    /// The premises of the proof.
172    pub premises: Vec<IntAtomic<Identifier, Int>>,
173    /// The consequent of the proof. If this is [`None`], the `premises` explicitly describe a
174    /// conflicting assignment.
175    pub consequent: Option<IntAtomic<Identifier, Int>>,
176    /// The constraint that introduced this inference.
177    pub generated_by: Option<ConstraintId>,
178    /// The label that identifies the reasoning that introduced this inference.
179    pub label: Option<Label>,
180}
181
182/// An deduction step.
183#[derive(Clone, Debug, PartialEq, Eq, Hash)]
184pub struct Deduction<Identifier, Int> {
185    /// The ID of the step.
186    pub constraint_id: ConstraintId,
187    /// The premises of the proof.
188    pub premises: Vec<IntAtomic<Identifier, Int>>,
189    /// The constraints to apply to derive the deduction. These should point to [`Inference`]s, but
190    /// the parser does not verify that.
191    pub sequence: Vec<ConstraintId>,
192}
193
194/// The conclusion of the proof. This is the final line, and a proof without a conclusion can be
195/// considered incomplete. All steps after the conclusion can be ignored.
196#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
197pub enum Conclusion<Identifier, Int> {
198    /// The problem is unsatisfiable.
199    Unsat,
200    /// The proof concludes the given dual bound.
201    DualBound(IntAtomic<Identifier, Int>),
202}
203
204/// An individual proof step from the proof.
205#[derive(Clone, Debug, PartialEq, Eq, Hash)]
206pub enum Step<Identifier, Int, Label> {
207    Inference(Inference<Identifier, Int, Label>),
208    Deduction(Deduction<Identifier, Int>),
209    Conclusion(Conclusion<Identifier, Int>),
210}
drcp_format/lib.rs

drcp_format/
lib.rs
