rate_common/
assignment.rs1use crate::{
8 clause::Reason,
9 literal::{Literal, Variable},
10 memory::{Array, BoundedVector, HeapSpace},
11};
12use std::{fmt, fmt::Display, ops::Index, slice};
13
14#[derive(Debug, Clone)]
21pub struct Assignment {
22 mapping: Array<Literal, bool>,
24 trail: BoundedVector<(Literal, Reason)>,
26 position_in_trail: Array<Literal, usize>,
28}
29
30impl PartialEq for Assignment {
31 fn eq(&self, other: &Assignment) -> bool {
32 self.mapping == other.mapping
33 && self.trail == other.trail
34 && (0..self.trail.len()).all(|pos| {
35 let lit = self.trail_at(pos).0;
36 self.position_in_trail[lit] == other.position_in_trail[lit]
37 })
38 }
39}
40
41#[allow(clippy::len_without_is_empty)]
42impl Assignment {
43 pub fn new(maxvar: Variable) -> Assignment {
45 let mut assignment = Assignment {
46 mapping: Array::new(false, maxvar.array_size_for_literals()),
47 trail: BoundedVector::with_capacity(maxvar.array_size_for_variables() + 2),
49 position_in_trail: Array::new(usize::max_value(), maxvar.array_size_for_literals()),
50 };
51 assignment.mapping[Literal::TOP] = true;
53 assignment.position_in_trail[Literal::TOP] = assignment.len();
54 assignment.trail.push((Literal::TOP, Reason::assumed()));
55 assignment
56 }
57 pub fn len(&self) -> usize {
59 self.trail.len()
60 }
61 pub fn position_in_trail(&self, literal: Literal) -> usize {
63 requires!(self[literal]);
64 self.position_in_trail[literal]
65 }
66 pub fn trail_at(&self, offset: usize) -> (Literal, Reason) {
68 self.trail[offset]
69 }
70 pub fn push(&mut self, lit: Literal, reason: Reason) {
72 requires!(!lit.is_constant());
73 requires!(!self[lit]);
74 self.mapping[lit] = true;
75 self.position_in_trail[lit] = self.len();
76 self.trail.push((lit, reason));
77 }
78 pub fn peek(&mut self) -> (Literal, Reason) {
80 self.trail[self.len() - 1]
81 }
82 pub fn pop(&mut self) -> Option<(Literal, Reason)> {
84 self.trail.pop().map(|(literal, reason)| {
85 if !literal.is_constant() {
86 self.mapping[literal] = false;
87 }
88 (literal, reason)
89 })
90 }
91 pub fn move_to(&mut self, src: usize, dst: usize) {
93 let (literal, reason) = self.trail[src];
94 self.trail[dst] = (literal, reason);
95 self.position_in_trail[literal] = dst;
96 }
97 pub fn resize(&mut self, level: usize) {
100 self.trail.resize(level)
101 }
102 pub fn unassign(&mut self, literal: Literal) {
104 requires!(self[literal], "Literal {} is not assigned.", literal);
105 self.mapping[literal] = false;
106 }
107 pub fn set_trail_at(&mut self, offset: usize, literal: Literal, reason: Reason) {
109 self.mapping[literal] = true;
110 self.trail[offset] = (literal, reason);
111 self.position_in_trail[literal] = offset;
112 }
113 pub fn iter(&self) -> slice::Iter<(Literal, Reason)> {
114 self.into_iter()
115 }
116}
117
118impl<'a> IntoIterator for &'a Assignment {
120 type Item = &'a (Literal, Reason);
121 type IntoIter = slice::Iter<'a, (Literal, Reason)>;
122 fn into_iter(self) -> Self::IntoIter {
123 self.trail.into_iter()
124 }
125}
126
127impl Display for Assignment {
128 fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
129 write!(f, "Assignment: {}", self.len())?;
130 for (literal, reason) in self {
131 write!(f, " {} ({}),", literal, reason)?;
132 }
133 Ok(())
134 }
135}
136
137impl Index<Literal> for Assignment {
138 type Output = bool;
139 fn index(&self, literal: Literal) -> &bool {
140 &self.mapping[literal]
141 }
142}
143
144impl HeapSpace for Assignment {
145 fn heap_space(&self) -> usize {
146 self.mapping.heap_space() + self.trail.heap_space() + self.position_in_trail.heap_space()
147 }
148}
149
150pub fn stable_under_unit_propagation(assignment: &Assignment, clause: &[Literal]) -> bool {
154 let clause_is_satisfied = clause.iter().any(|&literal| assignment[literal]);
155 let unknown_count = clause
156 .iter()
157 .filter(|&&literal| !assignment[literal] && !assignment[-literal])
158 .count();
159 clause_is_satisfied || unknown_count >= 2
160}