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

//! Mappings between variable names

use varisat_formula::lit::LitIdx;
use varisat_formula::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
        }
    }
}