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::Not;
13use std::str::FromStr;
14
15#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
16pub enum IntComparison {
17    GreaterEqual,
18    LessEqual,
19    Equal,
20    NotEqual,
21}
22
23impl Display for IntComparison {
24    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
25        let s = match self {
26            IntComparison::GreaterEqual => ">=",
27            IntComparison::LessEqual => "<=",
28            IntComparison::Equal => "==",
29            IntComparison::NotEqual => "!=",
30        };
31
32        write!(f, "{s}")
33    }
34}
35
36/// A contract that must be observed for the value in an [`IntAtomic`].
37///
38/// Implementations are provided for signed machine integers.
39pub trait IntValue: Clone + Display + FromStr + Ord {
40    fn increment(&self) -> Self;
41    fn decrement(&self) -> Self;
42}
43
44macro_rules! impl_int_value {
45    ($type:ty) => {
46        impl IntValue for $type {
47            fn increment(&self) -> Self {
48                (*self) + 1
49            }
50
51            fn decrement(&self) -> Self {
52                (*self) - 1
53            }
54        }
55    };
56}
57
58impl_int_value!(i8);
59impl_int_value!(i16);
60impl_int_value!(i32);
61impl_int_value!(i64);
62
63/// An integer atomic constraint of the form `[name op value]`, where `op` is an [`IntComparison`].
64#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
65pub struct IntAtomic<Identifier, Int> {
66    pub name: Identifier,
67    pub comparison: IntComparison,
68    pub value: Int,
69}
70
71impl<Identifier, Int> IntAtomic<Identifier, Int> {
72    /// Create a new integer atomic.
73    pub fn new(name: Identifier, comparison: IntComparison, value: Int) -> Self {
74        IntAtomic {
75            name,
76            comparison,
77            value,
78        }
79    }
80}
81
82impl<Identifier: Display, Int: Display> Display for IntAtomic<Identifier, Int> {
83    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
84        let IntAtomic {
85            name,
86            comparison,
87            value,
88        } = self;
89
90        write!(f, "[{name} {comparison} {value}]")
91    }
92}
93
94impl<Identifier, Int> Not for IntAtomic<Identifier, Int>
95where
96    Int: IntValue,
97{
98    type Output = Self;
99
100    fn not(self) -> Self::Output {
101        IntAtomic {
102            name: self.name,
103            comparison: match self.comparison {
104                IntComparison::GreaterEqual => IntComparison::LessEqual,
105                IntComparison::LessEqual => IntComparison::GreaterEqual,
106                IntComparison::Equal => IntComparison::NotEqual,
107                IntComparison::NotEqual => IntComparison::Equal,
108            },
109            value: match self.comparison {
110                IntComparison::GreaterEqual => self.value.decrement(),
111                IntComparison::LessEqual => self.value.increment(),
112                IntComparison::Equal | IntComparison::NotEqual => self.value,
113            },
114        }
115    }
116}
117
118/// The ID of a proof step.
119pub type ConstraintId = NonZero<u32>;
120
121/// An inference step.
122#[derive(Clone, Debug, PartialEq, Eq, Hash)]
123pub struct Inference<Identifier, Int, Label> {
124    /// The ID of the step.
125    pub constraint_id: ConstraintId,
126    /// The premises of the proof.
127    pub premises: Vec<IntAtomic<Identifier, Int>>,
128    /// The consequent of the proof. If this is [`None`], the `premises` explicitly describe a
129    /// conflicting assignment.
130    pub consequent: Option<IntAtomic<Identifier, Int>>,
131    /// The constraint that introduced this inference.
132    pub generated_by: Option<ConstraintId>,
133    /// The label that identifies the reasoning that introduced this inference.
134    pub label: Option<Label>,
135}
136
137/// An deduction step.
138#[derive(Clone, Debug, PartialEq, Eq, Hash)]
139pub struct Deduction<Identifier, Int> {
140    /// The ID of the step.
141    pub constraint_id: ConstraintId,
142    /// The premises of the proof.
143    pub premises: Vec<IntAtomic<Identifier, Int>>,
144    /// The constraints to apply to derive the deduction. These should point to [`Inference`]s, but
145    /// the parser does not verify that.
146    pub sequence: Vec<ConstraintId>,
147}
148
149/// The conclusion of the proof. This is the final line, and a proof without a conclusion can be
150/// considered incomplete. All steps after the conclusion can be ignored.
151#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
152pub enum Conclusion<Identifier, Int> {
153    /// The problem is unsatisfiable.
154    Unsat,
155    /// The proof concludes the given dual bound.
156    DualBound(IntAtomic<Identifier, Int>),
157}
158
159/// An individual proof step from the proof.
160#[derive(Clone, Debug, PartialEq, Eq, Hash)]
161pub enum Step<Identifier, Int, Label> {
162    Inference(Inference<Identifier, Int, Label>),
163    Deduction(Deduction<Identifier, Int>),
164    Conclusion(Conclusion<Identifier, Int>),
165}
drcp_format/lib.rs

drcp_format/
lib.rs
