rate_common/
clause.rs

1//! Data structures for the checker
2
3use crate::memory::Offset;
4use derive_more::Add;
5use serde_derive::{Deserialize, Serialize};
6use static_assertions::const_assert;
7use std::{
8    convert::{TryFrom, TryInto},
9    fmt,
10    io::{self, Write},
11    mem::{align_of, size_of},
12    ops::{Add, AddAssign, Sub, SubAssign},
13};
14
15use crate::literal::Literal;
16
17/// An index uniquely identifying a clause or lemma during the lifetime of the program
18#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone, Copy, Add, Hash, Default)]
19pub struct Clause {
20    pub index: ClauseIdentifierType,
21}
22
23/// The type that backs [Clause](struct.Clause.html).
24pub type ClauseIdentifierType = u32;
25
26impl Clause {
27    /// Create the clause index with the given ID.
28    /// # Panics
29    /// Panics if the index exceeds the internal limit.
30    pub fn new(index: ClauseIdentifierType) -> Clause {
31        requires!(index <= Clause::MAX_ID);
32        Clause { index }
33    }
34    /// Create the clause index with the given usize ID.
35    /// # Panics
36    /// Panics if the index exceeds the internal limit.
37    pub fn from_usize(index: usize) -> Clause {
38        requires!(index < ClauseIdentifierType::max_value().try_into().unwrap());
39        Clause::new(index as ClauseIdentifierType)
40    }
41    /// Create an iterator from clause indices `start` up to (excluding) `end`.
42    pub fn range(start: impl Offset, end: impl Offset) -> impl Iterator<Item = Clause> {
43        const_assert!(size_of::<usize>() >= size_of::<ClauseIdentifierType>());
44        (start.as_offset()..end.as_offset()).map(Clause::from_usize)
45    }
46    /// The maximum value a regular `Clause` can assume.
47    pub const MAX_ID: ClauseIdentifierType = Tagged32::MAX_PAYLOAD - 1;
48    /// We need one special value for deleted clauses that do not actually exist.
49    /// We cannot simply drop those deletions from the proof because `sick-check`
50    /// relies on the line in the proof.
51    pub const DOES_NOT_EXIST: Clause = Clause {
52        index: Clause::MAX_ID + 1,
53    };
54    /// A special value for clause IDs. Used in places where we are sure
55    /// that the value is written before being used as an actual clause ID.
56    pub const UNINITIALIZED: Clause = Clause {
57        index: Clause::MAX_ID + 2,
58    };
59}
60
61impl Offset for Clause {
62    fn as_offset(&self) -> usize {
63        self.index as usize
64    }
65}
66
67impl Add<ClauseIdentifierType> for Clause {
68    type Output = Clause;
69    fn add(self, value: ClauseIdentifierType) -> Clause {
70        Clause::new(self.index + value)
71    }
72}
73
74impl AddAssign<ClauseIdentifierType> for Clause {
75    fn add_assign(&mut self, value: ClauseIdentifierType) {
76        self.index += value;
77    }
78}
79
80impl Sub<ClauseIdentifierType> for Clause {
81    type Output = Clause;
82    fn sub(self, value: ClauseIdentifierType) -> Clause {
83        Clause::new(self.index - value)
84    }
85}
86
87impl SubAssign<ClauseIdentifierType> for Clause {
88    fn sub_assign(&mut self, value: ClauseIdentifierType) {
89        self.index -= value;
90    }
91}
92
93impl fmt::Display for Clause {
94    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
95        write!(f, "{}", self.index)
96    }
97}
98
99/// A clause introduction or deletion
100///
101/// This is essentially this enum, but we pack everything into 32 bits.
102/// ```
103/// # use rate_common::clause::Clause;
104/// enum ProofStep {
105///     Lemma(Clause),
106///     Deletion(Clause),
107/// }
108/// ```
109#[derive(Debug, PartialEq, Eq, Clone, Copy, Default)]
110pub struct ProofStep(Tagged32);
111
112impl ProofStep {
113    /// Create a proof step that introduces the given clause.
114    pub fn lemma(clause: Clause) -> ProofStep {
115        ProofStep(Tagged32::new(clause.index))
116    }
117    /// Create a proof step that deletes the given clause.
118    pub fn deletion(clause: Clause) -> ProofStep {
119        ProofStep(Tagged32::new(clause.index).with_bit1())
120    }
121    /// Return true if this proof step is a clause deletion.
122    pub fn is_deletion(self) -> bool {
123        self.0.bit1()
124    }
125    /// Return the clause that this proof step introduces or deletes.
126    pub fn clause(self) -> Clause {
127        Clause {
128            index: self.0.payload(),
129        }
130    }
131}
132
133/// The reason for assigning a literal
134///
135/// A literal can be assumed, or forced by some clause. The clause
136/// is stored as offset to reduce the number of indirections in
137/// [propagate](../checker/fn.propagate.html).
138///
139/// This is essentially this enum, but we pack everything into `size_of::<usize>()` bits.
140/// ```
141/// enum Reason {
142///     Assumed,
143///     Forced(usize),
144/// }
145/// ```
146#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
147pub struct Reason(TaggedUSize);
148
149impl Reason {
150    /// Create an invalid reason, i.e. for unassigned literals.
151    pub fn invalid() -> Reason {
152        Reason(TaggedUSize::new(0))
153    }
154    /// Create a reason for assumed literals.
155    pub fn assumed() -> Reason {
156        Reason(TaggedUSize::new(0).with_bit1())
157    }
158    /// Create a reason for a clause that has been forced by the clause with
159    /// the given offset.
160    pub fn forced(offset: usize) -> Reason {
161        Reason(
162            TaggedUSize::new(offset.try_into().unwrap())
163                .with_bit1()
164                .with_bit2(),
165        )
166    }
167    /// Return true when this is an assumption.
168    pub fn is_assumed(self) -> bool {
169        invariant!(self != Reason::invalid());
170        !self.0.bit2()
171    }
172    /// Return the offset of the clause. Only valid if this is not an
173    /// assumption or invalid.
174    pub fn offset(self) -> usize {
175        invariant!(self != Reason::invalid());
176        invariant!(self != Reason::assumed());
177        self.0.payload() as usize
178    }
179}
180
181impl fmt::Display for Reason {
182    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
183        write!(
184            f,
185            "{}",
186            if self.is_assumed() {
187                "Assumption".into()
188            } else {
189                format!("Forced by clause {}", self.offset())
190            }
191        )
192    }
193}
194
195/// An intermediate representation of an LRAT hint
196///
197/// This is essentially this enum, but we pack everything into 32 bits.
198/// ```
199/// # use rate_common::clause::Clause;
200/// enum LRATDependency {
201///     Unit(Clause),
202///     ForcedUnit(Clause),
203///     ResolutionCandidate(Clause),
204/// }
205/// ```
206#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Default)]
207pub struct LRATDependency(Tagged32);
208
209impl LRATDependency {
210    /// Create a hint stating that the given clause became unit during the
211    /// redundancy check.
212    pub fn unit_in_inference(clause: Clause) -> LRATDependency {
213        LRATDependency(Tagged32::new(clause.index as u32))
214    }
215    /// Return true if this was a unit in the inference check.
216    pub fn is_unit_in_inference(self) -> bool {
217        !self.0.bit1() && !self.0.bit2()
218    }
219    /// Create a hint stating that the given clause was unit even before
220    /// the redundancy check.
221    pub fn forced_unit(clause: Clause) -> LRATDependency {
222        LRATDependency(Tagged32::new(clause.index as u32).with_bit1())
223    }
224    /// Return true if this is a hint for a forced unit clause.
225    pub fn is_forced_unit(self) -> bool {
226        self.0.bit1() && !self.0.bit2()
227    }
228    /// Create a hint referring to the given clause as resolution candidate.
229    pub fn resolution_candidate(clause: Clause) -> LRATDependency {
230        LRATDependency(Tagged32::new(clause.index as u32).with_bit1().with_bit2())
231    }
232    /// Return true if this is a hint for a resolution candidate.
233    pub fn is_resolution_candidate(self) -> bool {
234        self.0.bit1() && self.0.bit2()
235    }
236    /// Return the clause referenced by this hint.
237    pub fn clause(self) -> Clause {
238        Clause {
239            index: self.0.payload(),
240        }
241    }
242}
243
244/// A literal in the LRAT proof output
245///
246/// This is essentially this enum, but we pack everything into 32 bits.
247/// ```
248/// # use rate_common::clause::Clause;
249/// enum LRATLiteral {
250///     ResolutionCandidate(Clause),
251///     Hint(Clause),
252///     Zero,
253/// }
254/// ```
255#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Default)]
256pub struct LRATLiteral(Tagged32);
257
258impl LRATLiteral {
259    /// Create a hint for a resolution candidate.
260    pub fn resolution_candidate(clause: Clause) -> LRATLiteral {
261        LRATLiteral(Tagged32::new(clause.index as u32))
262    }
263    /// Return true if this is refers to a resolution candidate.
264    pub fn is_resolution_candidate(self) -> bool {
265        !self.0.bit1() && !self.0.bit2()
266    }
267    /// Create a hint for a unit clause.
268    pub fn hint(clause: Clause) -> LRATLiteral {
269        LRATLiteral(Tagged32::new(clause.index as u32).with_bit1())
270    }
271    /// Return true if this is a unit clause hint.
272    pub fn is_hint(self) -> bool {
273        self.0.bit1() && !self.0.bit2()
274    }
275    /// Create a zero terminator literal.
276    pub fn zero() -> LRATLiteral {
277        LRATLiteral(Tagged32::new(0).with_bit1().with_bit2())
278    }
279    /// Return true if this is a zero terminator.
280    pub fn is_zero(self) -> bool {
281        self.0.bit1() && self.0.bit2()
282    }
283    /// Assuming this is not a zero terminator, return the referenced clause.
284    pub fn clause(self) -> Clause {
285        requires!(!self.is_zero());
286        Clause {
287            index: self.0.payload(),
288        }
289    }
290}
291
292/// A literal for the GRAT proof output
293#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
294pub struct GRATLiteral(pub i32);
295
296impl GRATLiteral {
297    pub const ZERO: Self = Self(0);
298    pub const UNIT_PROP: Self = Self(1);
299    pub const DELETION: Self = Self(2);
300    pub const RUP_LEMMA: Self = Self(3);
301    pub const RAT_LEMMA: Self = Self(4);
302    pub const CONFLICT: Self = Self(5);
303    pub const RAT_COUNTS: Self = Self(6);
304    /// Create a GRAT literal that references the given internal clause.
305    pub fn from_clause(clause: Clause) -> GRATLiteral {
306        requires!(clause.index + 1 < ClauseIdentifierType::max_value());
307        Self((clause.index + 1) as i32)
308    }
309    /// Compute the internal clause from a given GRAT literal.
310    pub fn to_clause(self) -> Clause {
311        requires!(self.0 != 0);
312        Clause::new(ClauseIdentifierType::try_from(self.0).unwrap() - 1)
313    }
314}
315
316impl fmt::Display for GRATLiteral {
317    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
318        write!(f, "{}", self.0)
319    }
320}
321
322/// Value with 30 bit payload with 2 flag bits
323#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone, Copy, Default)]
324pub struct Tagged32(u32);
325
326impl Tagged32 {
327    /// Mask for the both flag bits.
328    const MASK: u32 = Tagged32::MASK1 | Tagged32::MASK2;
329    /// Mask for the first flag bit.
330    const MASK1: u32 = 0x80_00_00_00;
331    /// Mask for the second flag bit.
332    const MASK2: u32 = 0x40_00_00_00;
333    /// The maximum value for the payload.
334    const MAX_PAYLOAD: u32 = u32::max_value() & !Tagged32::MASK;
335
336    pub fn new(payload: u32) -> Tagged32 {
337        requires!(payload <= Tagged32::MAX_PAYLOAD);
338        Tagged32(payload)
339    }
340    pub fn with_bit1(self) -> Tagged32 {
341        Tagged32(self.0 | Tagged32::MASK1)
342    }
343    pub fn with_bit2(self) -> Tagged32 {
344        Tagged32(self.0 | Tagged32::MASK2)
345    }
346    pub fn payload(self) -> u32 {
347        self.0 & !Tagged32::MASK
348    }
349    pub fn bit1(self) -> bool {
350        self.0 & Tagged32::MASK1 != 0
351    }
352    pub fn bit2(self) -> bool {
353        self.0 & Tagged32::MASK2 != 0
354    }
355}
356
357/// Value with `size_of::<usize>() - 2` bits of payload and 2 flag bits
358#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone, Copy, Default)]
359pub struct TaggedUSize(usize);
360
361impl TaggedUSize {
362    const MASK: usize = TaggedUSize::MASK1 | TaggedUSize::MASK2;
363    pub const MASK1: usize = 1 << (size_of::<usize>() * 8 - 1);
364    pub const MASK2: usize = 1 << (size_of::<usize>() * 8 - 2);
365    const MAX_PAYLOAD: usize = usize::max_value() & !TaggedUSize::MASK;
366
367    pub fn new(payload: usize) -> TaggedUSize {
368        requires!(payload <= TaggedUSize::MAX_PAYLOAD);
369        TaggedUSize(payload)
370    }
371    pub fn with_bit1(self) -> TaggedUSize {
372        TaggedUSize(self.0 | TaggedUSize::MASK1)
373    }
374    pub fn with_bit2(self) -> TaggedUSize {
375        TaggedUSize(self.0 | TaggedUSize::MASK2)
376    }
377    pub fn payload(self) -> usize {
378        self.0 & !TaggedUSize::MASK
379    }
380    pub fn bit1(self) -> bool {
381        self.0 & TaggedUSize::MASK1 != 0
382    }
383    pub fn bit2(self) -> bool {
384        self.0 & TaggedUSize::MASK2 != 0
385    }
386}
387
388/// The redundancy property to use for inference checks.
389#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
390pub enum RedundancyProperty {
391    RAT,
392    PR,
393}
394
395impl fmt::Display for RedundancyProperty {
396    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
397        write!(
398            f,
399            "{}",
400            match self {
401                RedundancyProperty::RAT => "RAT",
402                RedundancyProperty::PR => "PR",
403            }
404        )
405    }
406}
407
408/// State the sizes of data types.
409#[allow(dead_code)]
410fn assert_primitive_sizes() {
411    const_assert!(size_of::<crate::literal::Literal>() == 4);
412    const_assert!(size_of::<Clause>() == 4);
413    const_assert!(size_of::<LRATDependency>() == 4);
414    const_assert!(size_of::<LRATLiteral>() == 4);
415    const_assert!(size_of::<ProofStep>() == 4);
416    const_assert!(size_of::<Reason>() == size_of::<usize>());
417    const_assert!(align_of::<Reason>() == align_of::<usize>());
418}
419
420/// Write some literals in DIMACS format.
421///
422/// Includes a terminating 0, but no newline.
423pub fn write_clause<'a, T>(file: &mut impl Write, clause: T) -> io::Result<()>
424where
425    T: Iterator<Item = &'a Literal>,
426{
427    for &literal in clause {
428        if literal != Literal::BOTTOM {
429            write!(file, "{} ", literal)?;
430        }
431    }
432    write!(file, "0")
433}
434
435/// Write the some literals in DIMACS format to stdout.
436pub fn puts_clause<'a, T>(clause: T)
437where
438    T: IntoIterator<Item = &'a Literal>,
439{
440    for &literal in clause.into_iter() {
441        if literal != Literal::BOTTOM {
442            puts!("{} ", literal);
443        }
444    }
445    puts!("0")
446}
447
448/// Write the clause ID and literals to stdout, like [<ID] <literals> 0.
449pub fn puts_clause_with_id<'a, T>(clause: Clause, literals: T)
450where
451    T: IntoIterator<Item = &'a Literal>,
452{
453    puts!("[{}] ", clause);
454    puts_clause(literals);
455}
456
457/// Write the clause ID, literals and a witness to stdout, like
458/// [<ID] <literals> <witness> 0.
459pub fn puts_clause_with_id_and_witness(clause: Clause, literals: &[Literal], witness: &[Literal]) {
460    // The order of literals in the clause may have changed,
461    // but not in the witness. Make sure to print the first
462    // literal in the witness first to maintain the PR format.
463    let witness_head = witness.first().cloned();
464    puts!("[{}] ", clause);
465    for &literal in literals {
466        if literal != Literal::BOTTOM && Some(literal) != witness_head {
467            puts!("{} ", literal);
468        }
469    }
470    puts_clause(witness);
471}
rate_common/clause.rs

rate_common/
clause.rs
