summaryrefslogtreecommitdiffstats
path: root/vendor/varisat/src/clause/alloc.rs
blob: d395140405fbab3206655471f5cba94ffb122159 (plain)
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
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
//! Clause allocator.
use std::{mem::transmute, slice};

use varisat_formula::{lit::LitIdx, Lit};

use super::{Clause, ClauseHeader, HEADER_LEN};

/// Integer type used to store offsets into [`ClauseAlloc`]'s memory.
type ClauseOffset = u32;

/// Bump allocator for clause storage.
///
/// Clauses are allocated from a single continuous buffer. Clauses cannot be freed individually. To
/// reclaim space from deleted clauses, a new `ClauseAlloc` is created and the remaining clauses are
/// copied over.
///
/// When the `ClauseAlloc`'s buffer is full, it is reallocated using the growing strategy of
/// [`Vec`]. External references ([`ClauseRef`]) store an offset into the `ClauseAlloc`'s memory and
/// remaind valid when the buffer is grown. Clauses are aligned and the offset represents a multiple
/// of the alignment size. This allows using 32-bit offsets while still supporting up to 16GB of
/// clauses.
#[derive(Default)]
pub struct ClauseAlloc {
    buffer: Vec<LitIdx>,
}

impl ClauseAlloc {
    /// Create an emtpy clause allocator.
    pub fn new() -> ClauseAlloc {
        ClauseAlloc::default()
    }

    /// Create a clause allocator with preallocated capacity.
    pub fn with_capacity(capacity: usize) -> ClauseAlloc {
        ClauseAlloc {
            buffer: Vec::with_capacity(capacity),
        }
    }

    /// Allocate space for and add a new clause.
    ///
    /// Clauses have a minimal size of 3, as binary and unit clauses are handled separately. This is
    /// enforced on the ClauseAlloc level to safely avoid extra bound checks when accessing the
    /// initial literals of a clause.
    ///
    /// The size of the header will be set to the size of the given slice. The returned
    /// [`ClauseRef`] can be used to access the new clause.
    pub fn add_clause(&mut self, mut header: ClauseHeader, lits: &[Lit]) -> ClauseRef {
        let offset = self.buffer.len();

        assert!(
            lits.len() >= 3,
            "ClauseAlloc can only store ternary and larger clauses"
        );

        // TODO Maybe let the caller handle this?
        assert!(
            offset <= (ClauseRef::max_offset() as usize),
            "Exceeded ClauseAlloc's maximal buffer size"
        );

        header.set_len(lits.len());

        self.buffer.extend_from_slice(&header.data);

        let lit_idx_slice = unsafe {
            // This is safe as Lit and LitIdx have the same representation
            slice::from_raw_parts(lits.as_ptr() as *const LitIdx, lits.len())
        };

        self.buffer.extend_from_slice(lit_idx_slice);

        ClauseRef {
            offset: offset as ClauseOffset,
        }
    }

    /// Access the header of a clause.
    pub fn header(&self, cref: ClauseRef) -> &ClauseHeader {
        let offset = cref.offset as usize;
        assert!(
            offset as usize + HEADER_LEN <= self.buffer.len(),
            "ClauseRef out of bounds"
        );
        unsafe { self.header_unchecked(cref) }
    }

    /// Mutate the header of a clause.
    pub fn header_mut(&mut self, cref: ClauseRef) -> &mut ClauseHeader {
        let offset = cref.offset as usize;
        assert!(
            offset as usize + HEADER_LEN <= self.buffer.len(),
            "ClauseRef out of bounds"
        );
        unsafe { self.header_unchecked_mut(cref) }
    }

    unsafe fn header_unchecked(&self, cref: ClauseRef) -> &ClauseHeader {
        let offset = cref.offset as usize;
        let header_pointer = self.buffer.as_ptr().add(offset) as *const ClauseHeader;
        &*header_pointer
    }

    /// Mutate the header of a clause without bound checks.
    pub unsafe fn header_unchecked_mut(&mut self, cref: ClauseRef) -> &mut ClauseHeader {
        let offset = cref.offset as usize;
        let header_pointer = self.buffer.as_mut_ptr().add(offset) as *mut ClauseHeader;
        &mut *header_pointer
    }

    /// Access a clause.
    pub fn clause(&self, cref: ClauseRef) -> &Clause {
        let header = self.header(cref);
        let len = header.len();

        // Even on 32 bit systems these additions can't overflow as we never create clause refs with
        // an offset larger than ClauseRef::max_offset()

        let lit_offset = cref.offset as usize + HEADER_LEN;
        let lit_end = lit_offset + len;
        assert!(lit_end <= self.buffer.len(), "ClauseRef out of bounds");
        unsafe { self.clause_with_len_unchecked(cref, len) }
    }

