use std::{mem::transmute, slice};
use varisat_formula::{lit::LitIdx, Lit};
use super::{Clause, ClauseHeader, HEADER_LEN};
type ClauseOffset = u32;
#[derive(Default)]
pub struct ClauseAlloc {
buffer: Vec<LitIdx>,
}
impl ClauseAlloc {
pub fn new() -> ClauseAlloc {
ClauseAlloc::default()
}
pub fn with_capacity(capacity: usize) -> ClauseAlloc {
ClauseAlloc {
buffer: Vec::with_capacity(capacity),
}
}
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"
);
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 {
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,
}
}
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) }
}
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
}
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
}
pub fn clause(&self, cref: ClauseRef) -> &Clause {
let header = self.header(cref);
let len = header.len();
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) }
}
pub fn clause_mut(&mut self, cref: ClauseRef) -> &mut Clause {
let header = self.header(cref);
let len = header.len();
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) }
}
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
}
pub fn check_bounds(&self, cref: ClauseRef, len: usize) {
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,
))
}
pub fn buffer_size(&self) -> usize {
self.buffer.len()
}
}
#[derive(Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Debug)]
pub struct ClauseRef {
offset: ClauseOffset,
}
impl ClauseRef {
const fn max_offset() -> ClauseOffset {
((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());
}
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));
}
}
}
}