rate_common/
clausedatabase.rs

1//! Container for clauses
2
3use crate::{
4    clause::{puts_clause_with_id, Clause, ClauseIdentifierType},
5    literal::Literal,
6    memory::{HeapSpace, Offset, Vector},
7};
8
9use rate_macros::HeapSpace;
10use std::{
11    convert::TryFrom,
12    mem::size_of,
13    ops::{Index, IndexMut, Range},
14};
15
16pub trait ClauseStorage {
17    /// Initialze a new clause.
18    ///
19    /// This must be called before adding literals with
20    /// [`push_literal()`](#tymethod.push_literal).
21    fn open_clause(&mut self) -> Clause;
22    /// Add a literal to the current clause.
23    ///
24    /// If passed literal 0, the clause will be finished and
25    /// [`open_clause()`](#tymethod.open_clause) must be called before adding
26    /// literals to the next clause.
27    fn push_literal(&mut self, literal: Literal, verbose: bool);
28}
29
30/// Size of metadata that precede the literals of a clause
31pub const PADDING_START: usize = 2;
32/// Location of the fields within the metadata.
33pub const FIELDS_OFFSET: usize = 1;
34/// Size of the clause suffix (terminating 0)
35pub const PADDING_END: usize = 1;
36
37/// Stores clauses in a flat buffer
38#[derive(Debug, PartialEq, HeapSpace)]
39pub struct ClauseDatabase {
40    /// Stores clauses with some metadata.
41    /// The first element encodes the clause ID.
42    /// The second element contains a `struct ClauseFields`.
43    /// After that, the literals are stored (zero-terminated)
44    data: Vector<Literal>,
45    /// Maps clause ID to offset in above data.
46    offset: Vector<usize>,
47    /// Used to assert that `offset` contains an extra value that points
48    /// one beyond the last element of `data`.
49    have_sentinel: bool,
50}
51
52impl ClauseStorage for ClauseDatabase {
53    fn open_clause(&mut self) -> Clause {
54        requires!(self.have_sentinel);
55        let id = self.number_of_clauses();
56        self.pop_sentinel();
57        let clause = Clause::new(id);
58        self.offset.push(self.data.len()); // clause
59        self.data.push(Literal::from_raw(id));
60        self.data.push(Literal::from_raw(0)); // fields
61        clause
62    }
63    fn push_literal(&mut self, literal: Literal, verbose: bool) {
64        if literal.is_zero() {
65            self.close_clause(verbose)
66        } else {
67            self.data.push(literal)
68        }
69    }
70}
71
72impl Default for ClauseDatabase {
73    /// Create an empty clause database.
74    fn default() -> ClauseDatabase {
75        let mut db = ClauseDatabase {
76            data: Vector::new(),
77            offset: Vector::new(),
78            have_sentinel: false,
79        };
80        db.push_sentinel(db.data.len());
81        db
82    }
83}
84
85impl ClauseDatabase {
86    /// Create a database from raw elements; used only for tests.
87    #[cfg(test)]
88    pub fn from(data: Vector<Literal>, offset: Vector<usize>) -> ClauseDatabase {
89        let mut db = ClauseDatabase {
90            data,
91            offset,
92            have_sentinel: false,
93        };
94        db.push_sentinel(db.data.len());
95        db
96    }
97    /// Returns the total number that are stored.
98    pub fn number_of_clauses(&self) -> ClauseIdentifierType {
99        requires!(self.have_sentinel);
100        let sentinel_size = 1;
101        let number = self.offset.len() - sentinel_size;
102        requires!(ClauseIdentifierType::try_from(number).is_ok());
103        number as ClauseIdentifierType
104    }
105    /// Returns the clause that was added last.
106    pub fn last_clause(&self) -> Clause {
107        requires!(self.have_sentinel);
108        requires!(self.number_of_clauses() > 0);
109        Clause::new(self.number_of_clauses() - 1)
110    }
111    /// Returns the clause that was added last, assuming there is no sentinel
112    fn last_clause_no_sentinel(&self) -> Clause {
113        requires!(!self.have_sentinel);
114        let index = self.offset.len() - 1;
115        Clause::from_usize(index)
116    }
117    /// Add the sentinel, stating that `offset` is the end of the last clause.
118    fn push_sentinel(&mut self, offset: usize) {
119        requires!(!self.have_sentinel);
120        self.offset.push(offset);
121        self.have_sentinel = true;
122    }
123    /// Remove the sentinel to allow adding a new clause.
124    fn pop_sentinel(&mut self) {
125        requires!(self.have_sentinel);
126        self.offset.pop();
127        self.have_sentinel = false;
128    }
129    /// Finish the current clause.
130    fn close_clause(&mut self, verbose: bool) {
131        requires!(!self.have_sentinel);
132        let clause = self.last_clause_no_sentinel();
133        let start = self.offset[clause.as_offset()] + PADDING_START;
134        let end = self.data.len();
135        sort_clause(&mut self.data[start..end]);
136        let mut duplicate = false;
137        let mut length = 0;
138        for i in start..end {
139            if i + 1 < end && self[i] == self[i + 1] {
140                duplicate = true;
141            } else {
142                self[start + length] = self[i];
143                length += 1;
144            }
145        }
146        self.data.truncate(start + length);
147        if length == 1 {
148            self.data.push(Literal::BOTTOM);
149        }
150        self.data.push(Literal::new(0));
151        self.push_sentinel(self.data.len());
152        if verbose && duplicate {
153            as_warning!({
154                puts!("c removed duplicate literals in ");
155                puts_clause_with_id(clause, self.clause(clause));
156                puts!("\n");
157            });
158        }
159    }
160    /// Delete the last clause.
161    pub fn pop_clause(&mut self) {
162        requires!(self.have_sentinel);
163        let last_clause = self.last_clause();
164        let last_clause_offset = self.offset[last_clause.as_offset()];
165        self.data.truncate(last_clause_offset);
166        self.pop_sentinel();
167        self.offset.pop(); // clause
168        self.push_sentinel(last_clause_offset);
169    }
170    /// Give the DIMACS representation of a clause.
171    ///
172    /// Only used for debugging, prefer `clause::write_clause()`.
173    pub fn clause_to_string(&self, clause: Clause) -> String {
174        format!(
175            "[{}]{} 0",
176            clause,
177            self.clause(clause)
178                .iter()
179                .filter(|&literal| *literal != Literal::BOTTOM)
180                .map(|&literal| format!(" {}", literal))
181                .collect::<Vector<_>>()
182                .join("")
183        )
184    }
185    /// The literals in the the clause.
186    pub fn clause(&self, clause: Clause) -> &[Literal] {
187        &self.data[self.clause_range(clause)]
188    }
189    /// The internal offsets of the literals in the the clause.
190    pub fn clause_range(&self, clause: Clause) -> Range<usize> {
191        requires!(self.have_sentinel);
192        self.offset[clause.as_offset()] + PADDING_START
193            ..self.offset[clause.as_offset() + 1] - PADDING_END
194    }
195    /// The first two literals in the clause.
196    pub fn watches(&self, head: usize) -> [Literal; 2] {
197        [self[head], self[head + 1]]
198    }
199    /// Convert a clause identifier to the offset of the clause.
200    pub fn clause2offset(&self, clause: Clause) -> usize {
201        self.clause_range(clause).start
202    }
203    /// Convert a clause offset to the identifier of the clause.
204    pub fn offset2clause(&self, head: usize) -> Clause {
205        Clause::new(self[head - PADDING_START].encoding)
206    }
207    /// Swap the literal at the given offsets in the clause database.
208    pub fn swap(&mut self, a: usize, b: usize) {
209        self.data.swap(a, b);
210    }
211    /// Access the metadata for this clause.
212    pub fn fields(&self, clause: Clause) -> &u32 {
213        &self.data[self.offset[clause.as_offset()] + FIELDS_OFFSET].encoding
214    }
215    /// Access the mutable metadata for this clause.
216    pub fn fields_mut(&mut self, clause: Clause) -> &mut u32 {
217        &mut self.data[self.offset[clause.as_offset()] + FIELDS_OFFSET].encoding
218    }
219    /// Access the metadata for the clause with this offset.
220    /// This is possibly more efficient than [`fields()`](#method.fields).
221    pub fn fields_from_offset(&self, offset: usize) -> &u32 {
222        &self.data[offset - 1].encoding
223    }
224    /// Access the mutable metadata for the clause with this offset.
225    /// This is possibly more efficient than [`fields()`](#method.fields_mut).
226    pub fn fields_mut_from_offset(&mut self, offset: usize) -> &mut u32 {
227        &mut self.data[offset - 1].encoding
228    }
229    /// See [`Vec::shrink_to_fit()`](https://doc.rust-lang.org/std/vec/struct.Vec.html#method.shrink_to_fit).
230    pub fn shrink_to_fit(&mut self) {
231        // TODO: Should be (nightly) shrink_to(len() + 1), see rate::close_proof.
232        self.data.push(Literal::new(0));
233        self.data.shrink_to_fit();
234        self.data.pop();
235        self.offset.push(0);
236        self.offset.shrink_to_fit();
237        self.offset.pop();
238    }
239    /// Expected memory usage.
240    #[allow(dead_code)]
241    fn metrics(&self) {
242        let _db_size = self.data.capacity() * size_of::<Literal>();
243        let _drat_trim_clause_db_size = size_of::<Literal>()
244            * (
245                self.data.capacity() // our
246                // we add padding to unit clauses
247                - (0..self.number_of_clauses()).map(Clause::new).filter(|&c| is_size_1_clause(self.clause(c))).count()
248                + self.number_of_clauses() as usize // pivots
249                - (2 + 1) // extra empty clause (id + fields + zero literal)
250                + 1
251                // sentinel
252            );
253    }
254}
255
256impl Index<usize> for ClauseDatabase {
257    type Output = Literal;
258    fn index(&self, offset: usize) -> &Literal {
259        &self.data[offset]
260    }
261}
262
263impl IndexMut<usize> for ClauseDatabase {
264    fn index_mut(&mut self, offset: usize) -> &mut Literal {
265        &mut self.data[offset]
266    }
267}
268
269/// Stores witnesses in a flat buffer
270///
271/// Each witness is a set of literals that are associated with a clause.
272#[derive(Debug, PartialEq, HeapSpace)]
273pub struct WitnessDatabase {
274    data: Vector<Literal>,
275    offset: Vector<usize>,
276}
277
278impl ClauseStorage for WitnessDatabase {
279    fn open_clause(&mut self) -> Clause {
280        self.offset.pop();
281        let witness = Clause::from_usize(self.offset.len());
282        self.offset.push(self.data.len());
283        witness
284    }
285    fn push_literal(&mut self, literal: Literal, _verbose: bool) {
286        if literal.is_zero() {
287            self.close_witness();
288        } else {
289            self.data.push(literal);
290        }
291    }
292}
293
294impl Default for WitnessDatabase {
295    /// Create an empty witness database.
296    fn default() -> WitnessDatabase {
297        let mut db = WitnessDatabase {
298            data: Vector::new(),
299            offset: Vector::new(),
300        };
301        db.offset.push(0);
302        db
303    }
304}
305
306impl WitnessDatabase {
307    /// Create a database from raw elements; used only for tests.
308    #[cfg(test)]
309    pub fn from(data: Vector<Literal>, offset: Vector<usize>) -> WitnessDatabase {
310        WitnessDatabase { data, offset }
311    }
312    /// Finish the current witness.
313    /// Similar to [`close_clause()`](struct.ClauseDatabase.html#method.close_clause).
314    fn close_witness(&mut self) {
315        self.offset.push(self.data.len())
316    }
317    /// Give the DIMACS representation of a witness.
318    ///
319    /// Similar to [`clause_to_string()`](struct.ClauseDatabase.html#method.clause_to_string).
320    pub fn witness_to_string(&self, clause: Clause) -> String {
321        format!(
322            "Witness for [{}]:{} 0",
323            clause,
324            self.witness(clause)
325                .iter()
326                .map(|&literal| format!(" {}", literal))
327                .collect::<Vec<_>>()
328                .join("")
329        )
330    }
331    /// The literals in the the witness.
332    pub fn witness(&self, clause: Clause) -> &[Literal] {
333        &self.data[self.witness_range(clause)]
334    }
335    /// The internal offsets of the literals in the the witness.
336    pub fn witness_range(&self, clause: Clause) -> Range<usize> {
337        self.offset[clause.as_offset()]..self.offset[clause.as_offset() + 1]
338    }
339    /// See [`Vec::shrink_to_fit()`](https://doc.rust-lang.org/std/vec/struct.Vec.html#method.shrink_to_fit).
340    pub fn shrink_to_fit(&mut self) {
341        // TODO: Should be (nightly) shrink_to(len() + 1), see rate::close_proof.
342        self.data.push(Literal::new(0));
343        self.data.shrink_to_fit();
344        self.data.pop();
345        self.offset.push(0);
346        self.offset.shrink_to_fit();
347        self.offset.pop();
348    }
349}
350
351impl Index<usize> for WitnessDatabase {
352    type Output = Literal;
353    fn index(&self, offset: usize) -> &Literal {
354        &self.data[offset]
355    }
356}
357
358impl IndexMut<usize> for WitnessDatabase {
359    fn index_mut(&mut self, offset: usize) -> &mut Literal {
360        &mut self.data[offset]
361    }
362}
363
364/// Return true if this clause is of size one (special type of unit clause).
365fn is_size_1_clause(clause: &[Literal]) -> bool {
366    clause.len() == 2 && (clause[0] == Literal::BOTTOM || clause[1] == Literal::BOTTOM)
367}
368
369/// Sort a clause by its internal encoding
370fn sort_clause(clause: &mut [Literal]) {
371    let _sort_literally = |&literal: &Literal| literal.decode();
372    let _sort_magnitude = |&literal: &Literal| literal.encoding;
373    clause.sort_unstable_by_key(_sort_literally);
374}
rate_common/clausedatabase.rs

rate_common/
clausedatabase.rs
