1 files changed, 148 insertions, 0 deletions
diff --git a/vendor/varisat/src/clause/header.rs b/vendor/varisat/src/clause/header.rs
new file mode 100644
index 000000000..74656e8c1
--- /dev/null
+++ b/vendor/varisat/src/clause/header.rs
@@ -0,0 +1,148 @@
+//! Metadata stored in the header of each long clause.
+use std::cmp::min;
+
+use varisat_formula::{lit::LitIdx, Var};
+
+use super::Tier;
+
+/// Length of a [`ClauseHeader`] in multiples of [`LitIdx`]
+pub(super) const HEADER_LEN: usize = 3;
+
+const TIER_WORD: usize = HEADER_LEN - 2;
+const TIER_OFFSET: usize = 0;
+const TIER_MASK: LitIdx = 0b11;
+
+const DELETED_WORD: usize = HEADER_LEN - 2;
+const DELETED_OFFSET: usize = 2;
+
+const MARK_WORD: usize = HEADER_LEN - 2;
+const MARK_OFFSET: usize = 3;
+
+const GLUE_WORD: usize = HEADER_LEN - 2;
+const GLUE_OFFSET: usize = 4;
+const GLUE_MASK: LitIdx = (1 << 6) - 1;
+
+const ACTIVE_WORD: usize = HEADER_LEN - 2;
+const ACTIVE_OFFSET: usize = 10;
+
+const ACTIVITY_WORD: usize = HEADER_LEN - 3;
+
+/// Metadata for a clause.
+///
+/// This is stored in a [`ClauseAlloc`](super::ClauseAlloc) and thus must have a representation
+/// compatible with slice of [`LitIdx`] values.
+#[repr(transparent)]
+#[derive(Copy, Clone, Default)]
+pub struct ClauseHeader {
+    pub(super) data: [LitIdx; HEADER_LEN],
+}
+
+impl ClauseHeader {
+    /// Create a new clause header with default entries.
+    pub fn new() -> ClauseHeader {
+        Self::default()
+    }
+
+    /// Length of the clause.
+    pub fn len(&self) -> usize {
+        self.data[HEADER_LEN - 1] as usize
+    }
+
+    /// Set the length of the clause.
+    ///
+    /// Must be `<= Var::max_count()` as each variable may only be present once per clause.
+    pub fn set_len(&mut self, length: usize) {
+        debug_assert!(length <= Var::max_count());
+
+        self.data[HEADER_LEN - 1] = length as LitIdx;
+    }
+
+    /// Whether the clause is marked as deleted.
+    pub fn deleted(&self) -> bool {
+        (self.data[DELETED_WORD] >> DELETED_OFFSET) & 1 != 0
+    }
+
+    /// Mark the clause as deleted.
+    pub fn set_deleted(&mut self, deleted: bool) {
+        let word = &mut self.data[DELETED_WORD];
+        *word = (*word & !(1 << DELETED_OFFSET)) | ((deleted as LitIdx) << DELETED_OFFSET);
+    }
+
+    /// Current [`Tier`] of the clause.
+    pub fn tier(&self) -> Tier {
+        unsafe { Tier::from_index(((self.data[TIER_WORD] >> TIER_OFFSET) & TIER_MASK) as usize) }
+    }
+
+    /// Set the current [`Tier`] of the clause.
+    pub fn set_tier(&mut self, tier: Tier) {
+        let word = &mut self.data[TIER_WORD];
+        *word = (*word & !(TIER_MASK << TIER_OFFSET)) | ((tier as LitIdx) << TIER_OFFSET);
+    }
+
+    /// Whether the clause is redundant.
+    pub fn redundant(&self) -> bool {
+        self.tier() != Tier::Irred
+    }
+
+    /// Whether the clause is marked.
+    ///
+    /// The mark is a temporary bit that can be set by various routines, but should always be reset
+    /// to false.
+    pub fn mark(&self) -> bool {
+        (self.data[MARK_WORD] >> MARK_OFFSET) & 1 != 0
+    }
+
+    /// Mark or unmark the clause.
+    ///
+    /// Make sure to clear the mark after use.
+    pub fn set_mark(&mut self, mark: bool) {
+        let word = &mut self.data[MARK_WORD];
+        *word = (*word & !(1 << MARK_OFFSET)) | ((mark as LitIdx) << MARK_OFFSET);
+    }
+
+    /// The clause's active flag
+    ///
+    /// This is set when a clause was involved in conflict analysis and periodically reset.
+    pub fn active(&self) -> bool {
+        (self.data[ACTIVE_WORD] >> ACTIVE_OFFSET) & 1 != 0
+    }
+
+    /// Set or reset the clause's active flag.
+    pub fn set_active(&mut self, active: bool) {
+        let word = &mut self.data[ACTIVE_WORD];
+        *word = (*word & !(1 << ACTIVE_OFFSET)) | ((active as LitIdx) << ACTIVE_OFFSET);
+    }
+
+    /// The [glue][crate::glue] level.
+    pub fn glue(&self) -> usize {
+        ((self.data[GLUE_WORD] >> GLUE_OFFSET) & GLUE_MASK) as usize
+    }
+
+    /// Update the [glue][crate::glue] level.
+    pub fn set_glue(&mut self, glue: usize) {
+        let glue = min(glue, GLUE_MASK as usize) as LitIdx;
+        let word = &mut self.data[GLUE_WORD];
+
+        *word = (*word & !(GLUE_MASK << GLUE_OFFSET)) | (glue << GLUE_OFFSET);
+    }
+
+    /// Clause [activity][crate::clause::activity].
+    pub fn activity(&self) -> f32 {
+        f32::from_bits(self.data[ACTIVITY_WORD] as u32)
+    }
+
+    /// Update clause [activity][crate::clause::activity].
+    pub fn set_activity(&mut self, activity: f32) {
+        self.data[ACTIVITY_WORD] = activity.to_bits() as LitIdx;
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn tier_mask() {
+        assert!(Tier::count() <= TIER_MASK as usize + 1);
+    }
+}