veripb_formula/
assignment.rs

1//! Mapping of variables to values.
2
3use std::fmt::Display;
4
5use crate::{prelude::*, substitution::Substitutable};
6
7/// Data structure to store mapping from [`VarIdx`] to [`VarType`].
8#[derive(Debug, Default, Clone)]
9pub struct Assignment<V> {
10    pub assignment: Vec<V>,
11}
12
13impl<V> Assignment<V>
14where
15    V: VarType,
16{
17    /// Initialize a new [`Assignment`] with specific `size` where all entries are set to the default value of [`VarType`].
18    #[inline]
19    pub fn with_size(size: usize) -> Self {
20        Assignment::<V> {
21            assignment: vec![Default::default(); size],
22        }
23    }
24
25    /// Resizes the [`Assignment`] to the given `new_len`.
26    ///
27    /// If `new_len` is smaller than the current `len` of `Assignment`, the [`Assignment`] is truncated to `new_len`. If `new_len` is larger than the current `len` of [`Assignment`], then [`Assignment`] is increased up to `new_len` and filled with the default values for [`VarType`], but the entries up to the current length are left unchanged.
28    #[inline]
29    pub fn resize(&mut self, new_len: usize) {
30        self.assignment.resize(new_len, Default::default());
31    }
32
33    /// Set variable at index `idx` to `value`.
34    #[inline]
35    pub fn set_value(&mut self, idx: VarIdx, value: V::Value) {
36        self.assignment[idx].set_value(value);
37    }
38
39    /// Get the value of the variable at index `idx`.
40    #[inline]
41    pub fn get_value(&self, idx: VarIdx) -> V::Value {
42        self.assignment[idx].get_value()
43    }
44
45    /// Set a value by using a [`Lit`]. Hence, if [`Lit`] is negated, then the value assigned to its variable is negated.
46    #[inline]
47    pub fn set_lit_value(&mut self, lit: Lit, value: V::Value) {
48        if lit.is_negated() {
49            self.assignment[lit.get_var()].set_value(value.negate());
50        } else {
51            self.assignment[lit.get_var()].set_value(value);
52        }
53    }
54
55    /// Set a value by literal. Hence, if the literal is negated, then value assigned to its variable is negated.
56    ///
57    /// # Safety
58    ///
59    /// The caller must ensure that the [`Assignment`] has a large enough size, so that the variable index of `lit` is at most that size.
60    ///
61    /// Using a `lit` with variable index of at least the size of [`Assignment`] is undefined behaviour.
62    #[inline]
63    pub unsafe fn set_lit_value_unchecked(&mut self, lit: Lit, value: V::Value) {
64        debug_assert!(lit.get_var() < self.assignment.len());
65        if lit.is_negated() {
66            self.assignment
67                .get_unchecked_mut(lit.get_var())
68                .set_value(value.negate());
69        } else {
70            self.assignment
71                .get_unchecked_mut(lit.get_var())
72                .set_value(value);
73        }
74    }
75
76    /// Get the value of a [`Lit`]. Hence, if [`Lit`] is negated, then value assigned to its variable is negated.
77    #[inline]
78    pub fn get_lit_value(&self, lit: Lit) -> V::Value {
79        if let Some(value) = self.assignment.get(lit.get_var()) {
80            if lit.is_negated() {
81                value.get_value().negate()
82            } else {
83                value.get_value()
84            }
85        } else {
86            V::Value::default()
87        }
88    }
89
90    /// Same as `get_lit_value` but without bounds check.
91    ///
92    /// # Safety
93    ///
94    /// The caller must ensure that the [`Assignment`] has a large enough size, so that the variable index of `lit` is at most that size.
95    ///
96    /// Using a `lit` with variable index of at least the size of [`Assignment`] is undefined behaviour.
97    #[inline]
98    pub unsafe fn get_lit_value_unchecked(&self, lit: Lit) -> V::Value {
99        debug_assert!(lit.get_var() < self.assignment.len());
100        let value = self.assignment.get_unchecked(lit.get_var()).get_value();
101        if lit.is_negated() {
102            value.negate()
103        } else {
104            value
105        }
106    }
107
108    /// Reset the [`Assignment`] to its default values.
109    #[inline]
110    pub fn reset(&mut self) {
111        self.assignment.fill(Default::default());
112    }
113
114    /// Returns the number of variables in the [`Assignment`] no matter their value.
115    #[inline]
116    pub fn len(&self) -> usize {
117        self.assignment.len()
118    }
119
120    /// Returns `true` if the assignment is empty, i.e., it contains no variables, neither unassigned nor assigned.
121    #[inline]
122    pub fn is_empty(&self) -> bool {
123        self.assignment.is_empty()
124    }
125}
126
127impl Assignment<BooleanVar> {
128    /// Create an [`Assignment`] from a [`Vec<Lit>`].
129    ///
130    /// Returns `Some(assignment)` if the `literals` are consistent, i.e., [`Vec<Lit>`] does not contain a literal and its negation. If `literals` is not consistent, then [`None`] is returned.
131    #[inline]
132    pub fn from(literals: &Vec<Lit>) -> Option<Self> {
133        let mut assignment = Assignment::with_size(literals.len());
134        for &lit in literals {
135            if lit.get_var() >= assignment.len() {
136                assignment.resize(2 * lit.get_var());
137            }
138            if unsafe { assignment.get_lit_value_unchecked(lit) } == BoolValue::Assigned(false) {
139                return None;
140            }
141            unsafe { assignment.set_lit_value_unchecked(lit, BoolValue::Assigned(true)) };
142        }
143        Some(assignment)
144    }
145
146    /// Test if the variable is unassigned.
147    ///
148    /// Returns `true` if the variable matches `BoolValue::Unassigned`.
149    #[inline]
150    pub fn is_unassigned(&self, var: VarIdx) -> bool {
151        matches!(self.assignment[var].get_value(), BoolValue::Unassigned)
152    }
153
154    /// Test if the variable is assigned to some value.
155    ///
156    /// Returns `true` if the variable matches `BoolValue::Assigned(_)`.
157    #[inline]
158    pub fn is_assigned(&self, var: VarIdx) -> bool {
159        matches!(self.assignment[var].get_value(), BoolValue::Assigned(_))
160    }
161}
162
163impl ToPrettyString for Assignment<BooleanVar> {
164    fn to_pretty_string(&self, var_names: &VarNameManager) -> String {
165        let mut output = String::with_capacity(8 * self.len());
166        for (idx, var) in self.assignment.iter().enumerate() {
167            match var.get_value() {
168                BoolValue::Assigned(true) => {
169                    output.push_str(var_names.get_name(idx));
170                    output.push(' ');
171                }
172                BoolValue::Assigned(false) => {
173                    output.push('~');
174                    output.push_str(var_names.get_name(idx));
175                    output.push(' ');
176                }
177                BoolValue::Unassigned => {}
178            }
179        }
180        output.pop();
181        output
182    }
183}
184
185impl Substitutable for Assignment<BooleanVar> {
186    fn get_lit(&self, lit: Lit) -> Option<SubstitutionValue> {
187        match unsafe { self.get_lit_value_unchecked(lit) } {
188            BoolValue::Unassigned => None,
189            BoolValue::Assigned(true) => Some(SubstitutionValue::TRUE),
190            BoolValue::Assigned(false) => Some(SubstitutionValue::FALSE),
191        }
192    }
193}
194
195impl Display for Assignment<BooleanVar> {
196    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
197        for (idx, var) in self.assignment.iter().enumerate() {
198            match var.get_value() {
199                BoolValue::Unassigned => writeln!(f, "{}: -", idx + 1)?,
200                BoolValue::Assigned(val) => writeln!(f, "{}: {}", idx + 1, val)?,
201            }
202        }
203        Ok(())
204    }
205}
veripb_formula/assignment.rs

veripb_formula/
assignment.rs
