diff --git a/examples/ml/ml_example.ml b/examples/ml/ml_example.ml index 6fd795476..5b4e6e9ed 100644 --- a/examples/ml/ml_example.ml +++ b/examples/ml/ml_example.ml @@ -30,11 +30,11 @@ let model_converter_test ( ctx : context ) = let xr = (Expr.mk_const ctx (Symbol.mk_string ctx "x") (Real.mk_sort ctx)) in let yr = (Expr.mk_const ctx (Symbol.mk_string ctx "y") (Real.mk_sort ctx)) in let g4 = (mk_goal ctx true false false ) in - (Goal.add g4 [ (mk_gt ctx xr (Real.mk_numeral_nd ctx 10L 1L)) ]) ; + (Goal.add g4 [ (mk_gt ctx xr (Real.mk_numeral_nd ctx 10 1)) ]) ; (Goal.add g4 [ (mk_eq ctx yr - (Arithmetic.mk_add ctx [ xr; (Real.mk_numeral_nd ctx 1L 1L) ])) ]) ; - (Goal.add g4 [ (mk_gt ctx yr (Real.mk_numeral_nd ctx 1L 1L)) ]) ; + (Arithmetic.mk_add ctx [ xr; (Real.mk_numeral_nd ctx 1 1) ])) ]) ; + (Goal.add g4 [ (mk_gt ctx yr (Real.mk_numeral_nd ctx 1 1)) ]) ; ( let ar = (Tactic.apply (mk_tactic ctx "simplify") g4 None) in if ((get_num_subgoals ar) == 1 && @@ -163,7 +163,7 @@ let basic_tests ( ctx : context ) = ) ; model_converter_test ctx ; (* Real num/den test. *) - let rn = Real.mk_numeral_nd ctx 42L 43L in + let rn = Real.mk_numeral_nd ctx 42 43 in let inum = (get_numerator rn) in let iden = get_denominator rn in Printf.printf "Numerator: %s Denominator: %s\n" (Real.numeral_to_string inum) (Real.numeral_to_string iden) ; diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp index c0d599de7..7cfd5a345 100644 --- a/src/api/api_arith.cpp +++ b/src/api/api_arith.cpp @@ -48,7 +48,21 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } - Z3_ast Z3_API Z3_mk_real(Z3_context c, int64_t num, int64_t den) { + Z3_ast Z3_API Z3_mk_real_int64(Z3_context c, int64_t num, int64_t den) { + Z3_TRY; + LOG_Z3_mk_real_int64(c, num, den); + RESET_ERROR_CODE(); + if (den == 0) { + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); + RETURN_Z3(nullptr); + } + sort* s = mk_c(c)->m().mk_sort(mk_c(c)->get_arith_fid(), REAL_SORT); + ast* a = mk_c(c)->mk_numeral_core(rational(num, rational::i64())/rational(den, rational::i64()), s); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(nullptr); + } + + Z3_ast Z3_API Z3_mk_real(Z3_context c, int num, int den) { Z3_TRY; LOG_Z3_mk_real(c, num, den); RESET_ERROR_CODE(); @@ -57,7 +71,7 @@ extern "C" { RETURN_Z3(nullptr); } sort* s = mk_c(c)->m().mk_sort(mk_c(c)->get_arith_fid(), REAL_SORT); - ast* a = mk_c(c)->mk_numeral_core(rational(num, rational::i64())/rational(den, rational::i64()), s); + ast* a = mk_c(c)->mk_numeral_core(rational(num, den), s); RETURN_Z3(of_ast(a)); Z3_CATCH_RETURN(nullptr); } diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 9d4ddcfb4..3f47b6637 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -3630,7 +3630,7 @@ namespace z3 { inline expr context::int_val(uint64_t n) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); } inline expr context::int_val(char const * n) { Z3_ast r = Z3_mk_numeral(m_ctx, n, int_sort()); check_error(); return expr(*this, r); } - inline expr context::real_val(int64_t n, int64_t d) { Z3_ast r = Z3_mk_real(m_ctx, n, d); check_error(); return expr(*this, r); } + inline expr context::real_val(int64_t n, int64_t d) { Z3_ast r = Z3_mk_real_int64(m_ctx, n, d); check_error(); return expr(*this, r); } inline expr context::real_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); } inline expr context::real_val(unsigned n) { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); } inline expr context::real_val(int64_t n) { Z3_ast r = Z3_mk_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); } diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index c271f60cf..2fa4acc65 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1092,7 +1092,13 @@ struct let numeral_to_string (x:expr) = Z3native.get_numeral_string (Expr.gc x) x let mk_const (ctx:context) (name:Symbol.symbol) = Expr.mk_const ctx name (mk_sort ctx) let mk_const_s (ctx:context) (name:string) = mk_const ctx (Symbol.mk_string ctx name) - let mk_numeral_nd (ctx:context) (num:int64) (den:int64) = Z3native.mk_real ctx num den + let mk_numeral_nd (ctx:context) (num:int) (den:int) = + if den = 0 then + raise (Error "Denominator is zero") + else if not (check_int32 num) || not (check_int32 den) then + raise (Error "numerals don't fit in 32 bits") + else + Z3native.mk_real ctx num den let mk_numeral_s (ctx:context) (v:string) = Z3native.mk_numeral ctx v (mk_sort ctx) let mk_numeral_i (ctx:context) (v:int) = mk_int_expr ctx v (mk_sort ctx) diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index cb61bee68..b7fa27b5e 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -1264,7 +1264,7 @@ sig (** Create a real numeral from a fraction. @return A Term with rational value and sort Real {!mk_numeral_s} *) - val mk_numeral_nd : context -> int64 -> int64 -> Expr.expr + val mk_numeral_nd : context -> int -> int -> Expr.expr (** Create a real numeral. @return A Term with the given value and sort Real *) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index fd85dd781..88aaa8938 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -3417,11 +3417,21 @@ extern "C" { \sa Z3_mk_numeral \sa Z3_mk_int + \sa Z3_mk_real_int64 \sa Z3_mk_unsigned_int - def_API('Z3_mk_real', AST, (_in(CONTEXT), _in(INT64), _in(INT64))) + def_API('Z3_mk_real', AST, (_in(CONTEXT), _in(INT), _in(INT))) */ - Z3_ast Z3_API Z3_mk_real(Z3_context c, int64_t num, int64_t den); + Z3_ast Z3_API Z3_mk_real(Z3_context c, int num, int den); + + /** + \brief Create a real from a fraction of int64. + + \sa Z3_mk_real + def_API('Z3_mk_real_int64', AST, (_in(CONTEXT), _in(INT64), _in(INT64))) + */ + + Z3_ast Z3_API Z3_mk_real_int64(Z3_context c, int64_t num, int64_t den); /** \brief Create a numeral of an int, bit-vector, or finite-domain sort.