Real approx functions (#304)

It's a bit difficult to work with `Real` (in `z3`, not `z3-sys`) since the only provided way to get a value out at the end is `Real::as_real(&self) -> Option<(i64, i64)>`, which really only works for rational numbers. In this PR I've added two new functions to help:

* `Real::approx(&self, precision: usize) -> ::std::string::String`, which gives a string approximation of the real value up to `precision` correct digits after the decimal (via `Z3_get_numeral_decimal_string`).
* `Real::approx_f64(&self) -> f64`, which is just a convenience wrapper for `self.approx(17).parse().unwrap()` to get a full-precision `f64` approximation of the real number.

z3/src/ast.rs

@@ -930,6 +930,22 @@ impl<'ctx> Real<'ctx> {
         }
     }
 
+    pub fn approx(&self, precision: usize) -> ::std::string::String {
+        let s = unsafe {
+            CStr::from_ptr(Z3_get_numeral_decimal_string(
+                self.ctx.z3_ctx,
+                self.z3_ast,
+                precision as _,
+            ))
+        }
+        .to_str()
+        .unwrap();
+        s.strip_suffix('?').unwrap_or(s).to_owned()
+    }
+    pub fn approx_f64(&self) -> f64 {
+        self.approx(17).parse().unwrap() // 17 decimal digits needed to get full f64 precision
+    }
+
     pub fn from_int(ast: &Int<'ctx>) -> Real<'ctx> {
         unsafe { Self::wrap(ast.ctx, Z3_mk_int2real(ast.ctx.z3_ctx, ast.z3_ast)) }
     }

z3/tests/lib.rs

@@ -8,6 +8,10 @@ use z3::*;
 use num::{bigint::BigInt, rational::BigRational};
 use std::str::FromStr;
 
+mod objectives;
+mod ops;
+mod semver_tests;
+
 #[test]
 fn test_config() {
     let _ = env_logger::try_init();

z3/tests/ops.rs

@@ -1,7 +1,7 @@
 use z3::{
     ast,
     ast::{Array, Ast, AstKind, Bool, Dynamic, Float, Int, Real, BV},
-    Config, Context, DeclKind, FuncDecl, Sort,
+    Config, Context, DeclKind, FuncDecl, SatResult, Solver, Sort,
 };
 
 #[test]
@@ -296,3 +296,52 @@ fn test_func_decl_attributes() {
     assert_eq!(binary_decl.name(), "binary");
     assert_eq!(binary_decl.arity(), 2);
 }
+
+#[test]
+fn test_real_approx() {
+    let ctx = Context::new(&Config::default());
+    let x = Real::new_const(&ctx, "x");
+    let xx = &x * &x;
+    let zero = Real::from_real(&ctx, 0, 1);
+    let two = Real::from_real(&ctx, 2, 1);
+    let s = Solver::new(&ctx);
+    s.assert(&x.ge(&zero));
+    s.assert(&xx._eq(&two));
+    assert_eq!(s.check(), SatResult::Sat);
+    let m = s.get_model().unwrap();
+    let res = m.eval(&x, false).unwrap();
+    assert_eq!(res.as_real(), None); // sqrt is irrational
+    println!("f64 res: {}", res.approx_f64());
+    assert!((res.approx_f64() - ::std::f64::consts::SQRT_2).abs() < 1e-20);
+    assert_eq!(res.approx(0), "1.");
+    assert_eq!(res.approx(1), "1.4");
+    assert_eq!(res.approx(2), "1.41");
+    assert_eq!(res.approx(3), "1.414");
+    assert_eq!(res.approx(4), "1.4142");
+    assert_eq!(res.approx(5), "1.41421");
+    assert_eq!(res.approx(6), "1.414213");
+    assert_eq!(res.approx(7), "1.4142135");
+    assert_eq!(res.approx(8), "1.41421356");
+    assert_eq!(res.approx(9), "1.414213562");
+    assert_eq!(res.approx(10), "1.4142135623");
+    assert_eq!(res.approx(11), "1.41421356237");
+    assert_eq!(res.approx(12), "1.414213562373");
+    assert_eq!(res.approx(13), "1.4142135623730");
+    assert_eq!(res.approx(14), "1.41421356237309");
+    assert_eq!(res.approx(15), "1.414213562373095");
+    assert_eq!(res.approx(16), "1.4142135623730950");
+    assert_eq!(res.approx(17), "1.41421356237309504");
+    assert_eq!(res.approx(18), "1.414213562373095048");
+    assert_eq!(res.approx(19), "1.4142135623730950488");
+    assert_eq!(res.approx(20), "1.41421356237309504880");
+    assert_eq!(res.approx(21), "1.414213562373095048801");
+    assert_eq!(res.approx(22), "1.4142135623730950488016");
+    assert_eq!(res.approx(23), "1.41421356237309504880168");
+    assert_eq!(res.approx(24), "1.414213562373095048801688");
+    assert_eq!(res.approx(25), "1.4142135623730950488016887");
+    assert_eq!(res.approx(26), "1.41421356237309504880168872");
+    assert_eq!(res.approx(27), "1.414213562373095048801688724");
+    assert_eq!(res.approx(28), "1.4142135623730950488016887242");
+    assert_eq!(res.approx_f64(), res.approx(32).parse().unwrap());
+    assert_ne!(res.approx_f64(), res.approx(16).parse().unwrap());
+}