use std::cmp::min;
use varisat_formula::{lit::LitIdx, Var};
use super::Tier;
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;
#[repr(transparent)]
#[derive(Copy, Clone, Default)]
pub struct ClauseHeader {
pub(super) data: [LitIdx; HEADER_LEN],
}
impl ClauseHeader {
pub fn new() -> ClauseHeader {
Self::default()
}
pub fn len(&self) -> usize {
self.data[HEADER_LEN - 1] as usize
}
pub fn set_len(&mut self, length: usize) {
debug_assert!(length <= Var::max_count());
self.data[HEADER_LEN - 1] = length as LitIdx;
}
pub fn deleted(&self) -> bool {
(self.data[DELETED_WORD] >> DELETED_OFFSET) & 1 != 0
}
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);
}
pub fn tier(&self) -> Tier {
unsafe { Tier::from_index(((self.data[TIER_WORD] >> TIER_OFFSET) & TIER_MASK) as usize) }
}
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);
}
pub fn redundant(&self) -> bool {
self.tier() != Tier::Irred
}
pub fn mark(&self) -> bool {
(self.data[MARK_WORD] >> MARK_OFFSET) & 1 != 0
}
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);
}
pub fn active(&self) -> bool {
(self.data[ACTIVE_WORD] >> ACTIVE_OFFSET) & 1 != 0
}
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);
}
pub fn glue(&self) -> usize {
((self.data[GLUE_WORD] >> GLUE_OFFSET) & GLUE_MASK) as usize
}
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);
}
pub fn activity(&self) -> f32 {
f32::from_bits(self.data[ACTIVITY_WORD] as u32)
}
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);
}
}