rate_common/
assignment.rs

1//! A propositional assignment
2//!
3//! This has proven to be a useful abstraction. Unfortunately we need to expose
4//! most of its internals since we modify the assignment vector when applying a
5//! revision.
6
7use crate::{
8    clause::Reason,
9    literal::{Literal, Variable},
10    memory::{Array, BoundedVector, HeapSpace},
11};
12use std::{fmt, fmt::Display, ops::Index, slice};
13
14/// An assignment comprising a mapping plus a trail (vector of literals).
15///
16/// Note that [`Literal::TOP`] is always assigned.
17///
18/// It is valid to assign both a literal and its negation - this is how we detect
19/// a conflict.
20#[derive(Debug, Clone)]
21pub struct Assignment {
22    /// Maps assigned literal to true.
23    mapping: Array<Literal, bool>,
24    /// Assigned literals, in chronologic order.
25    trail: BoundedVector<(Literal, Reason)>,
26    /// Maps literal to their offset in `trail`, or `usize::max_value()`
27    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    /// Create an empty assignment.
44    pub fn new(maxvar: Variable) -> Assignment {
45        let mut assignment = Assignment {
46            mapping: Array::new(false, maxvar.array_size_for_literals()),
47            /// + 2 for Literal::TOP and one conflicting assignment
48            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        // Equivalent to assignment.push(Literal::TOP); but does not check invariants
52        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    /// Return the number of assigned literals.
58    pub fn len(&self) -> usize {
59        self.trail.len()
60    }
61    /// Return the position in the trail where this literal was assigned.
62    pub fn position_in_trail(&self, literal: Literal) -> usize {
63        requires!(self[literal]);
64        self.position_in_trail[literal]
65    }
66    /// Access the trail by offset.
67    pub fn trail_at(&self, offset: usize) -> (Literal, Reason) {
68        self.trail[offset]
69    }
70    /// Add a new literal to the trail, assigning it to true.
71    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    /// View the literal that was assigned last.
79    pub fn peek(&mut self) -> (Literal, Reason) {
80        self.trail[self.len() - 1]
81    }
82    /// Unassign the literal that was assigned last.
83    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    /// Move the literal at trail position `src` to `dst`.
92    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    /// Change the size of the trail.
98    /// Note: this does not change the assigned values, only the trail.
99    pub fn resize(&mut self, level: usize) {
100        self.trail.resize(level)
101    }
102    /// Remove the assignment for a literal, without modifying the trail.
103    pub fn unassign(&mut self, literal: Literal) {
104        requires!(self[literal], "Literal {} is not assigned.", literal);
105        self.mapping[literal] = false;
106    }
107    /// Insert a literal into the trail and assign it.
108    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
118/// Iterate over the literals in the trail, from oldest to newest.
119impl<'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
150/// Given an assignment, return true whenever the clause will not trigger
151/// unit propagation.
152/// This is equivalent to `UP-models` in rupee's sickcheck.
153pub 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}