1use 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#[derive(Debug, PartialEq, Eq, Clone, Copy, PartialOrd, Ord)]
12pub struct Variable(pub u32);
13
14#[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, PartialOrd, Ord, Default)]
16pub struct Literal {
17 pub encoding: u32,
23}
24
25impl Variable {
26 pub fn new(value: u32) -> Variable {
27 Variable(value)
28 }
29 pub fn literal(self) -> Literal {
31 requires!(i32::try_from(self.0).is_ok());
32 Literal::new(self.0 as i32)
33 }
34 pub fn array_size_for_variables(self) -> usize {
37 self.as_offset() + 1
38 }
39 pub fn array_size_for_literals(self) -> usize {
42 2 * (self.as_offset() + 1)
43 }
44}
45
46impl Offset for Variable {
48 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 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 pub const fn from_raw(encoding: u32) -> Literal {
72 Literal { encoding }
73 }
74
75 pub const TOP: Literal = Literal { encoding: 0 };
77 pub const BOTTOM: Literal = Literal { encoding: 1 };
79
80 pub const NEVER_READ: Literal = Literal {
82 encoding: u32::max_value(),
83 };
84
85 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 pub const fn variable(self) -> Variable {
105 Variable(self.encoding / 2)
106 }
107 pub fn is_constant(self) -> bool {
116 self.encoding <= 1
117 }
118 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 pub const fn is_zero(self) -> bool {
140 self.encoding == 0
141 }
142}
143
144impl Offset for Literal {
146 fn as_offset(&self) -> usize {
147 self.encoding as usize
148 }
149}
150
151impl ops::Neg for Literal {
162 type Output = Literal;
163 fn neg(self) -> Literal {
164 Literal {
165 encoding: self.encoding ^ 1,
166 }
167 }
168}
169
170impl 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
222struct 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}