Feat exact f64

[lucascool12]

Adds exact_f64 method to Reals as described in #287.

[dragazo]

Actually I think I was only partially understanding the C API docs. It's definitely the case that irrational numbers give a false zero, which this PR does handle correctly. But it looks like I was wrong in thinking that it only succeeds for numbers that fit perfectly in an f64. Cause your test case 1 / (i32::MAX - 90) definitely doesn't fit exactly in an f64 and yet is still seems to work. I also tested the classic 1 / 3 which also succeeds despite not being exactly encoded in f64 (updated test below if you want it).

So maybe the name I initially proposed, exact_f64, isn't quite right... But it's kind of weird cause the most accurate name seems to be as_rational_f64 or something... Cause basically it seems to be an f64 approximation of a rational number. That might pair well with the as_real function (renamed to as_rational if #305 gets merged).

But even then the precondition (option) of Z3_is_algebraic_number makes it seem like it should work for sqrt(2), but it doesn't... The C lib definitely needs better docs! lol

    let ctx = Context::new(&Config::default());
    let x = Real::new_const(&ctx, "x");
    let y = Real::new_const(&ctx, "y");
    let z = Real::new_const(&ctx, "z");
    let a = Real::new_const(&ctx, "a");
    let b = Real::new_const(&ctx, "b");
    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));
    s.assert(&y._eq(&Int::from_i64(&ctx, 5).to_real()));
    s.assert(&z._eq(&Real::from_real(&ctx, 1, 2)));
    s.assert(&a._eq(&Real::from_real(&ctx, 1, i32::MAX - 90)));
    s.assert(&b._eq(&Real::from_real(&ctx, 1, 3)));
    assert_eq!(s.check(), SatResult::Sat);
    let m = s.get_model().unwrap();
    let res_x = m.eval(&x, false).unwrap();
    let res_y = m.eval(&y, false).unwrap();
    let res_z = m.eval(&z, false).unwrap();
    let res_a = m.eval(&a, false).unwrap();
    let res_b = m.eval(&b, false).unwrap();
    assert_eq!(res_x.exact_f64(), None); // sqrt is irrational
    println!("{:?}", res_y.exact_f64());
    assert_eq!(res_y.exact_f64(), Some(5.0));
    println!("{:?}", res_z.exact_f64());
    assert_eq!(res_z.exact_f64(), Some(0.5));
    println!("{:?}", res_a.exact_f64());
    assert_eq!(res_a.exact_f64(), Some(1.0 / (i32::MAX - 90) as f64));
    println!("{:?}", res_b.exact_f64());
    assert_eq!(res_b.exact_f64(), Some(1.0 / 3.0));