varisat_checker/
transcript.rs

1//! Proof transcripts.
2use anyhow::Error;
3
4use varisat_formula::{Lit, Var};
5
6use crate::processing::{CheckedProofStep, CheckedSamplingMode, CheckedUserVar, CheckerData};
7
8/// Step of a proof transcript.
9///
10/// The proof transcript contains the solver queries and results that correspond to a checked proof.
11///
12/// The transcript uses the same variable numbering as used for solver calls.
13#[derive(Debug)]
14pub enum ProofTranscriptStep<'a> {
15    WitnessVar { var: Var },
16    SampleVar { var: Var },
17    HideVar { var: Var },
18    ObserveInternalVar { var: Var },
19    AddClause { clause: &'a [Lit] },
20    Unsat,
21    Model { assignment: &'a [Lit] },
22    Assume { assumptions: &'a [Lit] },
23    FailedAssumptions { failed_core: &'a [Lit] },
24}
25
26/// Implement to process transcript steps.
27pub trait ProofTranscriptProcessor {
28    /// Process a single proof transcript step.
29    fn process_step(&mut self, step: &ProofTranscriptStep) -> Result<(), Error>;
30}
31
32/// Create a transcript from proof steps
33#[derive(Default)]
34pub(crate) struct Transcript {
35    lit_buf: Vec<Lit>,
36}
37
38impl Transcript {
39    /// If a checked proof step has a corresponding transcript step, return that.
40    pub fn transcript_step(
41        &mut self,
42        step: &CheckedProofStep,
43        data: CheckerData,
44    ) -> Option<ProofTranscriptStep> {
45        match step {
46            CheckedProofStep::UserVar { var, user_var } => match user_var {
47                None => Some(ProofTranscriptStep::HideVar {
48                    var: data.user_from_proof_var(*var).unwrap(),
49                }),
50
51                Some(CheckedUserVar {
52                    sampling_mode: CheckedSamplingMode::Sample,
53                    new_var: true,
54                    ..
55                }) => None,
56
57                Some(CheckedUserVar {
58                    user_var,
59                    sampling_mode: CheckedSamplingMode::Witness,
60                    new_var: true,
61                }) => Some(ProofTranscriptStep::ObserveInternalVar { var: *user_var }),
62
63                Some(CheckedUserVar {
64                    user_var,
65                    sampling_mode: CheckedSamplingMode::Witness,
66                    new_var: false,
67                }) => Some(ProofTranscriptStep::WitnessVar { var: *user_var }),
68
69                Some(CheckedUserVar {
70                    user_var,
71                    sampling_mode: CheckedSamplingMode::Sample,
72                    new_var: false,
73                }) => Some(ProofTranscriptStep::SampleVar { var: *user_var }),
74            },
75            CheckedProofStep::AddClause { clause, .. }
76            | CheckedProofStep::DuplicatedClause { clause, .. }
77            | CheckedProofStep::TautologicalClause { clause, .. } => {
78                self.lit_buf.clear();
79                self.lit_buf.extend(clause.iter().map(|&lit| {
80                    lit.map_var(|var| {
81                        data.user_from_proof_var(var)
82                            .expect("hidden variable in clause")
83                    })
84                }));
85                Some(ProofTranscriptStep::AddClause {
86                    clause: &self.lit_buf,
87                })
88            }
89            CheckedProofStep::AtClause { clause, .. } => {
90                if clause.is_empty() {
91                    Some(ProofTranscriptStep::Unsat)
92                } else {
93                    None
94                }
95            }
96            CheckedProofStep::Model { assignment } => {
97                self.lit_buf.clear();
98                self.lit_buf.extend(assignment.iter().flat_map(|&lit| {
99                    data.user_from_proof_var(lit.var())
100                        .map(|var| var.lit(lit.is_positive()))
101                }));
102                Some(ProofTranscriptStep::Model {
103                    assignment: &self.lit_buf,
104                })
105            }
106            CheckedProofStep::Assumptions { assumptions } => {
107                self.lit_buf.clear();
108                self.lit_buf.extend(assumptions.iter().map(|&lit| {
109                    lit.map_var(|var| {
110                        data.user_from_proof_var(var)
111                            .expect("hidden variable in assumptions")
112                    })
113                }));
114                Some(ProofTranscriptStep::Assume {
115                    assumptions: &self.lit_buf,
116                })
117            }
118            CheckedProofStep::FailedAssumptions { failed_core, .. } => {
119                self.lit_buf.clear();
120                self.lit_buf.extend(failed_core.iter().map(|&lit| {
121                    lit.map_var(|var| {
122                        data.user_from_proof_var(var)
123                            .expect("hidden variable in assumptions")
124                    })
125                }));
126                Some(ProofTranscriptStep::FailedAssumptions {
127                    failed_core: &self.lit_buf,
128                })
129            }
130            _ => None,
131        }
132    }
133}
varisat_checker/transcript.rs

varisat_checker/
transcript.rs
