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);