Support retrieving values from get-model (i.e. extracting values from Terms)

[rbtying]

Take the following example program:

use miette::IntoDiagnostic;
use smtlib::{backend::Z3Binary, Real, Solver, Sort};

fn main() -> miette::Result<()> {
    miette::set_panic_hook();

    let mut solver = Solver::new(Z3Binary::new("z3").into_diagnostic()?)?;
    let x = Real::from_name("x");
    let y = Real::from_name("y");
    let z = Real::from_name("z");

    solver.assert(x.lt(0))?;
    solver.assert(z.lt(0))?;
    solver.assert(y.gt(1))?;
    solver.assert((x * x - y * z * (-10))._eq(y))?;

    let m = solver.check_sat_with_model()?.expect_sat()?;
    eprintln!("{}", m);
    eprintln!("x = {:?}", m.eval(x).unwrap());
    eprintln!("y = {:?}", m.eval(y).unwrap());
    eprintln!("z = {:?}", m.eval(z).unwrap());

    Ok(())
}

In this case, say I would like to get the values of x, y, and z as f64. Z3 will return the values in terms of define-fun, so this would require some ability to interpret the AST in Rust, most likely?

{ z: (- (/ 1.0 4.0)), x: (- 2.0), y: (/ 8.0 7.0) }

That is, I would want z = -0.25, x = -2, y = 1.14285714286 or some similar approximation, with the understanding that Real and f64 are not exactly equivalent.

Maybe this is already possible?