Merging upstream version 1.71.1+dfsg1.

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

2 files changed, 194 insertions, 0 deletions

diff --git a/vendor/varisat/src/variables/data.rs b/vendor/varisat/src/variables/data.rs
new file mode 100644
index 000000000..ea29e6280
--- /dev/null
+++ b/vendor/varisat/src/variables/data.rs
@@ -0,0 +1,70 @@
+//! Data associated with variables.
+
+/// Variable sampling mode.
+///
+/// This partitions all variables into three sets. Using these partitions it is possible to specify
+/// equivalence vs. equisatisfiability per variable. Let V be the set of all variables, S, W and H
+/// the sets of Sampling, Witness and Hidden variables. Let F be the input formula and G be the
+/// current formula. The following invariants are upheld:
+///
+///   * The formulas are always equisatisfiable:
+///     (∃ V) G ⇔ (∃ V) F
+///   * Restricted to the sampling variables they are equivalent:
+///     (∀ S) ((∃ V∖S) G ⇔ (∃ V∖S) F)
+///   * Restricted to the non-hidden variables the input formula is implied:
+///     (∀ V∖H) ((∃ H) G ⇒ (∃ H) F)
+///
+/// This ensures that the solver will be able to find and extend each satisfiable assignment of the
+/// sampling variables to an assignment that covers the witness variables.
+
+#[derive(Copy, Clone, PartialEq, Eq, Debug)]
+pub enum SamplingMode {
+    Sample,
+    Witness,
+    Hide,
+}
+
+/// Data associated with variables.
+///
+/// This is available for each _global_ variable, even if eliminated within the solver.
+#[derive(Clone)]
+pub struct VarData {
+    /// The variable's sampling mode.
+    pub sampling_mode: SamplingMode,
+    /// Whether the variable is forced by a unit clause.
+    ///
+    /// This is used to remember unit clauses after they are removed from the solver.
+    pub unit: Option<bool>,
+    /// True if there are no clauses containing this variable and other variables.
+    ///
+    /// This is the case if there are no clauses containing this variable or just a unit clause with
+    /// this variable.
+    pub isolated: bool,
+    /// True if this variable is part of the current assumptions.
+    pub assumed: bool,
+    /// Whether the global variable was deleted.
+    pub deleted: bool,
+}
+
+impl Default for VarData {
+    fn default() -> VarData {
+        VarData {
+            sampling_mode: SamplingMode::Hide,
+            unit: None,
+            isolated: true,
+            assumed: false,
+            deleted: true,
+        }
+    }
+}
+
+impl VarData {
+    /// Default variable data for a new user variable.
+    pub fn user_default() -> VarData {
+        VarData {
+            sampling_mode: SamplingMode::Sample,
+            deleted: false,
+            ..VarData::default()
+        }
+    }
+}
diff --git a/vendor/varisat/src/variables/var_map.rs b/vendor/varisat/src/variables/var_map.rs
new file mode 100644
index 000000000..730a6bf52
--- /dev/null
+++ b/vendor/varisat/src/variables/var_map.rs
@@ -0,0 +1,124 @@
+//! Mappings between variable names
+
+use varisat_formula::{lit::LitIdx, Var};
+
+const NO_VAR_IDX: LitIdx = Var::max_count() as LitIdx;
+
+/// A mapping from variables to variables.
+#[derive(Default)]
+pub struct VarMap {
+    mapping: Vec<LitIdx>,
+}
+
+impl VarMap {
+    /// Look up a variable in the mapping
+    pub fn get(&self, from: Var) -> Option<Var> {
+        match self.mapping.get(from.index()).cloned() {
+            Some(index) if index == NO_VAR_IDX => None,
+            Some(index) => Some(Var::from_index(index as usize)),
+            None => None,
+        }
+    }
+
+    /// Insert a new mapping.
+    ///
+    /// Note that the parameters are reversed from the usual order, to match the naming convention
+    /// used for maps.
+    ///
+    /// This has the precondition that `from` is not mapped.
+    pub fn insert(&mut self, into: Var, from: Var) {
+        if self.mapping.len() <= from.index() {
+            self.mapping.resize(from.index() + 1, NO_VAR_IDX);
+        }
+        debug_assert_eq!(self.mapping[from.index()], NO_VAR_IDX);
+        self.mapping[from.index()] = into.index() as LitIdx;
+    }
+
+    /// Remove a mapping.
+    ///
+    /// Does nothing if `from` is not mapped.
+    pub fn remove(&mut self, from: Var) {
+        if self.mapping.len() > from.index() {
+            self.mapping[from.index()] = NO_VAR_IDX;
+        }
+    }
+
+    /// One above the largest index that is mapped.
+    pub fn watermark(&self) -> usize {
+        self.mapping.len()
+    }
+}
+
+/// A bidirectional mapping between variables.
+///
+/// This is initialized with the identity mapping over all variables. It is possible to remove
+/// variables from this mapping on both sides.
+#[derive(Default)]
+pub struct VarBiMap {
+    fwd: VarMap,
+    bwd: VarMap,
+}
+
+impl VarBiMap {
+    /// Access the forward mapping.
+    pub fn fwd(&self) -> &VarMap {
+        &self.fwd
+    }
+
+    /// Access the backward mapping.
+    pub fn bwd(&self) -> &VarMap {
+        &self.bwd
+    }
+
+    /// Mutate the mapping in forward direction.
+    pub fn fwd_mut(&mut self) -> VarBiMapMut {
+        VarBiMapMut {
+            fwd: &mut self.fwd,
+            bwd: &mut self.bwd,
+        }
+    }
+
+    /// Mutate the mapping in backward direction.
+    pub fn bwd_mut(&mut self) -> VarBiMapMut {
+        VarBiMapMut {
+            fwd: &mut self.bwd,
+            bwd: &mut self.fwd,
+        }
+    }
+}
+
+/// Mutable view of a [`VarBiMap`].
+///
+/// Helper so `VarBiMap` mutating routines can work in both directions.
+pub struct VarBiMapMut<'a> {
+    fwd: &'a mut VarMap,
+    bwd: &'a mut VarMap,
+}
+
+impl<'a> VarBiMapMut<'a> {
+    /// Insert a new mapping.
+    ///
+    /// Note that the parameters are reversed from the usual order, to match the naming convention
+    /// used for maps.
+    ///
+    /// This has the precondition that `into` and `from` are not mapped.
+    pub fn insert(&mut self, into: Var, from: Var) {
+        self.fwd.insert(into, from);
+        self.bwd.insert(from, into);
+    }
+
+    /// Remove a mapping.
+    ///
+    /// Does nothing if `from` is not mapped.
+    ///
+    /// Returns the existing mapping if it was present.
+    pub fn remove(&mut self, from: Var) -> Option<Var> {
+        if let Some(into) = self.fwd.get(from) {
+            self.fwd.remove(from);
+            self.bwd.remove(into);
+            Some(into)
+        } else {
+            None
+        }
+    }
+}