varisat 0.2.2

A CDCL based SAT solver (library)
Documentation 
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

//! 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
        }
    }
}