From 84bf1f43ccfeb1bd99802ba2686bac6a6197502b Mon Sep 17 00:00:00 2001 From: Lucas Van Laer Date: Thu, 28 Mar 2024 11:36:57 +0100 Subject: [PATCH] feat: creating reals from numeral strings --- z3/src/ast.rs | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/z3/src/ast.rs b/z3/src/ast.rs index a52de25b..e612167a 100644 --- a/z3/src/ast.rs +++ b/z3/src/ast.rs @@ -583,10 +583,17 @@ impl<'ctx> Real<'ctx> { } pub fn from_real_str(ctx: &'ctx Context, num: &str, den: &str) -> Option> { + let fraction_string = format!("{num:} / {den:}"); + Self::from_str(ctx, &fraction_string) + } + + /// The string may be of the form \[num\]*\[.\[num\]*\]\[E\[+|-\]\[num\]...+\]. + /// Or a rational, that is, a string of the form \[num\]* / \[num\]* + pub fn from_str(ctx: &'ctx Context, numeral: &str) -> Option> { let sort = Sort::real(ctx); let ast = unsafe { - let fraction_cstring = CString::new(format!("{num:} / {den:}")).unwrap(); - let numeral_ptr = Z3_mk_numeral(ctx.z3_ctx, fraction_cstring.as_ptr(), sort.z3_sort); + let c_numeral = CString::new(numeral).unwrap(); + let numeral_ptr = Z3_mk_numeral(ctx.z3_ctx, c_numeral.as_ptr(), sort.z3_sort); if numeral_ptr.is_null() { return None; }