1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133

//! Proof transcripts.
use failure::Error;

use varisat_formula::{Lit, Var};

use crate::processing::{CheckedProofStep, CheckedSamplingMode, CheckedUserVar, CheckerData};

/// Step of a proof transcript.
///
/// The proof transcript contains the solver queries and results that correspond to a checked proof.
///
/// The transcript uses the same variable numbering as used for solver calls.
#[derive(Debug)]
pub enum ProofTranscriptStep<'a> {
    WitnessVar { var: Var },
    SampleVar { var: Var },
    HideVar { var: Var },
    ObserveInternalVar { var: Var },
    AddClause { clause: &'a [Lit] },
    Unsat,
    Model { assignment: &'a [Lit] },
    Assume { assumptions: &'a [Lit] },
    FailedAssumptions { failed_core: &'a [Lit] },
}

/// Implement to process transcript steps.
pub trait ProofTranscriptProcessor {
    /// Process a single proof transcript step.
    fn process_step(&mut self, step: &ProofTranscriptStep) -> Result<(), Error>;
}

/// Create a transcript from proof steps
#[derive(Default)]
pub(crate) struct Transcript {
    lit_buf: Vec<Lit>,
}

impl Transcript {
    /// If a checked proof step has a corresponding transcript step, return that.
    pub fn transcript_step(
        &mut self,
        step: &CheckedProofStep,
        data: CheckerData,
    ) -> Option<ProofTranscriptStep> {
        match step {
            CheckedProofStep::UserVar { var, user_var } => match user_var {
                None => Some(ProofTranscriptStep::HideVar {
                    var: data.user_from_proof_var(*var).unwrap(),
                }),

                Some(CheckedUserVar {
                    sampling_mode: CheckedSamplingMode::Sample,
                    new_var: true,
                    ..
                }) => None,

                Some(CheckedUserVar {
                    user_var,
                    sampling_mode: CheckedSamplingMode::Witness,
                    new_var: true,
                }) => Some(ProofTranscriptStep::ObserveInternalVar { var: *user_var }),

                Some(CheckedUserVar {
                    user_var,
                    sampling_mode: CheckedSamplingMode::Witness,
                    new_var: false,
                }) => Some(ProofTranscriptStep::WitnessVar { var: *user_var }),

                Some(CheckedUserVar {
                    user_var,
                    sampling_mode: CheckedSamplingMode::Sample,
                    new_var: false,
                }) => Some(ProofTranscriptStep::SampleVar { var: *user_var }),
            },
            CheckedProofStep::AddClause { clause, .. }
            | CheckedProofStep::DuplicatedClause { clause, .. }
            | CheckedProofStep::TautologicalClause { clause, .. } => {
                self.lit_buf.clear();
                self.lit_buf.extend(clause.iter().map(|&lit| {
                    lit.map_var(|var| {
                        data.user_from_proof_var(var)
                            .expect("hidden variable in clause")
                    })
                }));
                Some(ProofTranscriptStep::AddClause {
                    clause: &self.lit_buf,
                })
            }
            CheckedProofStep::AtClause { clause, .. } => {
                if clause.is_empty() {
                    Some(ProofTranscriptStep::Unsat)
                } else {
                    None
                }
            }
            CheckedProofStep::Model { assignment } => {
                self.lit_buf.clear();
                self.lit_buf.extend(assignment.iter().flat_map(|&lit| {
                    data.user_from_proof_var(lit.var())
                        .map(|var| var.lit(lit.is_positive()))
                }));
                Some(ProofTranscriptStep::Model {
                    assignment: &self.lit_buf,
                })
            }
            CheckedProofStep::Assumptions { assumptions } => {
                self.lit_buf.clear();
                self.lit_buf.extend(assumptions.iter().map(|&lit| {
                    lit.map_var(|var| {
                        data.user_from_proof_var(var)
                            .expect("hidden variable in assumptions")
                    })
                }));
                Some(ProofTranscriptStep::Assume {
                    assumptions: &self.lit_buf,
                })
            }
            CheckedProofStep::FailedAssumptions { failed_core, .. } => {
                self.lit_buf.clear();
                self.lit_buf.extend(failed_core.iter().map(|&lit| {
                    lit.map_var(|var| {
                        data.user_from_proof_var(var)
                            .expect("hidden variable in assumptions")
                    })
                }));
                Some(ProofTranscriptStep::FailedAssumptions {
                    failed_core: &self.lit_buf,
                })
            }
            _ => None,
        }
    }
}