Skip to content

Commit

Permalink
Implement ast::Float::as_f64
Browse files Browse the repository at this point in the history
  • Loading branch information
waywardmonkeys committed Oct 22, 2023
1 parent 1b897d8 commit 3f7dbb1
Show file tree
Hide file tree
Showing 2 changed files with 13 additions and 0 deletions.
4 changes: 4 additions & 0 deletions z3/src/ast.rs
Original file line number Diff line number Diff line change
Expand Up @@ -626,6 +626,10 @@ impl<'ctx> Float<'ctx> {
})
}
}

pub fn as_f64(&self) -> f64 {
unsafe { Z3_get_numeral_double(self.ctx.z3_ctx, self.z3_ast) }
}
}

impl_ast!(Datatype);
Expand Down
9 changes: 9 additions & 0 deletions z3/tests/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -416,6 +416,15 @@ fn test_real_cmp() {
assert_eq!(solver.check(), SatResult::Sat);
}

#[test]
fn test_float() {
let cfg = Config::new();
let ctx = Context::new(&cfg);

let f = ast::Float::from_f64(&ctx, 1.0);
assert_eq!(f.as_f64(), 1.0);
}

#[test]
fn test_float_add() {
let cfg = Config::new();
Expand Down

0 comments on commit 3f7dbb1

Please sign in to comment.