Adding support for Reals (#50)

pleich · web-flow · commit e4b2063cec12 · 2025-07-22T19:20:28.000-07:00
This PR would add support for `Real` values. In more detail: 
- It adds the type `real`, with the helper method `real_sort`
- It adds the method `con_to_real` for converting `Int` values to reals
- It adds the method `rdiv` which corresponds to division for reals
(i.e. `/`)
- It adds support for parsing real valued solutions (see below) 


## On Parsing `Real` Solutions

As it turns out, parsing the satisfying assignment for solutions to real
values is not as straightforward. In many cases, the SMT solver will
represent a solution as a fraction, e.g. if it assigns the value `2.5`
to a variable, when asked for the solution, it will return it as the
expression `/ 5.0 2.0`.

For my project, I am fine with the loss of precision when evaluating
this expression to an `f32` or `f64`. The `get_f32` and `get_f64`
methods in this PR will evaluate this expression and return the result.
However, if this is not desired, the next section discusses possible
alternatives.

I have written a small test that should check all possible variations of
solutions that can be returned by the SMT solver:
```rust 
#[test]
fn test_real_numbers() {
    let mut ctx = ContextBuilder::new()
        .solver("z3")
        .solver_args(["-smt2", "-in"])
        .build()
        .unwrap();

    let x = ctx.declare_const("x", ctx.real_sort()).unwrap();
    // x == 2.0
    ctx.assert(ctx.eq(x, ctx.decimal(2.0))).unwrap();
    assert_eq!(ctx.check().unwrap(), Response::Sat);
    let solution = ctx.get_value(vec![x]).unwrap();
    let sol = ctx.get_f64(solution[0].1).unwrap();
    // Z3 returns `2.0`
    assert!(sol == 2.0, "Expected solution to be 2.5, got {}", sol);

    let y = ctx.declare_const("y", ctx.real_sort()).unwrap();
    // y == -2.0
    ctx.assert(ctx.eq(y, ctx.decimal(-2.0))).unwrap();
    assert_eq!(ctx.check().unwrap(), Response::Sat);
    let solution = ctx.get_value(vec![y]).unwrap();
    let sol = ctx.get_f64(solution[0].1).unwrap();
    // Z3 returns `- 2.0`
    assert!(sol == -2.0, "Expected solution to be 2.5, got {}", sol);

    let z = ctx.declare_const("z", ctx.real_sort()).unwrap();
    // z == 2.5 / 1.0
    ctx.assert(ctx.eq(z, ctx.rdiv(ctx.decimal(2.5), ctx.decimal(1.0))))
        .unwrap();
    assert_eq!(ctx.check().unwrap(), Response::Sat);
    let solution = ctx.get_value(vec![z]).unwrap();
    let sol = ctx.get_f64(solution[0].1).unwrap();
    // Z3 returns `(/ 5.0 2.0)`
    assert!(sol == 2.5, "Expected solution to be 2.5, got {}", sol);

    let a = ctx.declare_const("a", ctx.real_sort()).unwrap();
    // a == 2.5 / -1.0
    ctx.assert(ctx.eq(a, ctx.rdiv(ctx.decimal(2.5), ctx.decimal(-1.0))))
        .unwrap();
    assert_eq!(ctx.check().unwrap(), Response::Sat);
    let solution = ctx.get_value(vec![a]).unwrap();
    let sol = ctx.get_f64(solution[0].1).unwrap();
    // Z3 returns `(- (/ 5.0 2.0))`
    assert!(sol == -2.5, "Expected solution to be -2.5, got {}", sol);
}
```


### Possible Alternatives

If the loss of precision that occurs when parsing the solution is not
desired, I see two alternatives:
- Explicitly have functions like `get_numerator` and `get_denominator` 
- Defining / importing a fractional type (possibly hidden behind a
feature flag)



Let me know your thoughts!
diff --git a/src/context.rs b/src/context.rs
@@ -704,7 +704,7 @@ impl Context {
     /// `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)
+        self.arena.get_i(expr)
     }
 
     /// Get the data for the given s-expression as an `u16`.
@@ -716,7 +716,7 @@ impl Context {
     /// `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)
+        self.arena.get_i(expr)
     }
 
     /// Get the data for the given s-expression as an `u32`.
@@ -728,7 +728,7 @@ impl Context {
     /// `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)
+        self.arena.get_i(expr)
     }
 
     /// Get the data for the given s-expression as an `u64`.
@@ -740,7 +740,7 @@ impl Context {
     /// `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)
+        self.arena.get_i(expr)
     }
 
     /// Get the data for the given s-expression as an `u128`.
@@ -752,7 +752,7 @@ impl Context {
     /// `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)
+        self.arena.get_i(expr)
     }
 
     /// Get the data for the given s-expression as an `usize`.
@@ -764,7 +764,7 @@ impl Context {
     /// `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)
+        self.arena.get_i(expr)
     }
 
     /// Get the data for the given s-expression as an `i8`.
@@ -776,7 +776,7 @@ impl Context {
     /// `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)
+        self.arena.get_i(expr)
     }
 
     /// Get the data for the given s-expression as an `i16`.
@@ -788,7 +788,7 @@ impl Context {
     /// `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)
+        self.arena.get_i(expr)
     }
 
     /// Get the data for the given s-expression as an `i32`.
@@ -800,7 +800,7 @@ impl Context {
     /// `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)
+        self.arena.get_i(expr)
     }
 
     /// Get the data for the given s-expression as an `i64`.
@@ -812,7 +812,7 @@ impl Context {
     /// `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)
+        self.arena.get_i(expr)
     }
 
     /// Get the data for the given s-expression as an `i128`.
@@ -824,7 +824,7 @@ impl Context {
     /// `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)
+        self.arena.get_i(expr)
     }
 
     /// Get the data for the given s-expression as an `isize`.
@@ -836,7 +836,30 @@ impl Context {
     /// `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)
+        self.arena.get_i(expr)
+    }
+
+    /// Get the data for the given s-expression as a `f32`.
+    ///
+    /// This allows you to inspect s-expressions. If the s-expression is not an
+    /// cannot be parsed into an `f32` 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_f32(&self, expr: SExpr) -> Option<f32> {
+        self.arena.get_f(expr)
+    }
+
+    /// Get the data for the given s-expression as a `f64`.
+    ///
+    /// This allows you to inspect s-expressions. If the s-expression is not an
+    /// cannot be parsed into an `f64` 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_f64(&self, expr: SExpr) -> Option<f64> {
+        self.arena.get_f(expr)
     }
 
     /// Access "known" atoms.
