cop/nano/
proof.rs

1use super::contrapositive::PreCp;
2use super::search::{Action, Context, OLitMat};
3use crate::offset::{Offset, Sub};
4use alloc::vec::Vec;
5use core::fmt::{self, Display};
6use core::ops::Neg;
7
8/// Offset contrapositive.
9pub type OContra<'t, P, C> = Offset<&'t PreCp<'t, crate::Lit<P, C, usize>, usize>>;
10
11/// A full proof for a litmat, including subproofs.
12pub enum Proof<'t, P, C> {
13    /// Lemma step
14    Lem,
15    /// Reduction step
16    Red,
17    /// Extension step, storing proofs for all items of the contrapositive
18    Ext(OContra<'t, P, C>, Vec<Self>),
19    /// Decomposition step, applicable if the litmat is a matrix
20    ///
21    /// This stores the index of the chosen clause in the matrix as well as
22    /// a proof for every litmat in the clause.
23    Dec(usize, Vec<Self>),
24}
25
26impl<'t, P, C> Proof<'t, P, C> {
27    /// Produce a tree-like proof from a series of proof search actions.
28    pub fn from_iter(iter: &mut impl Iterator<Item = Action<'t, P, C>>, off: &mut usize) -> Self {
29        match iter.next().unwrap() {
30            Action::Prove => Self::Lem,
31            Action::Reduce(_, _) => Self::Red,
32            Action::Extend(_, cs, skip) => {
33                let contra = &cs[skip];
34                let ocontra = Offset::new(*off, contra);
35                *off += contra.offset.map(|v| v + 1).unwrap_or(0);
36                let proofs = contra.into_iter().map(|_| Self::from_iter(iter, off));
37                Self::Ext(ocontra, proofs.collect())
38            }
39            Action::Decompose(mat, skip) => {
40                let cl = mat.into_iter().nth(skip).unwrap();
41                let lms = cl.map(|cl| &cl.1).into_iter();
42                let proofs = lms.map(|_| Self::from_iter(iter, off));
43                Self::Dec(skip, proofs.collect())
44            }
45        }
46    }
47
48    /// Given a proof and the litmat it proves, make it into something that can be displayed.
49    pub fn display(&self, lit: OLitMat<'t, P, C>) -> Disp<'_, 't, P, C> {
50        let depth = 0;
51        let proof = self;
52        Disp { depth, lit, proof }
53    }
54}
55
56impl<'t, P: Eq + Neg<Output = P> + Clone, C: Eq> Proof<'t, P, C> {
57    /// Check the proof.
58    pub fn check(
59        &self,
60        sub: &Sub<'t, C>,
61        lit: OLitMat<'t, P, C>,
62        mut ctx: Context<'t, P, C>,
63    ) -> bool {
64        use crate::LitMat::{Lit, Mat};
65        match (self, lit.transpose()) {
66            (Proof::Lem, Lit(lit)) => ctx.lemmas.iter().any(|lem| lit.eq_mod(sub, lem)),
67            (Proof::Red, Lit(lit)) => ctx.path.iter().any(|path| lit.neg_eq_mod(sub, path)),
68            (Proof::Ext(ocontra, proofs), Lit(lit)) => {
69                ctx.path.push(lit);
70                let rest = ocontra.into_iter();
71                rest.zip(proofs.iter()).all(|(clit, proof)| {
72                    let result = proof.check(sub, clit, ctx.clone());
73                    if let Lit(clit) = clit.transpose() {
74                        ctx.lemmas.push(clit);
75                    }
76                    result
77                }) && ocontra.map(|cp| cp.contra.lit).neg_eq_mod(sub, &lit)
78            }
79            (Proof::Dec(skip, proofs), Mat(mat)) => {
80                let cl = mat.into_iter().nth(*skip).unwrap();
81                let lms = cl.map(|cl| &cl.1).into_iter();
82                lms.zip(proofs.iter()).all(|(clit, proof)| {
83                    let result = proof.check(sub, clit, ctx.clone());
84                    if let Lit(clit) = clit.transpose() {
85                        ctx.lemmas.push(clit);
86                    }
87                    result
88                })
89            }
90            _ => panic!("proof step does not fit litmat"),
91        }
92    }
93}
94
95/// A proof together with additional information that can be displayed.
96pub struct Disp<'p, 't, P, C> {
97    depth: usize,
98    lit: OLitMat<'t, P, C>,
99    proof: &'p Proof<'t, P, C>,
100}
101
102impl<'p, 't, P: Display + Neg<Output = P> + Clone, C: Display> Display for Disp<'p, 't, P, C> {
103    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
104        write!(f, "{: <1$}", "", self.depth * 2)?;
105        write!(f, "{} ", self.lit)?;
106        use crate::LitMat::{Lit, Mat};
107        match (self.proof, self.lit.transpose()) {
108            (Proof::Lem, Lit(_)) => writeln!(f, "Lem")?,
109            (Proof::Red, Lit(_)) => writeln!(f, "Red")?,
110            (Proof::Ext(contra, proofs), Lit(lit)) => {
111                writeln!(f, "Ext {}{}", -lit.head().clone(), lit.args())?;
112                let depth = self.depth + 1;
113                for (proof, lit) in proofs.iter().zip(contra.into_iter()) {
114                    Self { depth, lit, proof }.fmt(f)?
115                }
116            }
117            (Proof::Dec(offset, proofs), Mat(mat)) => {
118                writeln!(f, "Dec {}", offset)?;
119                let depth = self.depth + 1;
120                let cl = mat.into_iter().nth(*offset).unwrap();
121                let lms = cl.map(|cl| &cl.1).into_iter();
122                for (proof, lit) in proofs.iter().zip(lms) {
123                    Self { depth, lit, proof }.fmt(f)?
124                }
125            }
126            _ => panic!("proof step does not fit litmat"),
127        }
128        Ok(())
129    }
130}
cop/nano/proof.rs

cop/nano/
proof.rs
