Add support for parsing negative solution values

src/context.rs

@@ -659,6 +659,186 @@ impl Context {
         self.arena.get(expr)
     }
 
+    /// Get the atom data for the given s-expression.
+    ///
+    /// This allows you to inspect s-expressions. If the s-expression is not an
+    /// atom this function returns `None`.
+    ///
+    /// You may only pass in `SExpr`s that were created by this
+    /// `Context`. Failure to do so is safe, but may trigger a panic or return
+    /// invalid data.
+    pub fn get_atom(&self, expr: SExpr) -> Option<&str> {
+        self.arena.get_atom(expr)
+    }
+
+    /// Get the string data for the given s-expression.
+    ///
+    /// This allows you to inspect s-expressions. If the s-expression is not an
+    /// string this function returns `None`.
+    ///
+    /// You may only pass in `SExpr`s that were created by this
+    /// `Context`. Failure to do so is safe, but may trigger a panic or return
+    /// invalid data.
+    pub fn get_str(&self, expr: SExpr) -> Option<&str> {
+        self.arena.get_str(expr)
+    }
+
+    /// Get the list data for the given s-expression.
+    ///
+    /// This allows you to inspect s-expressions.If the s-expression is not an
+    /// list this function returns `None`.
+    ///
+    /// You may only pass in `SExpr`s that were created by this
+    /// `Context`. Failure to do so is safe, but may trigger a panic or return
+    /// invalid data.
+    pub fn get_list(&self, expr: SExpr) -> Option<&[SExpr]> {
+        self.arena.get_list(expr)
+    }
+
+    /// Get the data for the given s-expression as an `u8`.
+    ///
+    /// This allows you to inspect s-expressions. If the s-expression is not an
+    /// cannot be parsed into an `u8` this function returns `None`.
+    ///
+    /// You may only pass in `SExpr`s that were created by this
+    /// `Context`. Failure to do so is safe, but may trigger a panic or return
+    /// invalid data.
+    pub fn get_u8(&self, expr: SExpr) -> Option<u8> {
+        self.arena.get_t(expr)
+    }
+
+    /// Get the data for the given s-expression as an `u16`.
+    ///
+    /// This allows you to inspect s-expressions. If the s-expression is not an
+    /// cannot be parsed into an `u16` this function returns `None`.
+    ///
+    /// You may only pass in `SExpr`s that were created by this
+    /// `Context`. Failure to do so is safe, but may trigger a panic or return
+    /// invalid data.
+    pub fn get_u16(&self, expr: SExpr) -> Option<u16> {
+        self.arena.get_t(expr)
+    }
+
+    /// Get the data for the given s-expression as an `u32`.
+    ///
+    /// This allows you to inspect s-expressions. If the s-expression is not an
+    /// cannot be parsed into an `u32` this function returns `None`.
+    ///
+    /// You may only pass in `SExpr`s that were created by this
+    /// `Context`. Failure to do so is safe, but may trigger a panic or return
+    /// invalid data.
+    pub fn get_u32(&self, expr: SExpr) -> Option<u32> {
+        self.arena.get_t(expr)
+    }
+
+    /// Get the data for the given s-expression as an `u64`.
+    ///
+    /// This allows you to inspect s-expressions. If the s-expression is not an
+    /// cannot be parsed into an `u64` this function returns `None`.
+    ///
+    /// You may only pass in `SExpr`s that were created by this
+    /// `Context`. Failure to do so is safe, but may trigger a panic or return
+    /// invalid data.
+    pub fn get_u64(&self, expr: SExpr) -> Option<u64> {
+        self.arena.get_t(expr)
+    }
+
+    /// Get the data for the given s-expression as an `u128`.
+    ///
+    /// This allows you to inspect s-expressions. If the s-expression is not an
+    /// cannot be parsed into an `u128` this function returns `None`.
+    ///
+    /// You may only pass in `SExpr`s that were created by this
+    /// `Context`. Failure to do so is safe, but may trigger a panic or return
+    /// invalid data.
+    pub fn get_u128(&self, expr: SExpr) -> Option<u128> {
+        self.arena.get_t(expr)
+    }
+
+    /// Get the data for the given s-expression as an `usize`.
+    ///
+    /// This allows you to inspect s-expressions. If the s-expression is not an
+    /// cannot be parsed into an `usize` this function returns `None`.
+    ///
+    /// You may only pass in `SExpr`s that were created by this
+    /// `Context`. Failure to do so is safe, but may trigger a panic or return
+    /// invalid data.
+    pub fn get_usize(&self, expr: SExpr) -> Option<usize> {
+        self.arena.get_t(expr)
+    }
+
+    /// Get the data for the given s-expression as an `i8`.
+    ///
+    /// This allows you to inspect s-expressions. If the s-expression is not an
+    /// cannot be parsed into an `i8` this function returns `None`.
+    ///
+    /// You may only pass in `SExpr`s that were created by this
+    /// `Context`. Failure to do so is safe, but may trigger a panic or return
+    /// invalid data.
+    pub fn get_i8(&self, expr: SExpr) -> Option<i8> {
+        self.arena.get_t(expr)
+    }
+
+    /// Get the data for the given s-expression as an `i16`.
+    ///
+    /// This allows you to inspect s-expressions. If the s-expression is not an
+    /// cannot be parsed into an `i16` this function returns `None`.
+    ///
+    /// You may only pass in `SExpr`s that were created by this
+    /// `Context`. Failure to do so is safe, but may trigger a panic or return
+    /// invalid data.
+    pub fn get_i16(&self, expr: SExpr) -> Option<i16> {
+        self.arena.get_t(expr)
+    }
+
+    /// Get the data for the given s-expression as an `i32`.
+    ///
+    /// This allows you to inspect s-expressions. If the s-expression is not an
+    /// cannot be parsed into an `i32` this function returns `None`.
+    ///
+    /// You may only pass in `SExpr`s that were created by this
+    /// `Context`. Failure to do so is safe, but may trigger a panic or return
+    /// invalid data.
+    pub fn get_i32(&self, expr: SExpr) -> Option<i32> {
+        self.arena.get_t(expr)
+    }
+
+    /// Get the data for the given s-expression as an `i64`.
+    ///
+    /// This allows you to inspect s-expressions. If the s-expression is not an
+    /// cannot be parsed into an `i64` this function returns `None`.
+    ///
+    /// You may only pass in `SExpr`s that were created by this
+    /// `Context`. Failure to do so is safe, but may trigger a panic or return
+    /// invalid data.
+    pub fn get_i64(&self, expr: SExpr) -> Option<i64> {
+        self.arena.get_t(expr)
+    }
+
+    /// Get the data for the given s-expression as an `i128`.
+    ///
+    /// This allows you to inspect s-expressions. If the s-expression is not an
+    /// cannot be parsed into an `i128` this function returns `None`.
+    ///
+    /// You may only pass in `SExpr`s that were created by this
+    /// `Context`. Failure to do so is safe, but may trigger a panic or return
+    /// invalid data.
+    pub fn get_i128(&self, expr: SExpr) -> Option<i128> {
+        self.arena.get_t(expr)
+    }
+
+    /// Get the data for the given s-expression as an `isize`.
+    ///
+    /// This allows you to inspect s-expressions. If the s-expression is not an
+    /// cannot be parsed into an `isize` this function returns `None`.
+    ///
+    /// You may only pass in `SExpr`s that were created by this
+    /// `Context`. Failure to do so is safe, but may trigger a panic or return
+    /// invalid data.
+    pub fn get_isize(&self, expr: SExpr) -> Option<isize> {
+        self.arena.get_t(expr)
+    }
+
     /// Access "known" atoms.
     ///
     /// This lets you skip the is-it-already-interned-or-not checks and hash map