    /// Mutate a clause.
    pub fn clause_mut(&mut self, cref: ClauseRef) -> &mut Clause {
        let header = self.header(cref);
        let len = header.len();

        // Even on 32 bit systems these additions can't overflow as we never create clause refs with
        // an offset larger than ClauseRef::max_offset()

        let lit_offset = cref.offset as usize + HEADER_LEN;
        let lit_end = lit_offset + len;
        assert!(lit_end <= self.buffer.len(), "ClauseRef out of bounds");
        unsafe { self.clause_with_len_unchecked_mut(cref, len) }
    }

    /// Mutate the literals of a clause without bound checks.
    pub unsafe fn lits_ptr_mut_unchecked(&mut self, cref: ClauseRef) -> *mut Lit {
        let offset = cref.offset as usize;
        self.buffer.as_ptr().add(offset + HEADER_LEN) as *mut Lit
    }

    /// Perform a manual bound check on a ClauseRef assuming a given clause length.
    pub fn check_bounds(&self, cref: ClauseRef, len: usize) {
        // Even on 32 bit systems these additions can't overflow as we never create clause refs with
        // an offset larger than ClauseRef::max_offset()

        let lit_offset = cref.offset as usize + HEADER_LEN;
        let lit_end = lit_offset + len;
        assert!(lit_end <= self.buffer.len(), "ClauseRef out of bounds");
    }

    unsafe fn clause_with_len_unchecked(&self, cref: ClauseRef, len: usize) -> &Clause {
        let offset = cref.offset as usize;
        #[allow(clippy::transmute_ptr_to_ptr)]
        transmute::<&[LitIdx], &Clause>(slice::from_raw_parts(
            self.buffer.as_ptr().add(offset),
            len + HEADER_LEN,
        ))
    }

    unsafe fn clause_with_len_unchecked_mut(&mut self, cref: ClauseRef, len: usize) -> &mut Clause {
        let offset = cref.offset as usize;
        #[allow(clippy::transmute_ptr_to_ptr)]
        transmute::<&mut [LitIdx], &mut Clause>(slice::from_raw_parts_mut(
            self.buffer.as_mut_ptr().add(offset),
            len + HEADER_LEN,
        ))
    }

    /// Current buffer size in multiples of [`LitIdx`].
    pub fn buffer_size(&self) -> usize {
        self.buffer.len()
    }
}

/// Compact reference to a clause.
///
/// Used with [`ClauseAlloc`] to access the clause.
#[derive(Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Debug)]
pub struct ClauseRef {
    offset: ClauseOffset,
}

impl ClauseRef {
    /// The largest offset supported by the ClauseAlloc
    const fn max_offset() -> ClauseOffset {
        // Make sure we can savely add a length to an offset without overflowing usize
        ((usize::max_value() >> 1) & (ClauseOffset::max_value() as usize)) as ClauseOffset
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    use varisat_formula::{cnf::strategy::*, CnfFormula, ExtendFormula};

    use proptest::*;

    proptest! {
        #[test]
        fn roundtrip_from_cnf_formula(input in cnf_formula(1..100usize, 0..1000, 3..30)) {

            let mut clause_alloc = ClauseAlloc::new();
            let mut clause_refs = vec![];

            for clause_lits in input.iter() {
                let header = ClauseHeader::new();
                clause_refs.push(clause_alloc.add_clause(header, clause_lits));
            }

            let mut recovered = CnfFormula::new();

            for cref in clause_refs {
                let clause = clause_alloc.clause(cref);
                prop_assert_eq!(clause.header().len(), clause.lits().len());
                recovered.add_clause(clause.lits());
            }

            // Ignore difference caused by unused vars
            recovered.set_var_count(input.var_count());

            prop_assert_eq!(input, recovered);
        }

        #[test]
        fn clause_mutation(input in cnf_formula(1..100usize, 0..1000, 3..30)) {

            let mut clause_alloc = ClauseAlloc::new();
            let mut clause_refs = vec![];

            for clause_lits in input.iter() {
                let header = ClauseHeader::new();
                clause_refs.push(clause_alloc.add_clause(header, clause_lits));
            }

            for &cref in clause_refs.iter() {
                let clause = clause_alloc.clause_mut(cref);
                clause.lits_mut().reverse();
            }

            for &cref in clause_refs.iter() {
                let clause_len = clause_alloc.clause(cref).lits().len();
                if clause_len > 3 {
                    clause_alloc.header_mut(cref).set_len(clause_len - 1);
                }
            }

            for (&cref, lits) in clause_refs.iter().zip(input.iter()) {
                let expected = if lits.len() > 3 {
                    lits[1..].iter().rev()
                } else {
                    lits.iter().rev()
                };
                prop_assert!(clause_alloc.clause(cref).lits().iter().eq(expected));
            }
        }
    }
}