From 5f527fa5626dd800db956267e089c782fd18f031 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 24 Jan 2015 15:54:32 +0000 Subject: [PATCH] documentation fixes Signed-off-by: Christoph M. Wintersteiger --- src/api/z3_fpa.h | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index ca5ffebf7..e1bd67d66 100644 --- a/src/api/z3_fpa.h +++ b/src/api/z3_fpa.h @@ -274,7 +274,7 @@ extern "C" { Z3_ast Z3_API Z3_mk_fpa_fp(__in Z3_context c, __in Z3_ast sgn, __in Z3_ast exp, __in Z3_ast sig); /** - \brief Create a numeral of FloatingPoint sort from a float. + \brief Create a numeral of FloatingPoint sort from a float. This function is used to create numerals that fit in a float value. It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string. @@ -292,20 +292,20 @@ extern "C" { Z3_ast Z3_API Z3_mk_fpa_numeral_float(__in Z3_context c, __in float v, __in Z3_sort ty); /** - \brief Create a numeral of FloatingPoint sort from a double. + \brief Create a numeral of FloatingPoint sort from a double. - This function is used to create numerals that fit in a double value. - It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string. + This function is used to create numerals that fit in a double value. + It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string. - \param c logical context - \param v value - \param ty sort + \param c logical context + \param v value + \param ty sort - ty must be a FloatingPoint sort + ty must be a FloatingPoint sort - \sa Z3_mk_numeral + \sa Z3_mk_numeral - def_API('Z3_mk_fpa_numeral_double', AST, (_in(CONTEXT), _in(DOUBLE), _in(SORT))) + def_API('Z3_mk_fpa_numeral_double', AST, (_in(CONTEXT), _in(DOUBLE), _in(SORT))) */ Z3_ast Z3_API Z3_mk_fpa_numeral_double(__in Z3_context c, __in double v, __in Z3_sort ty);