Skip to content

Commit

Permalink
test: add tests for Real::exact_f64
Browse files Browse the repository at this point in the history
  • Loading branch information
lucascool12 committed Aug 2, 2024
1 parent 2f32da9 commit d0e124d
Showing 1 changed file with 31 additions and 0 deletions.
31 changes: 31 additions & 0 deletions z3/tests/ops.rs
Original file line number Diff line number Diff line change
Expand Up @@ -345,3 +345,34 @@ fn test_real_approx() {
assert_eq!(res.approx_f64(), res.approx(32).parse().unwrap());
assert_ne!(res.approx_f64(), res.approx(16).parse().unwrap());
}

#[test]
fn test_real_exact() {
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 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)));
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();
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 as f64 / (i32::MAX - 90) as f64));
}

0 comments on commit d0e124d

Please sign in to comment.