Open lucascool12 opened 1 month ago
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));
Adds
exact_f64
method to Reals as described in #287.