drcp_format/writer/
mod.rs

1//! Implements the writing of DRCP files.
2//!
3//! # Example
4//! ```
5//! use std::num::NonZero;
6//!
7//! use drcp_format::Conclusion;
8//! use drcp_format::Deduction;
9//! use drcp_format::Inference;
10//! use drcp_format::IntAtomic;
11//! use drcp_format::IntComparison::*;
12//! use drcp_format::writer::ProofWriter;
13//!
14//! let mut buffer = Vec::new();
15//! let mut writer = ProofWriter::new(&mut buffer);
16//!
17//! writer
18//!     .log_inference(Inference {
19//!         constraint_id: NonZero::new(2).unwrap(),
20//!         premises: vec![
21//!             IntAtomic::new("x1", GreaterEqual, 1),
22//!             IntAtomic::new("x2", LessEqual, 3),
23//!         ],
24//!         consequent: Some(IntAtomic::new("x3", Equal, -3)),
25//!         generated_by: Some(NonZero::new(1).unwrap()),
26//!         label: Some("inf_name"),
27//!     })
28//!     .unwrap();
29//!
30//! writer
31//!     .log_deduction(Deduction {
32//!         constraint_id: NonZero::new(3).unwrap(),
33//!         premises: vec![
34//!             IntAtomic::new("x1", GreaterEqual, 1),
35//!             IntAtomic::new("x2", GreaterEqual, 4),
36//!         ],
37//!         sequence: vec![NonZero::new(2).unwrap()],
38//!     })
39//!     .unwrap();
40//!
41//! writer.log_conclusion::<&str>(Conclusion::Unsat).unwrap();
42//!
43//! let proof_string = String::from_utf8(buffer).expect("valid utf8");
44//! let expected = r#"
45//! a 1 [x1 >= 1]
46//! a 2 [x2 <= 3]
47//! a 3 [x3 == -3]
48//! i 2 1 2 0 3 c:1 l:inf_name
49//! n 3 1 -2 0 2
50//! c UNSAT
51//! "#;
52//!
53//! assert_eq!(expected.trim(), proof_string.trim());
54//! ```
55
56use std::collections::BTreeMap;
57use std::fmt::Display;
58use std::io::Write;
59use std::num::NonZero;
60
61use crate::Conclusion;
62use crate::Deduction;
63use crate::Inference;
64use crate::IntAtomic;
65use crate::IntValue;
66
67/// Write a DRCP proof to some sink.
68///
69/// See the module documentation of [`crate::writer`] for examples on how to use the
70/// [`ProofWriter`].
71#[derive(Debug)]
72pub struct ProofWriter<W, Int> {
73    /// The writer to the underlying sink.
74    writer: W,
75
76    /// A container for all the literals which are seen in the proof. Unseen literals need not be
77    /// defined in the literal definition file.
78    defined_atomics: BTreeMap<IntAtomic<Box<str>, Int>, NonZero<i32>>,
79
80    /// The next ID to use when a new atomic needs to be defined.
81    next_atomic_id: i32,
82}
83
84impl<W: Write, Int> ProofWriter<W, Int> {
85    /// Create a new proof writer which writes the proof to an underlying sink implementing
86    /// [`Write`].
87    pub fn new(writer: W) -> Self {
88        Self {
89            writer,
90            defined_atomics: BTreeMap::default(),
91            next_atomic_id: 0,
92        }
93    }
94}
95
96impl<W: Write, Int: IntValue> ProofWriter<W, Int> {
97    /// Write a deduction step.
98    ///
99    /// The `propagation_hints` can be optionally given to indicate which previously derived facts
100    /// should be applied to derive the conflict.
101    ///
102    /// This function wraps an IO operation, which is why it can fail with an IO error.
103    pub fn log_deduction<Identifier: Into<Box<str>>>(
104        &mut self,
105        deduction: Deduction<Identifier, Int>,
106    ) -> std::io::Result<()> {
107        let Deduction {
108            constraint_id,
109            premises,
110            sequence,
111        } = deduction;
112
113        let premises = premises
114            .into_iter()
115            .map(|premise| self.get_atomic_code(premise))
116            .collect::<Result<Vec<_>, _>>()?;
117
118        write!(&mut self.writer, "n {constraint_id}")?;
119
120        for code in premises {
121            write!(&mut self.writer, " {code}")?;
122        }
123
124        write!(&mut self.writer, " 0")?;
125
126        for constraint_id in sequence {
127            write!(&mut self.writer, " {constraint_id}")?;
128        }
129
130        writeln!(&mut self.writer)?;
131
132        Ok(())
133    }
134
135    /// Log an inference step.
136    ///
137    /// Besides premises and a consequent, an inference step can optionally include hints regarding
138    /// the constraint that generated the inference, and the label of the filtering algorithm which
139    /// identified the inference.
140    ///
141    /// If there is no consequent, then the format prescribes that the consequent is false, so that
142    /// the premises form a nogood.
143    ///
144    /// This function wraps an IO operation, which is why it can fail with an IO error.
145    pub fn log_inference<Identifier: Into<Box<str>>, Label: Display>(
146        &mut self,
147        inference: Inference<Identifier, Int, Label>,
148    ) -> std::io::Result<()> {
149        let Inference {
150            constraint_id,
151            premises,
152            consequent,
153            generated_by,
154            label,
155        } = inference;
156
157        let premises = premises
158            .into_iter()
159            .map(|premise| self.get_atomic_code(premise))
160            .collect::<Result<Vec<_>, _>>()?;
161
162        let consequent = consequent
163            .map(|premise| self.get_atomic_code(premise))
164            .transpose()?;
165
166        write!(&mut self.writer, "i {constraint_id}")?;
167
168        for code in premises {
169            write!(&mut self.writer, " {code}")?;
170        }
171
172        write!(&mut self.writer, " 0")?;
173
174        if let Some(code) = consequent {
175            write!(&mut self.writer, " {code}")?;
176        }
177
178        if let Some(generated_by) = generated_by {
179            write!(&mut self.writer, " c:{generated_by}")?;
180        }
181
182        if let Some(label) = label {
183            write!(&mut self.writer, " l:{label}")?;
184        }
185
186        writeln!(&mut self.writer)?;
187
188        Ok(())
189    }
190
191    /// Conclude the proof with a conclusion.
192    pub fn log_conclusion<Identifier: Into<Box<str>>>(
193        &mut self,
194        conclusion: Conclusion<Identifier, Int>,
195    ) -> std::io::Result<()> {
196        match conclusion {
197            Conclusion::Unsat => writeln!(&mut self.writer, "c UNSAT"),
198            Conclusion::DualBound(atomic) => {
199                let code = self.get_atomic_code(atomic)?;
200                writeln!(&mut self.writer, "c {code}")
201            }
202        }
203    }
204
205    fn get_atomic_code<Identifier: Into<Box<str>>>(
206        &mut self,
207        atomic: IntAtomic<Identifier, Int>,
208    ) -> std::io::Result<NonZero<i32>> {
209        let key = IntAtomic {
210            name: atomic.name.into(),
211            comparison: atomic.comparison,
212            value: atomic.value,
213        };
214
215        if !self.defined_atomics.contains_key(&key) {
216            self.next_atomic_id += 1;
217
218            let id = NonZero::new(self.next_atomic_id)
219                .expect("next_atomic_id starts at 0, and is incremented, so it can never be 0");
220
221            let _ = self.defined_atomics.insert(key.clone(), id);
222            let _ = self.defined_atomics.insert(!key.clone(), -id);
223
224            writeln!(&mut self.writer, "a {id} {key}")?;
225        }
226
227        Ok(self.defined_atomics[&key])
228    }
229}
230
231#[cfg(test)]
232mod tests {
233    use IntComparison::*;
234
235    use super::*;
236    use crate::ConstraintId;
237    use crate::IntComparison;
238    use crate::Step;
239
240    const TEST_ID: ConstraintId = NonZero::new(5).unwrap();
241
242    #[test]
243    fn write_basic_inference() {
244        test_step_serialization(
245            Step::Inference(Inference {
246                constraint_id: TEST_ID,
247                premises: vec![atomic("x1", GreaterEqual, 1), atomic("x2", LessEqual, 3)],
248                consequent: Some(atomic("x3", Equal, -3)),
249                generated_by: None,
250                label: None,
251            }),
252            vec![
253                "a 1 [x1 >= 1]",
254                "a 2 [x2 <= 3]",
255                "a 3 [x3 == -3]",
256                "i 5 1 2 0 3",
257            ],
258        );
259    }
260
261    #[test]
262    fn write_basic_deduction_without_sequence() {
263        test_step_serialization(
264            Step::Deduction(Deduction {
265                constraint_id: TEST_ID,
266                premises: vec![atomic("x1", GreaterEqual, 1), atomic("x2", LessEqual, 3)],
267                sequence: vec![],
268            }),
269            vec!["a 1 [x1 >= 1]", "a 2 [x2 <= 3]", "n 5 1 2 0"],
270        );
271    }
272
273    #[test]
274    fn write_basic_deduction_with_sequence() {
275        test_step_serialization(
276            Step::Deduction(Deduction {
277                constraint_id: TEST_ID,
278                premises: vec![atomic("x1", GreaterEqual, 1), atomic("x2", LessEqual, 3)],
279                sequence: vec![
280                    NonZero::new(1).unwrap(),
281                    NonZero::new(3).unwrap(),
282                    NonZero::new(4).unwrap(),
283                    NonZero::new(2).unwrap(),
284                ],
285            }),
286            vec!["a 1 [x1 >= 1]", "a 2 [x2 <= 3]", "n 5 1 2 0 1 3 4 2"],
287        );
288    }
289
290    #[test]
291    fn write_conclusion_unsat() {
292        test_step_serialization(Step::Conclusion(Conclusion::Unsat), vec!["c UNSAT"]);
293    }
294
295    #[test]
296    fn write_conclusion_dual_bound() {
297        test_step_serialization(
298            Step::Conclusion(Conclusion::DualBound(atomic("x1", GreaterEqual, 100))),
299            vec!["a 1 [x1 >= 100]", "c 1"],
300        );
301    }
302
303    fn atomic(name: &str, comparison: IntComparison, value: i32) -> IntAtomic<&str, i32> {
304        IntAtomic {
305            name,
306            comparison,
307            value,
308        }
309    }
310
311    fn test_step_serialization(step: Step<&str, i32, &str>, lines: Vec<&str>) {
312        let mut buffer = Vec::new();
313
314        {
315            let mut writer = ProofWriter::new(&mut buffer);
316
317            match step {
318                Step::Inference(inference) => writer.log_inference(inference).unwrap(),
319                Step::Deduction(deduction) => writer.log_deduction(deduction).unwrap(),
320                Step::Conclusion(conclusion) => writer.log_conclusion(conclusion).unwrap(),
321            }
322        }
323
324        let actual = String::from_utf8(buffer).expect("valid utf8");
325        let expected = lines.join("\n");
326        assert_eq!(expected.trim(), actual.trim());
327    }
328}
drcp_format/writer/mod.rs

drcp_format/writer/
mod.rs
