Merging upstream version 1.71.1+dfsg1.

Signed-off-by: Daniel Baumann <daniel.baumann@progress-linux.org>

2 files changed, 213 insertions, 0 deletions

diff --git a/vendor/varisat/src/proof/drat.rs b/vendor/varisat/src/proof/drat.rs
new file mode 100644
index 000000000..76382fab3
--- /dev/null
+++ b/vendor/varisat/src/proof/drat.rs
@@ -0,0 +1,85 @@
+use std::io::{self, Write};
+
+use varisat_formula::Lit;
+use varisat_internal_proof::ProofStep;
+
+/// Prepares a proof step for DRAT writing
+fn drat_step(
+    step: &ProofStep,
+    mut emit_drat_step: impl FnMut(bool, &[Lit]) -> io::Result<()>,
+) -> io::Result<()> {
+    match step {
+        ProofStep::AtClause { clause, .. } => {
+            emit_drat_step(true, &clause)?;
+        }
+        ProofStep::UnitClauses { units } => {
+            for &(unit, _hash) in units.iter() {
+                emit_drat_step(true, &[unit])?;
+            }
+        }
+        ProofStep::DeleteClause { clause, .. } => {
+            emit_drat_step(false, &clause[..])?;
+        }
+        ProofStep::SolverVarName { .. }
+        | ProofStep::UserVarName { .. }
+        | ProofStep::DeleteVar { .. }
+        | ProofStep::ChangeSamplingMode { .. }
+        | ProofStep::ChangeHashBits { .. }
+        | ProofStep::Model { .. }
+        | ProofStep::End => (),
+        ProofStep::AddClause { .. } => {
+            // TODO allow error handling here?
+            panic!("incremental clause additions not supported by DRAT proofs");
+        }
+        ProofStep::Assumptions { .. } | ProofStep::FailedAssumptions { .. } => {
+            // TODO allow error handling here?
+            panic!("assumptions not supported by DRAT proofs");
+        }
+    }
+
+    Ok(())
+}
+
+/// Writes a proof step in DRAT format
+pub fn write_step<'s>(target: &mut impl Write, step: &'s ProofStep<'s>) -> io::Result<()> {
+    drat_step(step, |add, clause| {
+        if !add {
+            target.write_all(b"d ")?;
+        }
+        write_literals(target, &clause[..])?;
+        Ok(())
+    })
+}
+
+/// Writes a proof step in binary DRAT format
+pub fn write_binary_step<'s>(target: &mut impl Write, step: &'s ProofStep<'s>) -> io::Result<()> {
+    drat_step(step, |add, clause| {
+        if add {
+            target.write_all(b"a")?;
+        } else {
+            target.write_all(b"d")?;
+        }
+        write_binary_literals(target, &clause[..])?;
+        Ok(())
+    })
+}
+
+/// Writes the literals of a clause for a step in a DRAT proof.
+fn write_literals(target: &mut impl Write, literals: &[Lit]) -> io::Result<()> {
+    for &lit in literals {
+        itoa::write(&mut *target, lit.to_dimacs())?;
+        target.write_all(b" ")?;
+    }
+    target.write_all(b"0\n")?;
+    Ok(())
+}
+
+/// Writes the literals of a clause for a step in a binary DRAT proof.
+fn write_binary_literals(target: &mut impl Write, literals: &[Lit]) -> io::Result<()> {
+    for &lit in literals {
+        let drat_code = lit.code() as u64 + 2;
+        leb128::write::unsigned(target, drat_code)?;
+    }
+    target.write_all(&[0])?;
+    Ok(())
+}
diff --git a/vendor/varisat/src/proof/map_step.rs b/vendor/varisat/src/proof/map_step.rs
new file mode 100644
index 000000000..0c08e6510
--- /dev/null
+++ b/vendor/varisat/src/proof/map_step.rs
@@ -0,0 +1,128 @@
+//! Maps literals and hashes of clause steps between the solver and the checker.
+
+use varisat_formula::{Lit, Var};
+
+use super::{ClauseHash, ProofStep};
+
+/// Maps literals and hashes of clause steps between the solver and the checker.
+#[derive(Default)]
+pub struct MapStep {
+    lit_buf: Vec<Lit>,
+    hash_buf: Vec<ClauseHash>,
+    unit_buf: Vec<(Lit, ClauseHash)>,
+}
+
+impl MapStep {
+    pub fn map_lits(&mut self, lits: &[Lit], map_var: impl Fn(Var) -> Var) -> &[Lit] {
+        let map_var_ref = &map_var;
+        self.lit_buf.clear();
+        self.lit_buf
+            .extend(lits.iter().map(|lit| lit.map_var(map_var_ref)));
+        &self.lit_buf
+    }
+
+    pub fn map<'s, 'a, 'b>(
+        &'a mut self,
+        step: &ProofStep<'b>,
+        map_var: impl Fn(Var) -> Var,
+        map_hash: impl Fn(ClauseHash) -> ClauseHash,
+    ) -> ProofStep<'s>
+    where
+        'a: 's,
+        'b: 's,
+    {
+        let map_var_ref = &map_var;
+        let map_lit = |lit: Lit| lit.map_var(map_var_ref);
+        match *step {
+            ProofStep::AddClause { clause } => {
+                self.lit_buf.clear();
+                self.lit_buf.extend(clause.iter().cloned().map(map_lit));
+                ProofStep::AddClause {
+                    clause: &self.lit_buf,
+                }
+            }
+
+            ProofStep::AtClause {
+                redundant,
+                clause,
+                propagation_hashes,
+            } => {
+                self.lit_buf.clear();
+                self.lit_buf.extend(clause.iter().cloned().map(map_lit));
+                self.hash_buf.clear();
+                self.hash_buf
+                    .extend(propagation_hashes.iter().cloned().map(map_hash));
+                ProofStep::AtClause {
+                    redundant,
+                    clause: &self.lit_buf,
+                    propagation_hashes: &self.hash_buf,
+                }
+            }
+
+            ProofStep::UnitClauses { units } => {
+                self.unit_buf.clear();
+                self.unit_buf.extend(
+                    units
+                        .iter()
+                        .map(|&(lit, hash)| (map_lit(lit), map_hash(hash))),
+                );
+                ProofStep::UnitClauses {
+                    units: &self.unit_buf,
+                }
+            }
+
+            ProofStep::DeleteClause { clause, proof } => {
+                self.lit_buf.clear();
+                self.lit_buf.extend(clause.iter().cloned().map(map_lit));
+                ProofStep::DeleteClause {
+                    clause: &self.lit_buf,
+                    proof,
+                }
+            }
+
+            ProofStep::Model { assignment } => {
+                self.lit_buf.clear();
+                self.lit_buf.extend(assignment.iter().cloned().map(map_lit));
+                ProofStep::Model {
+                    assignment: &self.lit_buf,
+                }
+            }
+
+            ProofStep::Assumptions { assumptions } => {
+                self.lit_buf.clear();
+                self.lit_buf
+                    .extend(assumptions.iter().cloned().map(map_lit));
+                ProofStep::Assumptions {
+                    assumptions: &self.lit_buf,
+                }
+            }
+
+            ProofStep::FailedAssumptions {
+                failed_core,
+                propagation_hashes,
+            } => {
+                self.lit_buf.clear();
+                self.lit_buf
+                    .extend(failed_core.iter().cloned().map(map_lit));
+                self.hash_buf.clear();
+                self.hash_buf
+                    .extend(propagation_hashes.iter().cloned().map(map_hash));
+                ProofStep::FailedAssumptions {
+                    failed_core: &self.lit_buf,
+                    propagation_hashes: &self.hash_buf,
+                }
+            }
+
+            ProofStep::ChangeHashBits { .. } | ProofStep::End => *step,
+
+            ProofStep::SolverVarName { .. }
+            | ProofStep::UserVarName { .. }
+            | ProofStep::DeleteVar { .. }
+            | ProofStep::ChangeSamplingMode { .. } => {
+                // while these steps do contain variables, they are used to update the mapping, so
+                // they shouldn't be mapped themselves.
+                *step
+            }
+        }
+    }
+}