use crate::{
clause::Reason,
literal::{Literal, Variable},
memory::{Array, BoundedVector, HeapSpace},
};
use std::{fmt, fmt::Display, ops::Index, slice};
#[derive(Debug, Clone)]
pub struct Assignment {
mapping: Array<Literal, bool>,
trail: BoundedVector<(Literal, Reason)>,
position_in_trail: Array<Literal, usize>,
}
impl PartialEq for Assignment {
fn eq(&self, other: &Assignment) -> bool {
self.mapping == other.mapping
&& self.trail == other.trail
&& (0..self.trail.len()).all(|pos| {
let lit = self.trail_at(pos).0;
self.position_in_trail[lit] == other.position_in_trail[lit]
})
}
}
#[allow(clippy::len_without_is_empty)]
impl Assignment {
pub fn new(maxvar: Variable) -> Assignment {
let mut assignment = Assignment {
mapping: Array::new(false, maxvar.array_size_for_literals()),
trail: BoundedVector::with_capacity(maxvar.array_size_for_variables() + 2),
position_in_trail: Array::new(usize::max_value(), maxvar.array_size_for_literals()),
};
assignment.mapping[Literal::TOP] = true;
assignment.position_in_trail[Literal::TOP] = assignment.len();
assignment.trail.push((Literal::TOP, Reason::assumed()));
assignment
}
pub fn len(&self) -> usize {
self.trail.len()
}
pub fn position_in_trail(&self, literal: Literal) -> usize {
requires!(self[literal]);
self.position_in_trail[literal]
}
pub fn trail_at(&self, offset: usize) -> (Literal, Reason) {
self.trail[offset]
}
pub fn push(&mut self, lit: Literal, reason: Reason) {
requires!(!lit.is_constant());
requires!(!self[lit]);
self.mapping[lit] = true;
self.position_in_trail[lit] = self.len();
self.trail.push((lit, reason));
}
pub fn peek(&mut self) -> (Literal, Reason) {
self.trail[self.len() - 1]
}
pub fn pop(&mut self) -> Option<(Literal, Reason)> {
self.trail.pop().map(|(literal, reason)| {
if !literal.is_constant() {
self.mapping[literal] = false;
}
(literal, reason)
})
}
pub fn move_to(&mut self, src: usize, dst: usize) {
let (literal, reason) = self.trail[src];
self.trail[dst] = (literal, reason);
self.position_in_trail[literal] = dst;
}
pub fn resize(&mut self, level: usize) {
self.trail.resize(level)
}
pub fn unassign(&mut self, literal: Literal) {
requires!(self[literal], "Literal {} is not assigned.", literal);
self.mapping[literal] = false;
}
pub fn set_trail_at(&mut self, offset: usize, literal: Literal, reason: Reason) {
self.mapping[literal] = true;
self.trail[offset] = (literal, reason);
self.position_in_trail[literal] = offset;
}
pub fn iter(&self) -> slice::Iter<(Literal, Reason)> {
self.into_iter()
}
}
impl<'a> IntoIterator for &'a Assignment {
type Item = &'a (Literal, Reason);
type IntoIter = slice::Iter<'a, (Literal, Reason)>;
fn into_iter(self) -> Self::IntoIter {
self.trail.into_iter()
}
}
impl Display for Assignment {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "Assignment: {}", self.len())?;
for (literal, reason) in self {
write!(f, " {} ({}),", literal, reason)?;
}
Ok(())
}
}
impl Index<Literal> for Assignment {
type Output = bool;
fn index(&self, literal: Literal) -> &bool {
&self.mapping[literal]
}
}
impl HeapSpace for Assignment {
fn heap_space(&self) -> usize {
self.mapping.heap_space() + self.trail.heap_space() + self.position_in_trail.heap_space()
}
}
pub fn stable_under_unit_propagation(assignment: &Assignment, clause: &[Literal]) -> bool {
let clause_is_satisfied = clause.iter().any(|&literal| assignment[literal]);
let unknown_count = clause
.iter()
.filter(|&&literal| !assignment[literal] && !assignment[-literal])
.count();
clause_is_satisfied || unknown_count >= 2
}