rate_common/
literal.rs

1//! Variable and literal representations
2
3use crate::memory::Offset;
4use serde::{
5    de::{self, Visitor},
6    Deserialize, Deserializer, Serialize, Serializer,
7};
8use std::{convert::TryFrom, fmt, fmt::Display, ops};
9
10/// A variable, encoded as 32 bit unsigned integer.
11#[derive(Debug, PartialEq, Eq, Clone, Copy, PartialOrd, Ord)]
12pub struct Variable(pub u32);
13
14/// A literal, encoded as 32 bit unsigned integer.
15#[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, PartialOrd, Ord, Default)]
16pub struct Literal {
17    /// We use a sign-magnitude encoding (also used by AIGER and others). This
18    /// allows us to directly use this as offset.
19    ///
20    /// - The least significant bit is the sign (negative if it is 1).
21    /// - The remaining bits encode the variable.
22    pub encoding: u32,
23}
24
25impl Variable {
26    pub fn new(value: u32) -> Variable {
27        Variable(value)
28    }
29    /// Convert a variable to a positive literal.
30    pub fn literal(self) -> Literal {
31        requires!(i32::try_from(self.0).is_ok());
32        Literal::new(self.0 as i32)
33    }
34    /// The size of an array that can contain variables up to and including
35    /// `self`.
36    pub fn array_size_for_variables(self) -> usize {
37        self.as_offset() + 1
38    }
39    /// The size of an array that can contain literals up to and including
40    /// `-self.literal()`.
41    pub fn array_size_for_literals(self) -> usize {
42        2 * (self.as_offset() + 1)
43    }
44}
45
46/// Enable as array index.
47impl Offset for Variable {
48    /// We simply use the variable index, so offset 0 will be generally unused.
49    fn as_offset(&self) -> usize {
50        requires!(usize::try_from(self.0).is_ok());
51        self.0 as usize
52    }
53}
54
55impl Display for Variable {
56    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
57        write!(f, "{}", self.literal())
58    }
59}
60
61impl Literal {
62    /// Create a literal from the signed representation used in DIMACS.
63    pub fn new(value: i32) -> Literal {
64        requires!(value != i32::min_value());
65        requires!((value.abs() as u32) < u32::pow(2, 31));
66        Literal {
67            encoding: (value.abs() as u32) * 2 + ((value < 0) as u32),
68        }
69    }
70    /// Create a literal without conversion.
71    pub const fn from_raw(encoding: u32) -> Literal {
72        Literal { encoding }
73    }
74
75    /// Encoded as 0.
76    pub const TOP: Literal = Literal { encoding: 0 };
77    /// Encoded as 1.
78    pub const BOTTOM: Literal = Literal { encoding: 1 };
79
80    /// Sentinel value of  `u32::max_value()` to detect errors.
81    pub const NEVER_READ: Literal = Literal {
82        encoding: u32::max_value(),
83    };
84
85    /// DIMACS representation.
86    /// # Examples
87    /// ```
88    /// use rate_common::literal::Literal;
89    /// assert_eq!(Literal::new(-1).decode(), -1);
90    /// ```
91    pub fn decode(self) -> i32 {
92        let magnitude = self.variable().0 as i32;
93        if self.encoding & 1 != 0 {
94            -magnitude
95        } else {
96            magnitude
97        }
98    }
99    /// # Examples
100    /// ```
101    /// use rate_common::literal::{Literal, Variable};
102    /// assert_eq!(Literal::new(-3).variable(), Variable(3));
103    /// ```
104    pub const fn variable(self) -> Variable {
105        Variable(self.encoding / 2)
106    }
107    /// True if it is [`Literal::TOP`] or [`Literal::BOTTOM`].
108    ///
109    /// # Examples
110    /// ```
111    /// use rate_common::literal::Literal;
112    /// assert!(Literal::TOP.is_constant());
113    /// assert!(!Literal::new(-3).is_constant());
114    /// ```
115    pub fn is_constant(self) -> bool {
116        self.encoding <= 1
117    }
118    /// Produce all literals from 1 and -1 up to the given variable.
119    ///
120    /// # Examples
121    ///
122    /// ```
123    /// use rate_common::literal::{Literal, Variable};
124    /// assert_eq!(Literal::all(Variable(2)).collect::<Vec<_>>(),
125    ///           vec!(Literal::new(1), Literal::new(-1), Literal::new(2), Literal::new(-2)));
126    /// ```
127    pub fn all(maxvar: Variable) -> impl Iterator<Item = Literal> {
128        let first = Variable(1).literal().encoding;
129        let last = maxvar.literal().encoding;
130        (first..last + 2).map(Literal::from_raw)
131    }
132    /// # Examples
133    ///
134    /// ```
135    /// use rate_common::literal::Literal;
136    /// assert!(Literal::new(0).is_zero());
137    /// assert!(!Literal::new(1).is_zero());
138    /// ```
139    pub const fn is_zero(self) -> bool {
140        self.encoding == 0
141    }
142}
143
144/// Enable as array index.
145impl Offset for Literal {
146    fn as_offset(&self) -> usize {
147        self.encoding as usize
148    }
149}
150
151// Note: it might be more idiomatic to use [`std::ops::Not`] (`!`).
152/// Negate a literal with operator `-`.
153///
154///
155/// # Examples
156///
157/// ```
158/// use rate_common::literal::Literal;
159/// assert!(-Literal::TOP == Literal::BOTTOM);
160/// ```
161impl ops::Neg for Literal {
162    type Output = Literal;
163    fn neg(self) -> Literal {
164        Literal {
165            encoding: self.encoding ^ 1,
166        }
167    }
168}
169
170/// # Examples
171///
172/// ```
173/// use rate_common::literal::Literal;
174/// assert_eq!(format!("{}", Literal::TOP), "+0");
175/// assert_eq!(format!("{}", Literal::BOTTOM), "-0");
176/// assert_eq!(format!("{}", Literal::new(11)), "11");
177/// ```
178impl Display for Literal {
179    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
180        write!(
181            f,
182            "{}{}",
183            if self == &Literal::TOP {
184                "+"
185            } else if self == &Literal::BOTTOM {
186                "-"
187            } else {
188                ""
189            },
190            self.decode()
191        )
192    }
193}
194
195impl Serialize for Literal {
196    fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
197    where
198        S: Serializer,
199    {
200        requires!(
201            !self.is_constant(),
202            "serialization of boolean constants is not supported"
203        );
204        serializer.serialize_i32(self.decode())
205    }
206}
207
208impl<'de> Deserialize<'de> for Literal {
209    fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
210    where
211        D: Deserializer<'de>,
212    {
213        let result = Literal::new(deserializer.deserialize_i32(I32Visitor)?);
214        requires!(
215            !result.is_constant(),
216            "deserialization of boolean constants is not supported"
217        );
218        Ok(result)
219    }
220}
221
222/// A deserializer for integers.
223///
224/// Used in the TOML parser in `sick-check`.
225struct I32Visitor;
226
227impl<'de> Visitor<'de> for I32Visitor {
228    type Value = i32;
229
230    fn expecting(&self, formatter: &mut fmt::Formatter) -> fmt::Result {
231        formatter.write_str("an integer between -2^31 and 2^31")
232    }
233
234    fn visit_i8<E>(self, value: i8) -> Result<Self::Value, E>
235    where
236        E: de::Error,
237    {
238        Ok(i32::from(value))
239    }
240
241    fn visit_i32<E>(self, value: i32) -> Result<Self::Value, E>
242    where
243        E: de::Error,
244    {
245        Ok(value)
246    }
247
248    fn visit_i64<E>(self, value: i64) -> Result<Self::Value, E>
249    where
250        E: de::Error,
251    {
252        use std::i32;
253        if value >= i64::from(i32::MIN) && value <= i64::from(i32::MAX) {
254            Ok(value as i32)
255        } else {
256            Err(E::custom(format!("i32 out of range: {}", value)))
257        }
258    }
259}