src/sexpr.rs

@@ -213,22 +213,118 @@ impl Arena {
             unreachable!()
         }
     }
+
+    pub fn get_atom(&self, expr: SExpr) -> Option<&str> {
+        if !expr.is_atom() {
+            return None;
+        }
+
+        let inner = self.0.borrow();
+        // Safety argument: the data will live as long as the containing context, and is
+        // immutable once it's inserted, so using the lifteime of the Arena is acceptable.
+        let data = unsafe { std::mem::transmute(inner.strings[expr.index()].as_str()) };
+        Some(data)
+    }
+
+    pub fn get_str(&self, expr: SExpr) -> Option<&str> {
+        if !expr.is_string() {
+            return None;
+        }
+
+        let inner = self.0.borrow();
+        // Safety argument: the data will live as long as the containing context, and is
+        // immutable once it's inserted, so using the lifteime of the Arena is acceptable.
+        let data = unsafe { std::mem::transmute(inner.strings[expr.index()].as_str()) };
+        Some(data)
+    }
+
+    pub fn get_list(&self, expr: SExpr) -> Option<&[SExpr]> {
+        if !expr.is_list() {
+            return None;
+        }
+
+        let inner = self.0.borrow();
+        // Safety argument: the data will live as long as the containing context, and is
+        // immutable once it's inserted, so using the lifteime of the Arena is acceptable.
+        let data = unsafe { std::mem::transmute(inner.lists[expr.index()].as_slice()) };
+        return Some(data);
+    }
+
+    pub(crate) fn get_t<T: TryParseInt>(&self, expr: SExpr) -> Option<T> {
+        let inner = self.0.borrow();
+
+        if expr.is_atom() {
+            let data = inner.strings[expr.index()].as_str();
+            return T::try_parse_t(data, false);
+        }
+
+        if expr.is_list() {
+            let data = inner.lists[expr.index()].as_slice();
+
+            if data.len() != 2 || data.iter().any(|expr| !expr.is_atom()) {
+                return None;
+            }
+
+            let is_negated = match inner.strings[data[0].index()].as_str() {
+                "-" => true,
+                "+" => false,
+                _ => return None,
+            };
+
+            let r_data = inner.strings[data[1].index()].as_str();
+
+            return T::try_parse_t(r_data, is_negated);
+        }
+
+        None
+    }
+}
+
+pub(crate) trait TryParseInt: Sized {
+    fn try_parse_t(a: &str, negate: bool) -> Option<Self>;
+}
+
+macro_rules! impl_get_int {
+    ( $( $ty:ty )* ) => {
+        $(
+            impl TryParseInt for $ty {
+                fn try_parse_t(a: &str, negate: bool) -> Option<Self> {
+                    let x = if let Some(a) = a.strip_prefix("#x") {
+                        <$ty>::from_str_radix(a, 16).ok()?
+                    } else if let Some(a) = a.strip_prefix("#b") {
+                        <$ty>::from_str_radix(a , 2).ok()?
+                    } else {
+                        a.parse::<$ty>().ok()?
+                    };
+
+                    if negate {
+                        return x.checked_neg();
+                    }
+
+                    Some(x)
+                }
+            }
+        )*
+    };
 }
 
