1 files changed, 189 insertions, 0 deletions
diff --git a/vendor/varisat-checker/src/processing.rs b/vendor/varisat-checker/src/processing.rs
new file mode 100644
index 000000000..038406cca
--- /dev/null
+++ b/vendor/varisat-checker/src/processing.rs
@@ -0,0 +1,189 @@
+//! Processing of checked proof steps.
+use partial_ref::{partial, PartialRef};
+
+use anyhow::Error;
+use varisat_formula::{Lit, Var};
+
+use crate::{
+    context::{parts::*, Context},
+    transcript::{self, ProofTranscriptProcessor},
+    variables::SamplingMode,
+    CheckerError,
+};
+
+/// A single step of a proof.
+///
+/// Clauses are identified by a unique increasing id assigned by the checker. Whenever the literals
+/// of a clause are included in a step, they are sorted and free of duplicates.
+#[derive(Debug)]
+pub enum CheckedProofStep<'a> {
+    /// Updates the corresponding user variable for a proof variable.
+    UserVar {
+        var: Var,
+        user_var: Option<CheckedUserVar>,
+    },
+    /// A clause of the input formula.
+    AddClause { id: u64, clause: &'a [Lit] },
+    /// A duplicated clause of the input formula.
+    ///
+    /// The checker detects duplicated clauses and will use the same id for all copies. This also
+    /// applies to clauses of the input formula. This step allows proof processors to identify the
+    /// input formula's clauses by consecutive ids. When a duplicate clause is found, an id is
+    /// allocated and this step is emitted. The duplicated clause is not considered part of the
+    /// formula and the allocated id will not be used in any other steps.
+    DuplicatedClause {
+        id: u64,
+        same_as_id: u64,
+        clause: &'a [Lit],
+    },
+    /// A tautological clause of the input formula.
+    ///
+    /// Tautological clauses can be completely ignored. This step is only used to give an id to a
+    /// tautological input clause.
+    TautologicalClause { id: u64, clause: &'a [Lit] },
+    /// Addition of an asymmetric tautology (AT).
+    ///
+    /// A clause C is an asymmetric tautology wrt. a formula F, iff unit propagation in F with the
+    /// negated literals of C as unit clauses leads to a conflict. The `propagations` field contains
+    /// clauses in the order they became unit and as last element the clause that caused a conflict.
+    AtClause {
+        id: u64,
+        redundant: bool,
+        clause: &'a [Lit],
+        propagations: &'a [u64],
+    },
+    /// Deletion of a redundant clause.
+    DeleteClause { id: u64, clause: &'a [Lit] },
+    /// Deletion of a clause that is an asymmetric tautology w.r.t the remaining irredundant
+    /// clauses.
+    DeleteAtClause {
+        id: u64,
+        keep_as_redundant: bool,
+        clause: &'a [Lit],
+        propagations: &'a [u64],
+    },
+    /// Deletion of a resolution asymmetric tautology w.r.t the remaining irredundant caluses.
+    ///
+    /// The pivot is always a hidden variable.
+    DeleteRatClause {
+        id: u64,
+        keep_as_redundant: bool,
+        clause: &'a [Lit],
+        pivot: Lit,
+        propagations: &'a ResolutionPropagations,
+    },
+    /// Make a redundant clause irredundant.
+    MakeIrredundant { id: u64, clause: &'a [Lit] },
+    /// A (partial) assignment that satisfies all clauses and assumptions.
+    Model { assignment: &'a [Lit] },
+    /// Change the active set of assumptions.
+    Assumptions { assumptions: &'a [Lit] },
+    /// Subset of assumptions incompatible with the formula.
+    ///
+    /// The proof consists of showing that the negation of the assumptions is an AT wrt. the
+    /// formula.
+    FailedAssumptions {
+        failed_core: &'a [Lit],
+        propagations: &'a [u64],
+    },
+}
+
+/// Sampling mode of a user variable.
+#[derive(Debug)]
+pub enum CheckedSamplingMode {
+    Sample,
+    Witness,
+}
+
+/// Corresponding user variable for a proof variable.
+#[derive(Debug)]
+pub struct CheckedUserVar {
+    pub user_var: Var,
+    pub sampling_mode: CheckedSamplingMode,
+    pub new_var: bool,
+}
+
+/// A list of clauses to resolve and propagations to show that the resolvent is an AT.
+#[derive(Debug)]
+pub struct ResolutionPropagations {
+    // TODO implement ResolutionPropagations
+}
+
+/// Checker data available to proof processors.
+#[derive(Copy, Clone)]
+pub struct CheckerData<'a, 'b>(pub partial!('a Context<'b>, VariablesP));
+
+impl<'a, 'b> CheckerData<'a, 'b> {
+    /// User variable corresponding to proof variable.
+    ///
+    /// Returns `None` if the proof variable is an internal or hidden variable.
+    pub fn user_from_proof_var(self, proof_var: Var) -> Option<Var> {
+        let variables = self.0.part(VariablesP);
+        variables
+            .var_data
+            .get(proof_var.index())
+            .and_then(|var_data| {
+                var_data.user_var.or_else(|| {
+                    // This is needed as yet another workaround to enable independently loading the
+                    // initial formula and proof.
+                    // TODO can this be solved in a better way?
+                    if var_data.sampling_mode == SamplingMode::Sample {
+                        Some(proof_var)
+                    } else {
+                        None
+                    }
+                })
+            })
+    }
+}
+
+/// Implement to process proof steps.
+pub trait ProofProcessor {
+    fn process_step(&mut self, step: &CheckedProofStep, data: CheckerData) -> Result<(), Error>;
+}
+
+/// Registry of proof and transcript processors.
+#[derive(Default)]
+pub struct Processing<'a> {
+    /// Registered proof processors.
+    pub processors: Vec<&'a mut dyn ProofProcessor>,
+    /// Registered transcript processors.
+    pub transcript_processors: Vec<&'a mut dyn ProofTranscriptProcessor>,
+    /// Proof step to transcript step conversion.
+    transcript: transcript::Transcript,
+}
+
+impl<'a> Processing<'a> {
+    /// Process a single step
+    pub fn step<'b>(
+        &mut self,
+        step: &CheckedProofStep<'b>,
+        data: CheckerData,
+    ) -> Result<(), CheckerError> {
+        for processor in self.processors.iter_mut() {
+            if let Err(err) = processor.process_step(step, data) {
+                return Err(CheckerError::ProofProcessorError { cause: err });
+            }
+        }
+        if !self.transcript_processors.is_empty() {
+            if let Some(transcript_step) = self.transcript.transcript_step(step, data) {
+                for processor in self.transcript_processors.iter_mut() {
+                    if let Err(err) = processor.process_step(&transcript_step) {
+                        return Err(CheckerError::ProofProcessorError { cause: err });
+                    }
+                }
+            }
+        }
+
+        Ok(())
+    }
+}
+
+/// Process a single step
+pub fn process_step<'a, 'b>(
+    mut ctx: partial!(Context<'a>, mut ProcessingP<'a>, VariablesP),
+    step: &CheckedProofStep<'b>,
+) -> Result<(), CheckerError> {
+    let (processing, mut ctx) = ctx.split_part_mut(ProcessingP);
+    processing.step(step, CheckerData(ctx.borrow()))
+}