@@ -997,6 +1020,19 @@ impl Context {
     chainable!(gte, gte_many, gte);
 }
 
+/// # Real Helpers
+///
+/// These methods help you construct s-expressions for various real operations.
+impl Context {
+    /// The `Real` sort.
+    pub fn real_sort(&self) -> SExpr {
+        self.atoms.real
+    }
+
+    left_assoc!(rdiv, rdiv_many, slash);
+    unary!(conv_to_real, to_real);
+}
+
 /// # Array Helpers
 ///
 /// These methods help you construct s-expressions for various array operations.
diff --git a/src/known_atoms.rs b/src/known_atoms.rs
@@ -48,6 +48,9 @@ macro_rules! for_each_known_atom {
             lt: "<";
             gte: ">=";
             gt: ">";
+            real: "Real";
+            slash: "/";
+            to_real: "to_real";
             array: "Array";
             select: "select";
             store: "store";
diff --git a/src/sexpr.rs b/src/sexpr.rs
@@ -1,4 +1,4 @@
-use std::{cell::RefCell, collections::HashMap};
+use std::{cell::RefCell, collections::HashMap, ops::Div};
 
 #[cfg(debug_assertions)]
 #[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
@@ -250,7 +250,7 @@ impl Arena {
         return Some(data);
     }
 
-    pub(crate) fn get_t<T: TryParseInt>(&self, expr: SExpr) -> Option<T> {
+    pub(crate) fn get_i<T: TryParseInt>(&self, expr: SExpr) -> Option<T> {
         let inner = self.0.borrow();
 
         if expr.is_atom() {
@@ -278,6 +278,58 @@ impl Arena {
 
         None
     }
+
+    pub(crate) fn get_f<T: TryParseFloat + Div<Output = T>>(&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 mut data = inner.lists[expr.index()].as_slice();
+
+            if !([1, 2, 3].contains(&data.len())) || !data[0].is_atom() {
+                return None;
+            }
+
+            let mut index = 0;
+            let is_negated = match inner.strings[data[0].index()].as_str() {
+                "-" => {
+                    index += 1;
+                    true
+                }
+                "+" => {
+                    index += 1;
+                    false
+                }
+                _ => false,
+            };
+
+            // Solution could be of the form  `(- (/ 1.0 2.0))`
+            if data.len() == 2 && !data[1].is_atom() {
+                data = inner.lists[data[1].index()].as_slice();
+                index = 0;
+            }
+
+            let data = &data[index..];
+
+            if data.len() == 1 {
+                return T::try_parse_t(inner.strings[data[0].index()].as_str(), is_negated);
+            }
+
+            // Solution returned is a fraction of the form `(/ 1.0 2.0)`
+            if data.len() == 3 && inner.strings[data[0].index()].as_str() == "/" {
+                let numerator =
+                    T::try_parse_t(inner.strings[data[1].index()].as_str(), is_negated)?;
+                let denominator = T::try_parse_t(inner.strings[data[2].index()].as_str(), false)?;
+                return Some(numerator / denominator);
+            }
+        }
+
+        None
+    }
 }
 
 pub(crate) trait TryParseInt: Sized {
@@ -310,6 +362,30 @@ macro_rules! impl_get_int {
 
 impl_get_int!(u8 u16 u32 u64 u128 usize i8 i16 i32 i64 i128 isize);
 
+pub(crate) trait TryParseFloat: Sized {
+    fn try_parse_t(a: &str, negate: bool) -> Option<Self>;
+}
+
+macro_rules! impl_get_float {
+    ( $( $ty:ty )* ) => {
+        $(
+            impl TryParseFloat for $ty {
+                fn try_parse_t(a: &str, negate: bool) -> Option<Self> {
+                    let mut x = a.parse::<$ty>().ok()?;
+
+                    if negate {
+                        x = -x;
+                    }
+
+                    Some(x)
+                }
+            }
+        )*
+    };
+}
+
+impl_get_float!(f32 f64);
+
 /// The data contents of an [`SExpr`][crate::SExpr].
 ///
 /// ## Converting `SExprData` to an Integer
diff --git a/tests/real_numbers.rs b/tests/real_numbers.rs
@@ -0,0 +1,48 @@
+use easy_smt::{ContextBuilder, Response};
+
+#[test]
+fn test_real_numbers() {
+    let mut ctx = ContextBuilder::new()
+        .solver("z3")
+        .solver_args(["-smt2", "-in"])
+        .build()
+        .unwrap();
+
+    let x = ctx.declare_const("x", ctx.real_sort()).unwrap();
+    // x == 2.0
+    ctx.assert(ctx.eq(x, ctx.decimal(2.0))).unwrap();
+    assert_eq!(ctx.check().unwrap(), Response::Sat);
+    let solution = ctx.get_value(vec![x]).unwrap();
+    let sol = ctx.get_f64(solution[0].1).unwrap();
+    // Z3 returns `2.0`
+    assert_eq!(sol, 2.0);
+
+    let y = ctx.declare_const("y", ctx.real_sort()).unwrap();
+    // y == -2.0
+    ctx.assert(ctx.eq(y, ctx.decimal(-2.0))).unwrap();
+    assert_eq!(ctx.check().unwrap(), Response::Sat);
+    let solution = ctx.get_value(vec![y]).unwrap();
+    let sol = ctx.get_f64(solution[0].1).unwrap();
+    // Z3 returns `- 2.0`
+    assert_eq!(sol, -2.0);
+
+    let z = ctx.declare_const("z", ctx.real_sort()).unwrap();
+    // z == 2.5 / 1.0
+    ctx.assert(ctx.eq(z, ctx.rdiv(ctx.decimal(2.5), ctx.decimal(1.0))))
+        .unwrap();
+    assert_eq!(ctx.check().unwrap(), Response::Sat);
+    let solution = ctx.get_value(vec![z]).unwrap();
+    let sol = ctx.get_f64(solution[0].1).unwrap();
+    // Z3 returns `(/ 5.0 2.0)`
+    assert_eq!(sol, 2.5);
+
+    let a = ctx.declare_const("a", ctx.real_sort()).unwrap();
+    // a == 2.5 / -1.0
+    ctx.assert(ctx.eq(a, ctx.rdiv(ctx.decimal(2.5), ctx.decimal(-1.0))))
+        .unwrap();
+    assert_eq!(ctx.check().unwrap(), Response::Sat);
+    let solution = ctx.get_value(vec![a]).unwrap();
+    let sol = ctx.get_f64(solution[0].1).unwrap();
+    // Z3 returns `(- (/ 5.0 2.0))`
+    assert_eq!(sol, -2.5);
+}