+impl_get_int!(u8 u16 u32 u64 u128 usize i8 i16 i32 i64 i128 isize);
+
 /// The data contents of an [`SExpr`][crate::SExpr].
 ///
 /// ## Converting `SExprData` to an Integer
 ///
-/// There are `TryFrom<SExprData>` implementations for common integer types that
-/// you can use:
+/// There are a variety of `Context::get_*` helper methods (such as for example
+/// [`Context::get_u8`] and [`Context::get_i64`]) to parse integers out of
+/// s-expressions. For example, you can use:
 ///
 /// ```
 /// let mut ctx = easy_smt::ContextBuilder::new().build().unwrap();
 ///
 /// let neg_one = ctx.binary(8, -1_i8);
 /// assert_eq!(ctx.display(neg_one).to_string(), "#b11111111");
 ///
-/// let x = u8::try_from(ctx.get(neg_one)).unwrap();
+/// let x = ctx.get_u8(neg_one).unwrap();
 /// assert_eq!(x, 0xff);
 /// ```
 #[derive(Debug)]
@@ -652,7 +748,8 @@ mod tests {
             .expect_err("Single atom doesn't close a list")
             .expect_more();
 
-        let expr = p.parse(&arena, ")")
+        let expr = p
+            .parse(&arena, ")")
             .expect("Closing paren should finish the parse");
 
         let SExprData::List(es) = arena.get(expr) else {