From 09247d2e29563d2f2a5926c85816ac1c2fb69187 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 1 Jan 2015 18:44:41 +0000 Subject: [PATCH] FPA theory and API overhaul Signed-off-by: Christoph M. Wintersteiger --- scripts/update_api.py | 14 +- src/api/api_fpa.cpp | 354 +++++++++++++++++--- src/api/dotnet/Context.cs | 14 +- src/api/z3_api.h | 3 +- src/api/z3_fpa.h | 641 ++++++++++++++++++++++++++---------- src/ast/float_decl_plugin.h | 39 ++- src/smt/theory_fpa.cpp | 200 ++++++----- src/smt/theory_fpa.h | 8 +- src/util/mpf.h | 2 +- 9 files changed, 944 insertions(+), 331 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 2fbf42cca..a47835904 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -124,6 +124,7 @@ SYMBOL = 9 PRINT_MODE = 10 ERROR_CODE = 11 DOUBLE = 12 +FLOAT = 13 FIRST_OBJ_ID = 100 @@ -131,28 +132,28 @@ def is_obj(ty): return ty >= FIRST_OBJ_ID Type2Str = { VOID : 'void', VOID_PTR : 'void*', INT : 'int', UINT : 'unsigned', INT64 : '__int64', UINT64 : '__uint64', DOUBLE : 'double', - STRING : 'Z3_string', STRING_PTR : 'Z3_string_ptr', BOOL : 'Z3_bool', SYMBOL : 'Z3_symbol', + FLOAT : 'float', STRING : 'Z3_string', STRING_PTR : 'Z3_string_ptr', BOOL : 'Z3_bool', SYMBOL : 'Z3_symbol', PRINT_MODE : 'Z3_ast_print_mode', ERROR_CODE : 'Z3_error_code' } Type2PyStr = { VOID_PTR : 'ctypes.c_void_p', INT : 'ctypes.c_int', UINT : 'ctypes.c_uint', INT64 : 'ctypes.c_longlong', - UINT64 : 'ctypes.c_ulonglong', DOUBLE : 'ctypes.c_double', + UINT64 : 'ctypes.c_ulonglong', DOUBLE : 'ctypes.c_double', FLOAT : 'ctypes.c_float', STRING : 'ctypes.c_char_p', STRING_PTR : 'ctypes.POINTER(ctypes.c_char_p)', BOOL : 'ctypes.c_bool', SYMBOL : 'Symbol', PRINT_MODE : 'ctypes.c_uint', ERROR_CODE : 'ctypes.c_uint' } # Mapping to .NET types Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint', INT64 : 'Int64', UINT64 : 'UInt64', DOUBLE : 'double', - STRING : 'string', STRING_PTR : 'byte**', BOOL : 'int', SYMBOL : 'IntPtr', + FLOAT : 'float', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'int', SYMBOL : 'IntPtr', PRINT_MODE : 'uint', ERROR_CODE : 'uint' } # Mapping to Java types Type2Java = { VOID : 'void', VOID_PTR : 'long', INT : 'int', UINT : 'int', INT64 : 'long', UINT64 : 'long', DOUBLE : 'double', - STRING : 'String', STRING_PTR : 'StringPtr', + FLOAT : 'float', STRING : 'String', STRING_PTR : 'StringPtr', BOOL : 'boolean', SYMBOL : 'long', PRINT_MODE : 'int', ERROR_CODE : 'int'} Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', INT64 : 'jlong', UINT64 : 'jlong', DOUBLE : 'jdouble', - STRING : 'jstring', STRING_PTR : 'jobject', + FLOAT : 'jfloat', STRING : 'jstring', STRING_PTR : 'jobject', BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint'} @@ -927,6 +928,9 @@ def def_API(name, result, params): elif ty == DOUBLE: log_c.write(" D(a%s);\n" % i) exe_c.write("in.get_double(%s)" % i) + elif ty == FLOAT: + log_c.write(" D(a%s);\n" % i) + exe_c.write("in.get_float(%s)" % i) elif ty == BOOL: log_c.write(" I(a%s);\n" % i) exe_c.write("in.get_bool(%s)" % i) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index bbf27d25d..89b278c91 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -7,6 +7,7 @@ Module Name: Abstract: + Additional APIs for floating-point arithmetic (FP). Author: @@ -31,7 +32,7 @@ extern "C" { Z3_sort r = of_sort(ctx->float_util().mk_rm_sort()); RETURN_Z3(r); Z3_CATCH_RETURN(0); - } + } Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(Z3_context c) { @@ -44,10 +45,20 @@ extern "C" { Z3_CATCH_RETURN(0); } + Z3_ast Z3_API Z3_mk_fpa_rne(Z3_context c) { + Z3_TRY; + LOG_Z3_mk_fpa_rne(c); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + Z3_ast r = of_ast(ctx->float_util().mk_round_nearest_ties_to_even()); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(Z3_context c) { Z3_TRY; - LOG_Z3_mk_fpa_round_nearest_ties_to_even(c); + LOG_Z3_mk_fpa_round_nearest_ties_to_away(c); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); Z3_ast r = of_ast(ctx->float_util().mk_round_nearest_ties_to_away()); @@ -55,10 +66,20 @@ extern "C" { Z3_CATCH_RETURN(0); } + Z3_ast Z3_API Z3_mk_fpa_rna(Z3_context c) { + Z3_TRY; + LOG_Z3_mk_fpa_rna(c); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + Z3_ast r = of_ast(ctx->float_util().mk_round_nearest_ties_to_away()); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(Z3_context c) { Z3_TRY; - LOG_Z3_mk_fpa_round_nearest_ties_to_even(c); + LOG_Z3_mk_fpa_round_toward_positive(c); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); Z3_ast r = of_ast(ctx->float_util().mk_round_toward_positive()); @@ -66,10 +87,20 @@ extern "C" { Z3_CATCH_RETURN(0); } + Z3_ast Z3_API Z3_mk_fpa_rtp(Z3_context c) { + Z3_TRY; + LOG_Z3_mk_fpa_rtp(c); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + Z3_ast r = of_ast(ctx->float_util().mk_round_toward_positive()); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(Z3_context c) { Z3_TRY; - LOG_Z3_mk_fpa_round_nearest_ties_to_even(c); + LOG_Z3_mk_fpa_round_toward_negative(c); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); Z3_ast r = of_ast(ctx->float_util().mk_round_toward_negative()); @@ -77,10 +108,20 @@ extern "C" { Z3_CATCH_RETURN(0); } + Z3_ast Z3_API Z3_mk_fpa_rtn(Z3_context c) { + Z3_TRY; + LOG_Z3_mk_fpa_rtn(c); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + Z3_ast r = of_ast(ctx->float_util().mk_round_toward_negative()); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(Z3_context c) { Z3_TRY; - LOG_Z3_mk_fpa_round_nearest_ties_to_even(c); + LOG_Z3_mk_fpa_round_toward_zero(c); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); Z3_ast r = of_ast(ctx->float_util().mk_round_toward_zero()); @@ -88,6 +129,16 @@ extern "C" { Z3_CATCH_RETURN(0); } + Z3_ast Z3_API Z3_mk_fpa_rtz(Z3_context c) { + Z3_TRY; + LOG_Z3_mk_fpa_rtz(c); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + Z3_ast r = of_ast(ctx->float_util().mk_round_toward_zero()); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits) { Z3_TRY; @@ -102,35 +153,35 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_sort Z3_API Z3_mk_fpa_sort_half(__in Z3_context c) { + Z3_sort Z3_API Z3_mk_fpa_sort_half(Z3_context c) { return Z3_mk_fpa_sort(c, 5, 11); } - Z3_sort Z3_API Z3_mk_fpa_sort_16(__in Z3_context c) { + Z3_sort Z3_API Z3_mk_fpa_sort_16(Z3_context c) { return Z3_mk_fpa_sort(c, 5, 11); } - Z3_sort Z3_API Z3_mk_fpa_sort_single(__in Z3_context c) { + Z3_sort Z3_API Z3_mk_fpa_sort_single(Z3_context c) { return Z3_mk_fpa_sort(c, 8, 24); } - Z3_sort Z3_API Z3_mk_fpa_sort_32(__in Z3_context c) { + Z3_sort Z3_API Z3_mk_fpa_sort_32(Z3_context c) { return Z3_mk_fpa_sort(c, 8, 24); } - Z3_sort Z3_API Z3_mk_fpa_sort_double(__in Z3_context c) { + Z3_sort Z3_API Z3_mk_fpa_sort_double(Z3_context c) { return Z3_mk_fpa_sort(c, 11, 53); } - Z3_sort Z3_API Z3_mk_fpa_sort_64(__in Z3_context c) { + Z3_sort Z3_API Z3_mk_fpa_sort_64(Z3_context c) { return Z3_mk_fpa_sort(c, 11, 53); } - Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(__in Z3_context c) { + Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(Z3_context c) { return Z3_mk_fpa_sort(c, 15, 113); } - Z3_sort Z3_API Z3_mk_fpa_sort_128(__in Z3_context c) { + Z3_sort Z3_API Z3_mk_fpa_sort_128(Z3_context c) { return Z3_mk_fpa_sort(c, 15, 113); } @@ -164,6 +215,28 @@ extern "C" { Z3_CATCH_RETURN(0); } + Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast sig, Z3_ast exp) { + Z3_TRY; + LOG_Z3_mk_fpa_fp(c, sgn, sig, exp); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + Z3_ast r = of_ast(ctx->float_util().mk_fp(to_expr(sgn), to_expr(sig), to_expr(exp))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_numeral_float(Z3_context c, float v, Z3_sort ty) { + Z3_TRY; + LOG_Z3_mk_fpa_numeral_float(c, v, ty); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + scoped_mpf tmp(ctx->float_util().fm()); + ctx->float_util().fm().set(tmp, ctx->float_util().get_ebits(to_sort(ty)), ctx->float_util().get_sbits(to_sort(ty)), v); + Z3_ast r = of_ast(ctx->float_util().mk_value(tmp)); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + Z3_ast Z3_API Z3_mk_fpa_numeral_double(Z3_context c, double v, Z3_sort ty) { Z3_TRY; LOG_Z3_mk_fpa_numeral_double(c, v, ty); @@ -175,6 +248,51 @@ extern "C" { RETURN_Z3(r); Z3_CATCH_RETURN(0); } + + Z3_ast Z3_API Z3_mk_fpa_numeral_int(Z3_context c, signed v, Z3_sort ty) { + Z3_TRY; + LOG_Z3_mk_fpa_numeral_int(c, v, ty); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + scoped_mpf tmp(ctx->float_util().fm()); + ctx->float_util().fm().set(tmp, + ctx->float_util().get_ebits(to_sort(ty)), + ctx->float_util().get_sbits(to_sort(ty)), + v); + Z3_ast r = of_ast(ctx->float_util().mk_value(tmp)); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_numeral_uint_int(Z3_context c, bool sgn, unsigned sig, signed exp, Z3_sort ty) { + Z3_TRY; + LOG_Z3_mk_fpa_numeral_uint64_int64(c, sgn, sig, exp, ty); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + scoped_mpf tmp(ctx->float_util().fm()); + ctx->float_util().fm().set(tmp, + ctx->float_util().get_ebits(to_sort(ty)), + ctx->float_util().get_sbits(to_sort(ty)), + sgn, sig, exp); + Z3_ast r = of_ast(ctx->float_util().mk_value(tmp)); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_numeral_uint64_int64(Z3_context c, bool sgn, __uint64 sig, __int64 exp, Z3_sort ty) { + Z3_TRY; + LOG_Z3_mk_fpa_numeral_uint64_int64(c, sgn, sig, exp, ty); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + scoped_mpf tmp(ctx->float_util().fm()); + ctx->float_util().fm().set(tmp, + ctx->float_util().get_ebits(to_sort(ty)), + ctx->float_util().get_sbits(to_sort(ty)), + sgn, sig, exp); + Z3_ast r = of_ast(ctx->float_util().mk_value(tmp)); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t) { Z3_TRY; @@ -265,20 +383,40 @@ extern "C" { RETURN_Z3(r); Z3_CATCH_RETURN(0); } - - Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2) { + + Z3_ast Z3_API Z3_mk_fpa_round_to_integral(Z3_context c, Z3_ast rm, Z3_ast t) { Z3_TRY; - LOG_Z3_mk_fpa_eq(c, t1, t2); + LOG_Z3_mk_fpa_round_to_integral(c, rm, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_float_eq(to_expr(t1), to_expr(t2))); + Z3_ast r = of_ast(ctx->float_util().mk_round_to_integral(to_expr(rm), to_expr(t))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2) { + Z3_TRY; + LOG_Z3_mk_fpa_min(c, t1, t2); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + Z3_ast r = of_ast(ctx->float_util().mk_min(to_expr(t1), to_expr(t2))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2) { + Z3_TRY; + LOG_Z3_mk_fpa_max(c, t1, t2); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + Z3_ast r = of_ast(ctx->float_util().mk_max(to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_fpa_le(Z3_context c, Z3_ast t1, Z3_ast t2) { + Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2) { Z3_TRY; - LOG_Z3_mk_fpa_le(c, t1, t2); + LOG_Z3_mk_fpa_leq(c, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); Z3_ast r = of_ast(ctx->float_util().mk_le(to_expr(t1), to_expr(t2))); @@ -296,9 +434,9 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_fpa_ge(Z3_context c, Z3_ast t1, Z3_ast t2) { + Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2) { Z3_TRY; - LOG_Z3_mk_fpa_ge(c, t1, t2); + LOG_Z3_mk_fpa_geq(c, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); Z3_ast r = of_ast(ctx->float_util().mk_ge(to_expr(t1), to_expr(t2))); @@ -315,6 +453,16 @@ extern "C" { RETURN_Z3(r); Z3_CATCH_RETURN(0); } + + Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2) { + Z3_TRY; + LOG_Z3_mk_fpa_eq(c, t1, t2); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + Z3_ast r = of_ast(ctx->float_util().mk_float_eq(to_expr(t1), to_expr(t2))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } Z3_ast Z3_API Z3_mk_fpa_is_normal(Z3_context c, Z3_ast t) { Z3_TRY; @@ -346,9 +494,9 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_fpa_is_inf(Z3_context c, Z3_ast t) { + Z3_ast Z3_API Z3_mk_fpa_is_infinite(Z3_context c, Z3_ast t) { Z3_TRY; - LOG_Z3_mk_fpa_is_inf(c, t); + LOG_Z3_mk_fpa_is_infinite(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); Z3_ast r = of_ast(ctx->float_util().mk_is_inf(to_expr(t))); @@ -366,40 +514,142 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2) { + Z3_ast Z3_API Z3_mk_fpa_is_negative(Z3_context c, Z3_ast t) { Z3_TRY; - LOG_Z3_mk_fpa_min(c, t1, t2); + LOG_Z3_mk_fpa_is_negative(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_min(to_expr(t1), to_expr(t2))); - RETURN_Z3(r); - Z3_CATCH_RETURN(0); - } - - Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2) { - Z3_TRY; - LOG_Z3_mk_fpa_max(c, t1, t2); - RESET_ERROR_CODE(); - api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_max(to_expr(t1), to_expr(t2))); + Z3_ast r = of_ast(ctx->float_util().mk_is_negative(to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_fpa_convert(Z3_context c, Z3_sort s, Z3_ast rm, Z3_ast t) { + Z3_ast Z3_API Z3_mk_fpa_is_positive(Z3_context c, Z3_ast t) { Z3_TRY; - LOG_Z3_mk_fpa_convert(c, s, rm, t); + LOG_Z3_mk_fpa_is_positive(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - expr * args [2] = { to_expr(rm), to_expr(t) }; - Z3_ast r = of_ast(ctx->m().mk_app(ctx->float_util().get_family_id(), OP_FLOAT_TO_FP, - to_sort(s)->get_num_parameters(), to_sort(s)->get_parameters(), - 2, args)); + Z3_ast r = of_ast(ctx->float_util().mk_is_positive(to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(__in Z3_context c, __in Z3_ast t) { + + Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s) { + Z3_TRY; + LOG_Z3_mk_fpa_to_fp_bv(c, bv, s); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + float_util & fu = ctx->float_util(); + if (!ctx->bvutil().is_bv(to_expr(bv)) || + !fu.is_float(to_sort(s))) { + SET_ERROR_CODE(Z3_INVALID_ARG); + return 0; + } + Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(bv))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s) { + Z3_TRY; + LOG_Z3_mk_fpa_to_fp_float(c, rm, t, s); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + float_util & fu = ctx->float_util(); + if (!fu.is_rm(to_expr(rm)) || + !fu.is_float(to_expr(t)) || + !fu.is_float(to_sort(s))) { + SET_ERROR_CODE(Z3_INVALID_ARG); + return 0; + } + Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_to_fp_real(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s) { + Z3_TRY; + LOG_Z3_mk_fpa_to_fp_real(c, rm, t, s); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + float_util & fu = ctx->float_util(); + if (!fu.is_rm(to_expr(rm)) || + !ctx->autil().is_real(to_expr(t)) || + !fu.is_float(to_sort(s))) { + SET_ERROR_CODE(Z3_INVALID_ARG); + return 0; + } + Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s) { + Z3_TRY; + LOG_Z3_mk_fpa_to_fp_signed(c, rm, t, s); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + float_util & fu = ctx->float_util(); + if (!fu.is_rm(to_expr(rm)) || + !ctx->bvutil().is_bv(to_expr(t)) || + !fu.is_float(to_sort(s))) { + SET_ERROR_CODE(Z3_INVALID_ARG); + return 0; + } + Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s) { + Z3_TRY; + LOG_Z3_mk_fpa_to_fp_unsigned(c, rm, t, s); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + float_util & fu = ctx->float_util(); + if (!fu.is_rm(to_expr(rm)) || + !ctx->bvutil().is_bv(to_expr(t)) || + !fu.is_float(to_sort(s))) { + SET_ERROR_CODE(Z3_INVALID_ARG); + return 0; + } + Z3_ast r = of_ast(fu.mk_to_fp_unsigned(to_sort(s), to_expr(rm), to_expr(t))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_to_ubv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz) { + Z3_TRY; + LOG_Z3_mk_fpa_to_ubv(c, rm, t, sz); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + Z3_ast r = of_ast(ctx->float_util().mk_to_ubv(to_expr(rm), to_expr(t), sz)); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz) { + Z3_TRY; + LOG_Z3_mk_fpa_to_sbv(c, rm, t, sz); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + Z3_ast r = of_ast(ctx->float_util().mk_to_sbv(to_expr(rm), to_expr(t), sz)); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_to_real(Z3_context c, Z3_ast t) { + Z3_TRY; + LOG_Z3_mk_fpa_to_real(c, t); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + Z3_ast r = of_ast(ctx->float_util().mk_to_real(to_expr(t))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t) { Z3_TRY; LOG_Z3_mk_fpa_to_ieee_bv(c, t); RESET_ERROR_CODE(); @@ -409,4 +659,22 @@ extern "C" { Z3_CATCH_RETURN(0); } + Z3_ast Z3_API Z3_mk_fpa_to_fp_real_int(Z3_context c, Z3_ast rm, Z3_ast sig, Z3_ast exp, Z3_sort s) { + Z3_TRY; + LOG_Z3_mk_fpa_to_fp_real_int(c, rm, sig, exp, s); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + float_util & fu = ctx->float_util(); + if (!fu.is_rm(to_expr(rm)) || + !ctx->autil().is_real(to_expr(sig)) || + !ctx->autil().is_int(to_expr(exp)) || + !fu.is_float(to_sort(s))) { + SET_ERROR_CODE(Z3_INVALID_ARG); + return 0; + } + Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(sig), to_expr(exp))); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); + } + }; diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 87090dcc9..69855fc4f 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -3661,10 +3661,10 @@ namespace Microsoft.Z3 /// /// floating point term /// floating point term - public BoolExpr MkFPLe(FPExpr t1, FPExpr t2) + public BoolExpr MkFPLEq(FPExpr t1, FPExpr t2) { Contract.Ensures(Contract.Result() != null); - return new BoolExpr(this, Native.Z3_mk_fpa_le(this.nCtx, t1.NativeObject, t2.NativeObject)); + return new BoolExpr(this, Native.Z3_mk_fpa_leq(this.nCtx, t1.NativeObject, t2.NativeObject)); } /// @@ -3683,10 +3683,10 @@ namespace Microsoft.Z3 /// /// floating point term /// floating point term - public BoolExpr MkFPGe(FPExpr t1, FPExpr t2) + public BoolExpr MkFPGEq(FPExpr t1, FPExpr t2) { Contract.Ensures(Contract.Result() != null); - return new BoolExpr(this, Native.Z3_mk_fpa_ge(this.nCtx, t1.NativeObject, t2.NativeObject)); + return new BoolExpr(this, Native.Z3_mk_fpa_geq(this.nCtx, t1.NativeObject, t2.NativeObject)); } /// @@ -3737,7 +3737,7 @@ namespace Microsoft.Z3 public BoolExpr MkFPIsInf(FPExpr t) { Contract.Ensures(Contract.Result() != null); - return new BoolExpr(this, Native.Z3_mk_fpa_is_inf(this.nCtx, t.NativeObject)); + return new BoolExpr(this, Native.Z3_mk_fpa_is_infinite(this.nCtx, t.NativeObject)); } /// @@ -3782,10 +3782,10 @@ namespace Microsoft.Z3 /// floating point sort /// floating point rounding mode term /// floating point term - public FPExpr MkFPConvert(FPSort s, FPRMExpr rm, FPExpr t) + public FPExpr MkFPToFP(FPSort s, FPRMExpr rm, FPExpr t) { Contract.Ensures(Contract.Result() != null); - return new FPExpr(this, Native.Z3_mk_fpa_convert(this.nCtx, s.NativeObject, rm.NativeObject, t.NativeObject)); + return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, s.NativeObject, rm.NativeObject, t.NativeObject)); } #endregion diff --git a/src/api/z3_api.h b/src/api/z3_api.h index e4bb4bd1d..776e4e9fe 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1700,8 +1700,7 @@ extern "C" { /** \brief Create the real type. - This type is not a floating point number. - Z3 does not have support for floating point numbers yet. + Note that this type is not a floating point number. def_API('Z3_mk_real_sort', SORT, (_in(CONTEXT), )) */ diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index 50ad49590..48d3e790d 100644 --- a/src/api/z3_fpa.h +++ b/src/api/z3_fpa.h @@ -7,7 +7,7 @@ Module Name: Abstract: - Additional APIs for floating-point arithmetic (FPA). + Additional APIs for floating-point arithmetic (FP). Author: @@ -36,7 +36,7 @@ extern "C" { /*@{*/ /** - \brief Create a rounding mode sort. + \brief Create the RoundingMode sort. \param c logical context. @@ -45,7 +45,7 @@ extern "C" { Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(__in Z3_context c); /** - \brief Create a numeral of rounding mode sort which represents the NearestTiesToEven rounding mode. + \brief Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. \param c logical context. @@ -54,7 +54,16 @@ extern "C" { Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(__in Z3_context c); /** - \brief Create a numeral of rounding mode sort which represents the NearestTiesToAway rounding mode. + \brief Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. + + \param c logical context. + + def_API('Z3_mk_fpa_rne', AST, (_in(CONTEXT),)) + */ + Z3_ast Z3_API Z3_mk_fpa_rne(__in Z3_context c); + + /** + \brief Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. \param c logical context. @@ -63,25 +72,52 @@ extern "C" { Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(__in Z3_context c); /** - \brief Create a numeral of rounding mode sort which represents the TowardPositive rounding mode. + \brief Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. + + \param c logical context. + + def_API('Z3_mk_fpa_rna', AST, (_in(CONTEXT),)) + */ + Z3_ast Z3_API Z3_mk_fpa_rna(__in Z3_context c); + + /** + \brief Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. \param c logical context. def_API('Z3_mk_fpa_round_toward_positive', AST, (_in(CONTEXT),)) */ - Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(__in Z3_context c); + Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(__in Z3_context c); /** - \brief Create a numeral of rounding mode sort which represents the TowardNegative rounding mode. + \brief Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. + + \param c logical context. + + def_API('Z3_mk_fpa_rtp', AST, (_in(CONTEXT),)) + */ + Z3_ast Z3_API Z3_mk_fpa_rtp(__in Z3_context c); + + /** + \brief Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. \param c logical context. def_API('Z3_mk_fpa_round_toward_negative', AST, (_in(CONTEXT),)) */ - Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(__in Z3_context c); + Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(__in Z3_context c); /** - \brief Create a numeral of rounding mode sort which represents the TowardZero rounding mode. + \brief Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. + + \param c logical context. + + def_API('Z3_mk_fpa_rtn', AST, (_in(CONTEXT),)) + */ + Z3_ast Z3_API Z3_mk_fpa_rtn(__in Z3_context c); + + /** + \brief Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. \param c logical context. @@ -89,14 +125,21 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(__in Z3_context c); - - /** - \brief Create a floating point sort. + \brief Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. \param c logical context. - \param ebits number of exponent bits - \param sbits number of significand bits + + def_API('Z3_mk_fpa_rtz', AST, (_in(CONTEXT),)) + */ + Z3_ast Z3_API Z3_mk_fpa_rtz(__in Z3_context c); + + /** + \brief Create a FloatingPoint sort. + + \param c logical context. + \param ebits number of exponent bits. + \param sbits number of significand bits. \remark ebits must be larger than 1 and sbits must be larger than 2. @@ -105,85 +148,61 @@ extern "C" { Z3_sort Z3_API Z3_mk_fpa_sort(__in Z3_context c, __in unsigned ebits, __in unsigned sbits); /** - \brief Create the half-precision (16-bit) floating point sort. + \brief Create the half-precision (16-bit) FloatingPoint sort. \param c logical context. - \param ebits number of exponent bits - \param sbits number of significand bits - - \remark ebits must be larger than 1 and sbits must be larger than 2. def_API('Z3_mk_fpa_sort_half', SORT, (_in(CONTEXT),)) */ Z3_sort Z3_API Z3_mk_fpa_sort_half(__in Z3_context c); /** - \brief Create the half-precision (16-bit) floating point sort. + \brief Create the half-precision (16-bit) FloatingPoint sort. - \param c logical context. - \param ebits number of exponent bits - \param sbits number of significand bits + \param c logical context. - \remark ebits must be larger than 1 and sbits must be larger than 2. - - def_API('Z3_mk_fpa_sort_16', SORT, (_in(CONTEXT),)) + def_API('Z3_mk_fpa_sort_16', SORT, (_in(CONTEXT),)) */ Z3_sort Z3_API Z3_mk_fpa_sort_16(__in Z3_context c); /** - \brief Create the single-precision (32-bit) floating point sort. + \brief Create the single-precision (32-bit) FloatingPoint sort. - \param c logical context. - \param ebits number of exponent bits - \param sbits number of significand bits - - \remark ebits must be larger than 1 and sbits must be larger than 2. + \param c logical context. def_API('Z3_mk_fpa_sort_single', SORT, (_in(CONTEXT),)) */ Z3_sort Z3_API Z3_mk_fpa_sort_single(__in Z3_context c); /** - \brief Create the single-precision (32-bit) floating point sort. + \brief Create the single-precision (32-bit) FloatingPoint sort. - \param c logical context. - \param ebits number of exponent bits - \param sbits number of significand bits + \param c logical context. - \remark ebits must be larger than 1 and sbits must be larger than 2. - - def_API('Z3_mk_fpa_sort_32', SORT, (_in(CONTEXT),)) + def_API('Z3_mk_fpa_sort_32', SORT, (_in(CONTEXT),)) */ Z3_sort Z3_API Z3_mk_fpa_sort_32(__in Z3_context c); /** - \brief Create the double-precision (64-bit) floating point sort. + \brief Create the double-precision (64-bit) FloatingPoint sort. \param c logical context. - \param ebits number of exponent bits - \param sbits number of significand bits - - \remark ebits must be larger than 1 and sbits must be larger than 2. def_API('Z3_mk_fpa_sort_double', SORT, (_in(CONTEXT),)) */ Z3_sort Z3_API Z3_mk_fpa_sort_double(__in Z3_context c); /** - \brief Create the double-precision (64-bit) floating point sort. + \brief Create the double-precision (64-bit) FloatingPoint sort. - \param c logical context. - \param ebits number of exponent bits - \param sbits number of significand bits + \param c logical context. - \remark ebits must be larger than 1 and sbits must be larger than 2. - - def_API('Z3_mk_fpa_sort_64', SORT, (_in(CONTEXT),)) + def_API('Z3_mk_fpa_sort_64', SORT, (_in(CONTEXT),)) */ Z3_sort Z3_API Z3_mk_fpa_sort_64(__in Z3_context c); /** - \brief Create the quadruple-precision (128-bit) floating point sort. + \brief Create the quadruple-precision (128-bit) FloatingPoint sort. \param c logical context. \param ebits number of exponent bits @@ -196,15 +215,15 @@ extern "C" { Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(__in Z3_context c); /** - \brief Create the quadruple-precision (128-bit) floating point sort. + \brief Create the quadruple-precision (128-bit) FloatingPoint sort. - \param c logical context. - \param ebits number of exponent bits - \param sbits number of significand bits + \param c logical context. + \param ebits number of exponent bits + \param sbits number of significand bits - \remark ebits must be larger than 1 and sbits must be larger than 2. + \remark ebits must be larger than 1 and sbits must be larger than 2. - def_API('Z3_mk_fpa_sort_128', SORT, (_in(CONTEXT),)) + def_API('Z3_mk_fpa_sort_128', SORT, (_in(CONTEXT),)) */ Z3_sort Z3_API Z3_mk_fpa_sort_128(__in Z3_context c); @@ -219,7 +238,7 @@ extern "C" { Z3_ast Z3_API Z3_mk_fpa_nan(__in Z3_context c, __in Z3_sort s); /** - \brief Create a floating point infinity of sort s. + \brief Create a floating-point infinity of sort s. \param c logical context. \param s target sort @@ -232,29 +251,64 @@ extern "C" { Z3_ast Z3_API Z3_mk_fpa_inf(__in Z3_context c, __in Z3_sort s, __in Z3_bool negative); /** - \brief Create a floating point zero of sort s. + \brief Create a floating-point zero of sort s. - \param c logical context. - \param s target sort - \param negative indicates whether the result should be negative + \param c logical context. + \param s target sort + \param negative indicates whether the result should be negative - When \c negative is true, -zero will be generated instead of +zero. + When \c negative is true, -zero will be generated instead of +zero. - def_API('Z3_mk_fpa_zero', AST, (_in(CONTEXT),_in(SORT),_in(BOOL))) + def_API('Z3_mk_fpa_zero', AST, (_in(CONTEXT),_in(SORT),_in(BOOL))) */ Z3_ast Z3_API Z3_mk_fpa_zero(__in Z3_context c, __in Z3_sort s, __in Z3_bool negative); /** - \brief Create a numeral of floating point sort from a double. + \brief Create an expression of FloatingPoint sort from three bit-vector expressions. + + Note that \c sign is required to be a bit-vector of size 1. Significand and exponent + are required to be greater than 1 and 2 respectively. The FloatingPoint sort + of the resulting expression is automatically determined from the bit-vector sizes + of the arguments. + + \params c logical context. + \params sgn sign + \params sig significand + \params exp exponent + + def_API('Z3_mk_fpa_fp', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_fp(__in Z3_context c, __in Z3_ast sgn, __in Z3_ast sig, __in Z3_ast exp); + + /** + \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. + + \params c logical context. + \params v value. + \params ty sort. + + ty must be a FloatingPoint sort + + \sa Z3_mk_numeral + + def_API('Z3_mk_fpa_numeral_float', AST, (_in(CONTEXT), _in(FLOAT), _in(SORT))) + */ + 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. - This function can be use to create numerals that fit in a double value. + 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. \params c logical context. \params v value. \params ty sort. - ty must be a floating point sort + ty must be a FloatingPoint sort \sa Z3_mk_numeral @@ -262,13 +316,57 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_fpa_numeral_double(__in Z3_context c, __in double v, __in Z3_sort ty); + /** + \brief Create a numeral of FloatingPoint sort from a signed integer. + + \params c logical context. + \params v value. + + ty must be a FloatingPoint sort + + \sa Z3_mk_numeral + + def_API('Z3_mk_fpa_numeral_int', AST, (_in(CONTEXT), _in(INT), _in(SORT))) + */ + Z3_ast Z3_API Z3_mk_fpa_numeral_int(__in Z3_context c, __in signed v, Z3_sort ty); + + /** + \brief Create a numeral of FloatingPoint sort from a sign bit and two integers. + + \params c logical context. + \params sgn sign bit (true == negative). + \params sig significand. + \params exp exponent. + + ty must be a FloatingPoint sort + + \sa Z3_mk_numeral + + def_API('Z3_mk_fpa_numeral_uint_int', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in(INT), _in(SORT))) + */ + Z3_ast Z3_API Z3_mk_fpa_numeral_uint_int(__in Z3_context c, __in bool sgn, __in unsigned sig, __in signed exp, Z3_sort ty); + + /** + \brief Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers. + + \params c logical context. + \params sgn sign bit (true == negative). + \params sig significand. + \params exp exponent. + + ty must be a FloatingPoint sort + + \sa Z3_mk_numeral + + def_API('Z3_mk_fpa_numeral_uint64_int64', AST, (_in(CONTEXT), _in(BOOL), _in(UINT64), _in(INT64), _in(SORT))) + */ + Z3_ast Z3_API Z3_mk_fpa_numeral_uint64_int64(__in Z3_context c, __in bool sgn, __in __uint64 sig, __in __int64 exp, Z3_sort ty); + /** \brief Floating-point absolute value \param c logical context. - \param t floating-point term. - - t must have floating point sort. + \param t term of FloatingPoint sort. def_API('Z3_mk_fpa_abs', AST, (_in(CONTEXT),_in(AST))) */ @@ -278,9 +376,7 @@ extern "C" { \brief Floating-point negation \param c logical context. - \param t floating-point term. - - t must have floating point sort. + \param t term of FloatingPoint sort. def_API('Z3_mk_fpa_neg', AST, (_in(CONTEXT),_in(AST))) */ @@ -290,11 +386,11 @@ extern "C" { \brief Floating-point addition \param c logical context. - \param rm rounding mode - \param t1 floating-point term. - \param t2 floating-point term. + \param rm term of RoundingMode sort. + \param t1 term of FloatingPoint sort. + \param t2 term of FloatingPoint sort. - rm must be of FPA rounding mode sort, t1 and t2 must have the same floating point sort. + rm must be of RoundingMode sort, t1 and t2 must have the same FloatingPoint sort. def_API('Z3_mk_fpa_add', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST))) */ @@ -304,11 +400,11 @@ extern "C" { \brief Floating-point subtraction \param c logical context. - \param rm rounding mode - \param t1 floating-point term. - \param t2 floating-point term. + \param rm term of RoundingMode sort. + \param t1 term of FloatingPoint sort. + \param t2 term of FloatingPoint sort. - rm must be of FPA rounding mode sort, t1 and t2 must have the same floating point sort. + rm must be of RoundingMode sort, t1 and t2 must have the same FloatingPoint sort. def_API('Z3_mk_fpa_sub', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST))) */ @@ -318,11 +414,11 @@ extern "C" { \brief Floating-point multiplication \param c logical context. - \param rm rounding mode - \param t1 floating-point term. - \param t2 floating-point term. + \param rm term of RoundingMode sort. + \param t1 term of FloatingPoint sort. + \param t2 term of FloatingPoint sort. - rm must be of FPA rounding mode sort, t1 and t2 must have the same floating point sort. + rm must be of RoundingMode sort, t1 and t2 must have the same FloatingPoint sort. def_API('Z3_mk_fpa_mul', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST))) */ @@ -332,11 +428,11 @@ extern "C" { \brief Floating-point division \param c logical context. - \param rm rounding mode - \param t1 floating-point term. - \param t2 floating-point term. + \param rm term of RoundingMode sort. + \param t1 term of FloatingPoint sort. + \param t2 term of FloatingPoint sort. - The nodes rm must be of FPA rounding mode sort t1 and t2 must have the same floating point sort. + The nodes rm must be of RoundingMode sort t1 and t2 must have the same FloatingPoint sort. def_API('Z3_mk_fpa_div', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST))) */ @@ -346,13 +442,13 @@ extern "C" { \brief Floating-point fused multiply-add. \param c logical context. - \param rm rounding mode - \param t1 floating-point term. - \param t2 floating-point term. + \param rm term of RoundingMode sort. + \param t1 term of FloatingPoint sort. + \param t2 term of FloatingPoint sort. The result is round((t1 * t2) + t3) - rm must be of FPA rounding mode sort, t1, t2, and t3 must have the same floating point sort. + rm must be of RoundingMode sort, t1, t2, and t3 must have the same FloatingPoint sort. def_API('Z3_mk_fpa_fma', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST),_in(AST))) */ @@ -362,10 +458,10 @@ extern "C" { \brief Floating-point square root \param c logical context. - \param rm rounding mode - \param t floating-point term. + \param rm term of RoundingMode sort. + \param t term of FloatingPoint sort. - rm must be of FPA rounding mode sort, t must have floating point sort. + rm must be of RoundingMode sort, t must have FloatingPoint sort. def_API('Z3_mk_fpa_sqrt', AST, (_in(CONTEXT),_in(AST),_in(AST))) */ @@ -375,198 +471,387 @@ extern "C" { \brief Floating-point remainder \param c logical context. - \param t1 floating-point term. - \param t2 floating-point term. + \param t1 term of FloatingPoint sort. + \param t2 term of FloatingPoint sort. - t1 and t2 must have the same floating point sort. + t1 and t2 must have the same FloatingPoint sort. def_API('Z3_mk_fpa_rem', AST, (_in(CONTEXT),_in(AST),_in(AST))) */ - Z3_ast Z3_API Z3_mk_fpa_rem(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); - + Z3_ast Z3_API Z3_mk_fpa_rem(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); + /** - \brief Floating-point equality + \brief Floating-point roundToIntegral. Rounds a floating-point number to + the closest integer, again represented as a floating-point number. \param c logical context. - \param t1 floating-point term. - \param t2 floating-point term. + \param rm term of RoundingMode sort. + \param t term of FloatingPoint sort. - Note that this is IEEE 754 equality (as opposed to SMT-LIB =). + t must be of FloatingPoint sort. - t1 and t2 must have the same floating point sort. - - def_API('Z3_mk_fpa_eq', AST, (_in(CONTEXT),_in(AST),_in(AST))) - */ - Z3_ast Z3_API Z3_mk_fpa_eq(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); + def_API('Z3_mk_fpa_round_to_integral', AST, (_in(CONTEXT),_in(AST),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_round_to_integral(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t); + + /** + \brief Minimum of floating-point numbers + + \param c logical context. + \param t1 term of FloatingPoint sort. + \param t2 term of FloatingPoint sort. + + t1, t2 must have the same FloatingPoint sort. + + def_API('Z3_mk_fpa_min', AST, (_in(CONTEXT),_in(AST),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_min(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); + + /** + \brief Maximum of floating-point numbers + + \param c logical context. + \param t1 term of FloatingPoint sort. + \param t2 term of FloatingPoint sort. + + t1, t2 must have the same FloatingPoint sort. + + def_API('Z3_mk_fpa_max', AST, (_in(CONTEXT),_in(AST),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_max(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); /** \brief Floating-point less than or equal \param c logical context. - \param t1 floating-point term. - \param t2 floating-point term. + \param t1 term of FloatingPoint sort. + \param t2 term of FloatingPoint sort. - t1 and t2 must have the same floating point sort. + t1 and t2 must have the same FloatingPoint sort. - def_API('Z3_mk_fpa_le', AST, (_in(CONTEXT),_in(AST),_in(AST))) + def_API('Z3_mk_fpa_leq', AST, (_in(CONTEXT),_in(AST),_in(AST))) */ - Z3_ast Z3_API Z3_mk_fpa_le(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); + Z3_ast Z3_API Z3_mk_fpa_leq(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); /** \brief Floating-point less-than \param c logical context. - \param t1 floating-point term. - \param t2 floating-point term. + \param t1 term of FloatingPoint sort. + \param t2 term of FloatingPoint sort. - t1 and t2 must have the same floating point sort. + t1 and t2 must have the same FloatingPoint sort. def_API('Z3_mk_fpa_lt', AST, (_in(CONTEXT),_in(AST),_in(AST))) */ Z3_ast Z3_API Z3_mk_fpa_lt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); - - + /** \brief Floating-point greater than or equal \param c logical context. - \param t1 floating-point term. - \param t2 floating-point term. + \param t1 term of FloatingPoint sort. + \param t2 term of FloatingPoint sort. - t1 and t2 must have the same floating point sort. + t1 and t2 must have the same FloatingPoint sort. - def_API('Z3_mk_fpa_ge', AST, (_in(CONTEXT),_in(AST),_in(AST))) + def_API('Z3_mk_fpa_geq', AST, (_in(CONTEXT),_in(AST),_in(AST))) */ - Z3_ast Z3_API Z3_mk_fpa_ge(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); + Z3_ast Z3_API Z3_mk_fpa_geq(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); /** \brief Floating-point greater-than \param c logical context. - \param t1 floating-point term. - \param t2 floating-point term. + \param t1 term of FloatingPoint sort. + \param t2 term of FloatingPoint sort. - t1 and t2 must have the same floating point sort. + t1 and t2 must have the same FloatingPoint sort. def_API('Z3_mk_fpa_gt', AST, (_in(CONTEXT),_in(AST),_in(AST))) */ Z3_ast Z3_API Z3_mk_fpa_gt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); - + /** - \brief Predicate indicating whether t is a normal floating point number + \brief Floating-point equality \param c logical context. - \param t floating-point term. + \param t1 term of FloatingPoint sort. + \param t2 term of FloatingPoint sort. - t must have floating point sort. + Note that this is IEEE 754 equality (as opposed to SMT-LIB =). + + t1 and t2 must have the same FloatingPoint sort. + + def_API('Z3_mk_fpa_eq', AST, (_in(CONTEXT),_in(AST),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_eq(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); + + /** + \brief Predicate indicating whether t is a normal floating-point number. + + \param c logical context. + \param t term of FloatingPoint sort. + + t must have FloatingPoint sort. def_API('Z3_mk_fpa_is_normal', AST, (_in(CONTEXT),_in(AST))) */ Z3_ast Z3_API Z3_mk_fpa_is_normal(__in Z3_context c, __in Z3_ast t); /** - \brief Predicate indicating whether t is a subnormal floating point number + \brief Predicate indicating whether t is a subnormal floating-point number. \param c logical context. - \param t floating-point term. + \param t term of FloatingPoint sort. - t must have floating point sort. + t must have FloatingPoint sort. def_API('Z3_mk_fpa_is_subnormal', AST, (_in(CONTEXT),_in(AST))) */ Z3_ast Z3_API Z3_mk_fpa_is_subnormal(__in Z3_context c, __in Z3_ast t); /** - \brief Predicate indicating whether t is a floating point number with zero value, i.e., +0 or -0. + \brief Predicate indicating whether t is a floating-point number with zero value, i.e., +zero or -zero. \param c logical context. - \param t floating-point term. + \param t term of FloatingPoint sort. - t must have floating point sort. + t must have FloatingPoint sort. def_API('Z3_mk_fpa_is_zero', AST, (_in(CONTEXT),_in(AST))) */ Z3_ast Z3_API Z3_mk_fpa_is_zero(__in Z3_context c, __in Z3_ast t); /** - \brief Predicate indicating whether t is a floating point number representing +Inf or -Inf + \brief Predicate indicating whether t is a floating-point number representing +oo or -oo. \param c logical context. - \param t floating-point term. + \param t term of FloatingPoint sort. - t must have floating point sort. + t must have FloatingPoint sort. - def_API('Z3_mk_fpa_is_inf', AST, (_in(CONTEXT),_in(AST))) + def_API('Z3_mk_fpa_is_infinite', AST, (_in(CONTEXT),_in(AST))) */ - Z3_ast Z3_API Z3_mk_fpa_is_inf(__in Z3_context c, __in Z3_ast t); + Z3_ast Z3_API Z3_mk_fpa_is_infinite(__in Z3_context c, __in Z3_ast t); /** \brief Predicate indicating whether t is a NaN \param c logical context. - \param t floating-point term. + \param t term of FloatingPoint sort. - t must have floating point sort. + t must have FloatingPoint sort. def_API('Z3_mk_fpa_is_nan', AST, (_in(CONTEXT),_in(AST))) */ Z3_ast Z3_API Z3_mk_fpa_is_nan(__in Z3_context c, __in Z3_ast t); /** - \brief Minimum of floating point numbers + \brief Predicate indicating whether t is a negative floating-point number. \param c logical context. - \param t1 floating-point term. - \param t2 floating-point term. + \param t term of FloatingPoint sort. - t1, t2 must have the same floating point sort. - - def_API('Z3_mk_fpa_min', AST, (_in(CONTEXT),_in(AST),_in(AST))) - */ - Z3_ast Z3_API Z3_mk_fpa_min(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); - - /** - \brief Maximum of floating point numbers + t must have FloatingPoint sort. - \param c logical context. - \param t1 floating-point term. - \param t2 floating-point term. - - t1, t2 must have the same floating point sort. - - def_API('Z3_mk_fpa_max', AST, (_in(CONTEXT),_in(AST),_in(AST))) - */ - Z3_ast Z3_API Z3_mk_fpa_max(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); + def_API('Z3_mk_fpa_is_negative', AST, (_in(CONTEXT),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_is_negative(__in Z3_context c, __in Z3_ast t); /** - \brief Conversion of a floating point number to another floating-point sort s. - - Produces a term that represents the conversion of a floating-point term t to a different - floating point sort s. If necessary, rounding according to rm is applied. + \brief Predicate indicating whether t is a positive floating-point number. \param c logical context. + \param t term of FloatingPoint sort. + + t must have FloatingPoint sort. + + def_API('Z3_mk_fpa_is_positive', AST, (_in(CONTEXT),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_is_positive(__in Z3_context c, __in Z3_ast t); + + /** + \brief Conversion of a single IEEE 754-2008 bit-vector into a floating-point number. + + Produces a term that represents the conversion of a bit-vector term bv to a + floating-point term of sort s. + + \param c logical context. + \param bv a bit-vector term. \param s floating-point sort. - \param rm rounding mode. - \param t floating-point term. - s must be a floating point sort, rm must have rounding mode sort, and t must have floating point sort. + s must be a FloatingPoint sort, t must be of bit-vector sort, and the bit-vector + size of bv, m, must be equal to ebits+sbits of s. The format of the bit-vector is + as defined by the IEEE 754-2008 interchange format and the resulting floating-point + sort (ebits, sbits) is automatically determined. - def_API('Z3_mk_fpa_convert', AST, (_in(CONTEXT),_in(SORT),_in(AST),_in(AST))) + def_API('Z3_mk_fpa_to_fp_bv', AST, (_in(CONTEXT),_in(AST),_in(SORT))) */ - Z3_ast Z3_API Z3_mk_fpa_convert(__in Z3_context c, __in Z3_sort s, __in Z3_ast rm, __in Z3_ast t); + Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(__in Z3_context c, __in Z3_ast bv, __in Z3_sort s); /** - \brief Conversion of a floating point term to a bit-vector term in IEEE754 format. + \brief Conversion of a floating-point term into another floating-point term of different floating-point sort. + + Produces a term that represents the conversion of a floating-point term t to a + floating-point term of sort s. If necessary, the result will be rounded according + to rounding mode rm. + + \param c logical context. + \param rm term of RoundingMode sort. + \param t term of FloatingPoint sort. + \param s floating-point sort. + + s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of floating-point sort. + + def_API('Z3_mk_fpa_to_fp_float', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT))) + */ + Z3_ast Z3_API Z3_mk_fpa_to_fp_float(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in Z3_sort s); + + /** + \brief Conversion of a term of real sort into a term of FloatingPoint sort. + + Produces a term that represents the conversion of term t of real sort into a + floating-point term of sort s. If necessary, the result will be rounded according + to rounding mode rm. + + \param c logical context. + \param rm term of RoundingMode sort. + \param t term of Real sort. + \param s floating-point sort. + + s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of real sort. + + def_API('Z3_mk_fpa_to_fp_real', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT))) + */ + Z3_ast Z3_API Z3_mk_fpa_to_fp_real(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in Z3_sort s); + + /** + \brief Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort. + + Produces a term that represents the conversion of the bit-vector term t into a + floating-point term of sort s. The bit-vector t is taken to be in signed + 2's complement format. If necessary, the result will be rounded according + to rounding mode rm. + + \param c logical context. + \param rm term of RoundingMode sort. + \param t term of bit-vector sort. + \param s floating-point sort. + + s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of bit-vector sort. + + def_API('Z3_mk_fpa_to_fp_signed', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT))) + */ + Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in Z3_sort s); + + /** + \brief Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort. + + Produces a term that represents the conversion of the bit-vector term t into a + floating-point term of sort s. The bit-vector t is taken to be in unsigned + 2's complement format. If necessary, the result will be rounded according + to rounding mode rm. + + \param c logical context. + \param rm term of RoundingMode sort. + \param t term of bit-vector sort. + \param s floating-point sort. + + s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of bit-vector sort. + + def_API('Z3_mk_fpa_to_fp_unsigned', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT))) + */ + Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in Z3_sort s); + + /** + \brief Conversion of a floating-point term into an unsigned bit-vector. + + Produces a term that represents the conversion of the floating-poiunt term t into a + bit-vector term in unsigned 2's complement format. If necessary, the result will be + rounded according to rounding mode rm. \param c logical context. - \param t floating-point term. + \param rm term of RoundingMode sort. + \param t term of FloatingPoint sort. + \param sz size of the resulting bit-vector. - t must have floating point sort. The size of the resulting bit-vector is automatically determined. + def_API('Z3_mk_fpa_to_ubv', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(UINT))) + */ + Z3_ast Z3_API Z3_mk_fpa_to_ubv(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in unsigned sz); + + /** + \brief Conversion of a floating-point term into a signed bit-vector. + + Produces a term that represents the conversion of the floating-poiunt term t into a + bit-vector term in signed 2's complement format. If necessary, the result will be + rounded according to rounding mode rm. + + \param c logical context. + \param rm term of RoundingMode sort. + \param t term of FloatingPoint sort. + \param sz size of the resulting bit-vector. + + def_API('Z3_mk_fpa_to_sbv', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(UINT))) + */ + Z3_ast Z3_API Z3_mk_fpa_to_sbv(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in unsigned sz); + + /** + \brief Conversion of a floating-point term into a real number. + + Produces a term that represents the conversion of the floating-poiunt term t into a + real number. Note that this type of conversion will often result in non-linear + constraints over real terms. + + \param c logical context. + \param t term of FloatingPoint sort. + + def_API('Z3_mk_fpa_to_real', AST, (_in(CONTEXT),_in(AST))) + */ + Z3_ast Z3_API Z3_mk_fpa_to_real(__in Z3_context c, __in Z3_ast t); + + /** + @name Z3-specific extensions + */ + /*@{*/ + + /** + \brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. + + \param c logical context. + \param t term of FloatingPoint sort. + + t must have FloatingPoint sort. The size of the resulting bit-vector is automatically + determined. + + Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion + knows only one NaN and it will always produce the same bit-vector represenatation of + that NaN. def_API('Z3_mk_fpa_to_ieee_bv', AST, (_in(CONTEXT),_in(AST))) */ Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(__in Z3_context c, __in Z3_ast t); + /** + \brief Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort. + + Produces a term that represents the conversion of sig * 2^exp into a + floating-point term of sort s. If necessary, the result will be rounded + according to rounding mode rm. + + \param c logical context. + \param rm term of RoundingMode sort. + \param sig significand term of Real sort. + \param exp exponent term of Real sort. + \param s floating-point sort. + + s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of real sort. + + def_API('Z3_mk_fpa_to_fp_real_int', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST),_in(SORT))) + */ + Z3_ast Z3_API Z3_mk_fpa_to_fp_real_int(__in Z3_context c, __in Z3_ast rm, __in Z3_ast sig, __in Z3_ast exp, __in Z3_sort s); + + /*@}*/ /*@}*/ /*@}*/ diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index 1598db9c3..cbcd706cd 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -263,9 +263,41 @@ public: bool is_zero(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_zero(v); } bool is_pzero(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_pzero(v); } bool is_nzero(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_nzero(v); } + + app * mk_fp(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_FP, arg1, arg2, arg3); } + app * mk_to_fp(sort * s, expr * bv_t) { + SASSERT(is_float(s) && s->get_num_parameters() == 2); + return m().mk_app(m_fid, OP_FLOAT_TO_FP, 2, s->get_parameters(), 1, &bv_t); + } + app * mk_to_fp(sort * s, expr * rm, expr * t) { + SASSERT(is_float(s) && s->get_num_parameters() == 2); + expr * args[] = { rm, t }; + return m().mk_app(m_fid, OP_FLOAT_TO_FP, 2, s->get_parameters(), 2, args); + } + app * mk_to_fp(sort * s, expr * rm, expr * sig, expr * exp) { + SASSERT(is_float(s) && s->get_num_parameters() == 2); + expr * args[] = { rm, sig, exp }; + return m().mk_app(m_fid, OP_FLOAT_TO_FP, 2, s->get_parameters(), 3, args); + } + app * mk_to_fp_unsigned(sort * s, expr * rm, expr * t) { + SASSERT(is_float(s) && s->get_num_parameters() == 2); + expr * args[] = { rm, t }; + return m().mk_app(m_fid, OP_FLOAT_TO_FP_UNSIGNED, 2, s->get_parameters(), 2, args); + } bool is_to_fp(expr * n) { return is_app_of(n, m_fid, OP_FLOAT_TO_FP); } - + + app * mk_to_ubv(expr * rm, expr * t, unsigned sz) { + parameter ps[] = { parameter(sz) }; + expr * args[] = { rm, t }; + return m().mk_app(m_fid, OP_FLOAT_TO_UBV, 1, ps, 2, args); } + app * mk_to_sbv(expr * rm, expr * t, unsigned sz) { + parameter ps[] = { parameter(sz) }; + expr * args[] = { rm, t }; + return m().mk_app(m_fid, OP_FLOAT_TO_SBV, 1, ps, 2, args); + } + app * mk_to_real(expr * t) { return m().mk_app(m_fid, OP_FLOAT_TO_REAL, t); } + app * mk_add(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_ADD, arg1, arg2, arg3); } app * mk_mul(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_MUL, arg1, arg2, arg3); } app * mk_sub(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_SUB, arg1, arg2, arg3); } @@ -276,7 +308,7 @@ public: app * mk_min(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_MIN, arg1, arg2); } app * mk_abs(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_ABS, arg1); } app * mk_sqrt(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_SQRT, arg1, arg2); } - app * mk_round(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_ROUND_TO_INTEGRAL, arg1, arg2); } + app * mk_round_to_integral(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_ROUND_TO_INTEGRAL, arg1, arg2); } app * mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4) { expr * args[4] = { arg1, arg2, arg3, arg4 }; return m().mk_app(m_fid, OP_FLOAT_FMA, 4, args); @@ -306,6 +338,9 @@ public: app * mk_internal_to_ubv_unspecified(unsigned width); app * mk_internal_to_sbv_unspecified(unsigned width); app * mk_internal_to_real_unspecified(); + + bool is_wrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FLOAT_INTERNAL_BVWRAP); } + bool is_unwrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FLOAT_INTERNAL_BVUNWRAP); } }; #endif diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index f7fd1de30..03a2e73bf 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -48,13 +48,11 @@ namespace smt { } else { sort * s = f->get_range(); - func_decl_ref w(m), u(m); - m_th.get_wrap(s, w, u); expr_ref bv(m); - bv = m.mk_app(w, m.mk_const(f)); + bv = m_th.wrap(m.mk_const(f)); unsigned bv_sz = m_th.m_bv_util.get_bv_size(bv); - unsigned ebits = m_th.m_float_util.get_ebits(f->get_range()); - unsigned sbits = m_th.m_float_util.get_sbits(f->get_range()); + unsigned ebits = m_th.m_float_util.get_ebits(s); + unsigned sbits = m_th.m_float_util.get_sbits(s); SASSERT(bv_sz == ebits + sbits); m_th.m_converter.mk_triple(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv), m_bv_util.mk_extract(sbits - 2, 0, bv), @@ -76,12 +74,7 @@ namespace smt { } else { SASSERT(is_rm(f->get_range())); - - sort * s = f->get_range(); - func_decl_ref w(m), u(m); - m_th.get_wrap(s, w, u); - result = m.mk_app(w, m.mk_const(f)); - + result = m_th.wrap(m.mk_const(f)); m_rm_const2bv.insert(f, result); m.inc_ref(f); m.inc_ref(result); @@ -133,13 +126,15 @@ namespace smt { SASSERT(bv_sz == (m_ebits+m_sbits)); SASSERT(all_rat.is_int()); mpzm.set(all_bits, all_rat.to_mpq().numerator()); - + scoped_mpz sgn_z(mpzm), sig_z(mpzm), exp_z(mpzm); mpzm.machine_div2k(all_bits, m_ebits + m_sbits - 1, sgn_z); mpzm.mod(all_bits, mpfm.m_powers2(m_ebits + m_sbits - 1), all_bits); mpzm.machine_div2k(all_bits, m_sbits - 1, exp_z); mpzm.mod(all_bits, mpfm.m_powers2(m_sbits - 1), all_bits); + + mpzm.set(sig_z, all_bits); TRACE("t_fpa_detail", tout << "sgn=" << mpzm.to_string(sgn_z) << " ; " << "sig=" << mpzm.to_string(sig_z) << " ; " << @@ -190,36 +185,53 @@ namespace smt { return result; } - void theory_fpa::get_wrap(sort * s, func_decl_ref & wrap, func_decl_ref & unwrap) - { - func_decl *w, *u; + app_ref theory_fpa::wrap(expr * e) { + SASSERT(!m_float_util.is_wrap(e)); + ast_manager & m = get_manager(); + context & ctx = get_context(); + sort * e_srt = m.get_sort(e); - if (!m_wraps.find(s, w) || !m_unwraps.find(s, u)) { - SASSERT(!m_wraps.contains(s)); - SASSERT(!m_unwraps.contains(s)); - ast_manager & m = get_manager(); - context & ctx = get_context(); + func_decl *w; + + if (!m_wraps.find(e_srt, w)) { + SASSERT(!m_wraps.contains(e_srt)); + sort * bv_srt = 0; - if (m_converter.is_rm(s)) + if (m_converter.is_rm(e_srt)) bv_srt = m_bv_util.mk_sort(3); else { - SASSERT(m_converter.is_float(s)); - unsigned ebits = m_float_util.get_ebits(s); - unsigned sbits = m_float_util.get_sbits(s); + SASSERT(m_converter.is_float(e_srt)); + unsigned ebits = m_float_util.get_ebits(e_srt); + unsigned sbits = m_float_util.get_sbits(e_srt); bv_srt = m_bv_util.mk_sort(ebits + sbits); } - w = m.mk_func_decl(get_family_id(), OP_FLOAT_INTERNAL_BVWRAP, 0, 0, 1, &s, bv_srt); + w = m.mk_func_decl(get_family_id(), OP_FLOAT_INTERNAL_BVWRAP, 0, 0, 1, &e_srt, bv_srt); + m_wraps.insert(e_srt, w); + m.inc_ref(w); + } + + return app_ref(m.mk_app(w, e), m); + } + + app_ref theory_fpa::unwrap(expr * e, sort * s) { + SASSERT(!m_float_util.is_unwrap(e)); + ast_manager & m = get_manager(); + context & ctx = get_context(); + sort * e_srt = m.get_sort(e); + + func_decl *u; + + if (!m_unwraps.find(e_srt, u)) { + SASSERT(!m_unwraps.contains(e_srt)); + sort * bv_srt = m.get_sort(e); u = m.mk_func_decl(get_family_id(), OP_FLOAT_INTERNAL_BVUNWRAP, 0, 0, 1, &bv_srt, s); - m_wraps.insert(s, w); m_unwraps.insert(s, u); - m.inc_ref(w); m.inc_ref(u); } - wrap = w; - unwrap = u; + return app_ref(m.mk_app(u, e), m); } expr_ref theory_fpa::convert_atom(expr * e) { @@ -235,32 +247,39 @@ namespace smt { expr_ref theory_fpa::convert_term(expr * e) { ast_manager & m = get_manager(); + TRACE("t_fpa_detail", tout << "converting: " << mk_ismt2_pp(e, m) << " sort is: " << mk_ismt2_pp(m.get_sort(e), m) << std::endl;); + context & ctx = get_context(); - expr_ref res(m); + expr_ref ec(m), res(m); proof_ref pr(m); - m_rw(e, res); - - SASSERT(is_app(res)); - - if (m_float_util.is_rm(e)) { - SASSERT(is_sort_of(m.get_sort(res), m_bv_util.get_family_id(), BV_SORT)); - SASSERT(m_bv_util.get_bv_size(res) == 3); - ctx.internalize(res, false); - m_th_rw(res, res); + m_rw(e, ec); + + SASSERT(is_app(ec)); + app_ref eca(to_app(ec), m); + TRACE("t_fpa_detail", tout << "eca = " << mk_ismt2_pp(eca, m) << " sort is: " << mk_ismt2_pp(m.get_sort(eca), m) << std::endl;); + + if (m_float_util.is_rm(e)) { + expr_ref bv_rm(m); + bv_rm = eca; + TRACE("t_fpa_detail", tout << "bvrm = " << mk_ismt2_pp(bv_rm, m) << " sort is: " << mk_ismt2_pp(m.get_sort(bv_rm), m) << std::endl;); + SASSERT(is_sort_of(m.get_sort(bv_rm), m_bv_util.get_family_id(), BV_SORT)); + SASSERT(m_bv_util.get_bv_size(bv_rm) == 3); + m_th_rw(bv_rm, res); } else if (m_float_util.is_float(e)) { - SASSERT(to_app(res)->get_family_id() == get_family_id()); - float_op_kind k = (float_op_kind)(to_app(res)->get_decl_kind()); + SASSERT(eca->get_family_id() == get_family_id()); + float_op_kind k = (float_op_kind)(eca->get_decl_kind()); + SASSERT(k == OP_FLOAT_TO_FP || k == OP_FLOAT_INTERNAL_BVUNWRAP); switch (k) { case OP_FLOAT_TO_FP: { - SASSERT(to_app(res)->get_num_args() == 3); - SASSERT(is_sort_of(m.get_sort(to_app(res)->get_arg(0)), m_bv_util.get_family_id(), BV_SORT)); - SASSERT(is_sort_of(m.get_sort(to_app(res)->get_arg(1)), m_bv_util.get_family_id(), BV_SORT)); - SASSERT(is_sort_of(m.get_sort(to_app(res)->get_arg(2)), m_bv_util.get_family_id(), BV_SORT)); - + SASSERT(eca->get_num_args() == 3); + SASSERT(is_sort_of(m.get_sort(eca->get_arg(0)), m_bv_util.get_family_id(), BV_SORT)); + SASSERT(is_sort_of(m.get_sort(eca->get_arg(1)), m_bv_util.get_family_id(), BV_SORT)); + SASSERT(is_sort_of(m.get_sort(eca->get_arg(2)), m_bv_util.get_family_id(), BV_SORT)); + expr *sgn, *sig, *exp; expr_ref s_sgn(m), s_sig(m), s_exp(m); - m_converter.split_triple(res, sgn, sig, exp); + m_converter.split_triple(eca, sgn, sig, exp); m_th_rw(sgn, s_sgn); m_th_rw(sig, s_sig); m_th_rw(exp, s_exp); @@ -269,12 +288,13 @@ namespace smt { break; } default: - /* nothing */; + res = eca; } } else UNREACHABLE(); + SASSERT(res.get() != 0); return res; } @@ -292,6 +312,28 @@ namespace smt { return res; } + expr_ref theory_fpa::convert_unwrap(expr * e) { + SASSERT(m_float_util.is_unwrap(e)); + ast_manager & m = get_manager(); + sort * srt = m.get_sort(e); + expr_ref res(m); + if (m_float_util.is_rm(srt)) { + res = to_app(e)->get_arg(0); + } + else { + SASSERT(m_float_util.is_float(srt)); + unsigned ebits = m_float_util.get_ebits(srt); + unsigned sbits = m_float_util.get_sbits(srt); + expr * bv = to_app(e)->get_arg(0); + unsigned bv_sz = m_bv_util.get_bv_size(bv); + m_converter.mk_triple(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv), + m_bv_util.mk_extract(sbits - 2, 0, bv), + m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv), + res); + } + return res; + } + expr_ref theory_fpa::convert(expr * e) { ast_manager & m = get_manager(); @@ -306,7 +348,9 @@ namespace smt { return res; } else { - if (m.is_bool(e)) + if (m_float_util.is_unwrap(e)) + res = convert_unwrap(e); + else if (m.is_bool(e)) res = convert_atom(e); else if (m_float_util.is_float(e) || m_float_util.is_rm(e)) res = convert_term(e); @@ -452,34 +496,18 @@ namespace smt { if (m_float_util.is_rm(owner_sort)) { // For every RM term, we need to make sure that it's - // associated bit-vector is within the valid range. - // This also ensures that wrap(owner) is internalized. - func_decl_ref wrap(m), unwrap(m); - get_wrap(owner_sort, wrap, unwrap); - if (owner->get_decl() != unwrap) + // associated bit-vector is within the valid range. + if (!m_float_util.is_unwrap(owner)) { - expr_ref wrapped(m), valid(m), limit(m); - wrapped = m.mk_app(wrap, owner.get()); + expr_ref valid(m), limit(m); limit = m_bv_util.mk_numeral(4, 3); - valid = m_bv_util.mk_ule(wrapped, limit); + valid = m_bv_util.mk_ule(wrap(owner), limit); assert_cnstr(valid); } } - else if (m_float_util.is_float(owner_sort)) { - // For every FP term, we need to make sure that - // its wrapped version is also internalized so that - // we can build a model for it later. - func_decl_ref wrap(m), unwrap(m); - get_wrap(owner_sort, wrap, unwrap); - if (owner->get_decl() != unwrap) { - expr_ref wrapped(m); - wrapped = m.mk_app(wrap, owner.get()); - if (!ctx.e_internalized(wrapped)) - ctx.internalize(wrapped, false); - } - } - else - UNREACHABLE(); + + if (!ctx.relevancy() && !m_float_util.is_unwrap(owner)) + assert_cnstr(m.mk_eq(unwrap(wrap(owner), owner_sort), owner)); } void theory_fpa::new_eq_eh(theory_var x, theory_var y) { @@ -498,8 +526,7 @@ namespace smt { app * ye = get_enode(y)->get_owner(); if ((m.is_bool(xe) && m.is_bool(ye)) || - (m_bv_util.is_bv(xe) && m_bv_util.is_bv(ye))) - { + (m_bv_util.is_bv(xe) && m_bv_util.is_bv(ye))) { SASSERT(xe->get_decl()->get_family_id() == get_family_id()); return; } @@ -509,16 +536,13 @@ namespace smt { yc = convert(ye); expr_ref c(m); - + if (fu.is_float(xe) && fu.is_float(ye)) { - func_decl_ref wrap(m), unwrap(m); - get_wrap(m.get_sort(ye), wrap, unwrap); - if (ye->get_decl() == unwrap) - return; expr *x_sgn, *x_sig, *x_exp; m_converter.split_triple(xc, x_sgn, x_sig, x_exp); + expr *y_sgn, *y_sig, *y_exp; m_converter.split_triple(yc, y_sgn, y_sig, y_exp); @@ -614,12 +638,10 @@ namespace smt { if (m_float_util.is_float(n) || m_float_util.is_rm(n)) { sort * s = m.get_sort(n); - func_decl_ref wrap(m), unwrap(m); - get_wrap(s, wrap, unwrap); - if (n->get_decl() != unwrap) { + if (!m_float_util.is_unwrap(n)) { expr_ref wrapped(m), c(m); - wrapped = m.mk_app(wrap, n); + wrapped = wrap(n); mpf_rounding_mode rm; scoped_mpf val(mpfm); if (m_float_util.is_rm_value(n, rm)) { @@ -633,15 +655,13 @@ namespace smt { SASSERT(is_app(bv_val_e)); SASSERT(to_app(bv_val_e)->get_num_args() == 3); app_ref bv_val_a(to_app(bv_val_e.get()), m); - c = m.mk_eq(wrapped, m_bv_util.mk_concat( m_bv_util.mk_concat( - bv_val_a->get_arg(0), - bv_val_a->get_arg(1)), - bv_val_a->get_arg(2))); + expr * args[] = { bv_val_a->get_arg(0), bv_val_a->get_arg(1), bv_val_a->get_arg(2) }; + c = m.mk_eq(wrapped, m_bv_util.mk_concat(3, args)); c = m.mk_and(c, mk_side_conditions()); assert_cnstr(c); } else { - c = m.mk_eq(m.mk_app(unwrap, wrapped), n); + c = m.mk_eq(unwrap(wrapped, m.get_sort(n)), n); assert_cnstr(c); } } @@ -696,11 +716,9 @@ namespace smt { return alloc(expr_wrapper_proc, owner); model_value_proc * res = 0; - func_decl_ref wrap(m), unwrap(m); - get_wrap(m.get_sort(owner), wrap, unwrap); app_ref wrapped(m); - wrapped = m.mk_app(wrap, owner); + wrapped = wrap(owner); CTRACE("t_fpa", !ctx.e_internalized(wrapped), tout << "Model dependency not internalized: " << diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index c21096ec0..c51b02c28 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -176,11 +176,15 @@ namespace smt { expr_ref convert_atom(expr * e); expr_ref convert_term(expr * e); expr_ref convert_conversion_term(expr * e); - void get_wrap(sort * s, func_decl_ref & wrap, func_decl_ref & unwrap); + expr_ref convert_unwrap(expr * e); + void add_trail(ast * a); void attach_new_th_var(enode * n); - void assert_cnstr(expr * e); + void assert_cnstr(expr * e); + + app_ref wrap(expr * e); + app_ref unwrap(expr * e, sort * s); }; }; diff --git a/src/util/mpf.h b/src/util/mpf.h index 83646f9f3..b919e0371 100644 --- a/src/util/mpf.h +++ b/src/util/mpf.h @@ -75,7 +75,7 @@ public: void set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode rm, mpq const & value); void set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode rm, char const * value); void set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode rm, mpq const & significand, mpz const & exponent); - void set(mpf & o, unsigned ebits, unsigned sbits, bool sign, uint64 significand, int exponent); + void set(mpf & o, unsigned ebits, unsigned sbits, bool sign, uint64 significand, mpf_exp_t exponent); void set(mpf & o, unsigned ebits, unsigned sbits, bool sign, mpz const & significand, mpf_exp_t exponent); void set(mpf & o, mpf const & x); void set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode rm, mpf const & x);