From 5e5758bb25e080cb45ae0bd7c6e0a3593e1f6606 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 8 Jan 2015 13:37:18 +0000 Subject: [PATCH] More float -> fpa renaming Signed-off-by: Christoph M. Wintersteiger --- src/api/api_context.cpp | 2 +- src/api/api_context.h | 4 +- src/api/api_fpa.cpp | 146 +++++++++--------- src/api/api_numeral.cpp | 10 +- src/ast/ast_smt2_pp.h | 6 +- src/ast/fpa_decl_plugin.cpp | 26 ++-- src/ast/fpa_decl_plugin.h | 6 +- src/ast/rewriter/fpa_rewriter.h | 2 +- src/cmd_context/cmd_context.cpp | 4 +- src/smt/theory_fpa.cpp | 68 ++++---- src/smt/theory_fpa.h | 14 +- src/tactic/fpa/fpa2bv_model_converter.cpp | 2 +- .../fpa/{qffpa_tactic.cpp => qffp_tactic.cpp} | 8 +- .../fpa/{qffpa_tactic.h => qffp_tactic.h} | 8 +- src/tactic/portfolio/default_tactic.cpp | 2 +- src/tactic/portfolio/smt_strategic_solver.cpp | 6 +- 16 files changed, 158 insertions(+), 156 deletions(-) rename src/tactic/fpa/{qffpa_tactic.cpp => qffp_tactic.cpp} (96%) rename src/tactic/fpa/{qffpa_tactic.h => qffp_tactic.h} (82%) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index b83b72e35..3408cdf3c 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -88,7 +88,7 @@ namespace api { m_arith_util(m()), m_bv_util(m()), m_datalog_util(m()), - m_float_util(m()), + m_fpa_util(m()), m_last_result(m()), m_ast_trail(m()), m_replay_stack() { diff --git a/src/api/api_context.h b/src/api/api_context.h index c71b88b61..6312b3f69 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -57,7 +57,7 @@ namespace api { arith_util m_arith_util; bv_util m_bv_util; datalog::dl_decl_util m_datalog_util; - float_util m_float_util; + fpa_util m_fpa_util; // Support for old solver API smt_params m_fparams; @@ -118,7 +118,7 @@ namespace api { arith_util & autil() { return m_arith_util; } bv_util & bvutil() { return m_bv_util; } datalog::dl_decl_util & datalog_util() { return m_datalog_util; } - float_util & float_util() { return m_float_util; } + fpa_util & fpa_util() { return m_fpa_util; } family_id get_basic_fid() const { return m_basic_fid; } family_id get_array_fid() const { return m_array_fid; } family_id get_arith_fid() const { return m_arith_fid; } diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 0f0f68ae1..94dfaaa68 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -29,7 +29,7 @@ extern "C" { LOG_Z3_mk_fpa_rounding_mode_sort(c); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_sort r = of_sort(ctx->float_util().mk_rm_sort()); + Z3_sort r = of_sort(ctx->fpa_util().mk_rm_sort()); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -40,7 +40,7 @@ extern "C" { LOG_Z3_mk_fpa_round_nearest_ties_to_even(c); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_round_nearest_ties_to_even()); + Z3_ast r = of_ast(ctx->fpa_util().mk_round_nearest_ties_to_even()); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -50,7 +50,7 @@ extern "C" { 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()); + Z3_ast r = of_ast(ctx->fpa_util().mk_round_nearest_ties_to_even()); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -61,7 +61,7 @@ extern "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()); + Z3_ast r = of_ast(ctx->fpa_util().mk_round_nearest_ties_to_away()); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -71,7 +71,7 @@ extern "C" { 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()); + Z3_ast r = of_ast(ctx->fpa_util().mk_round_nearest_ties_to_away()); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -82,7 +82,7 @@ extern "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()); + Z3_ast r = of_ast(ctx->fpa_util().mk_round_toward_positive()); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -92,7 +92,7 @@ extern "C" { 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()); + Z3_ast r = of_ast(ctx->fpa_util().mk_round_toward_positive()); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -103,7 +103,7 @@ extern "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()); + Z3_ast r = of_ast(ctx->fpa_util().mk_round_toward_negative()); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -113,7 +113,7 @@ extern "C" { 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()); + Z3_ast r = of_ast(ctx->fpa_util().mk_round_toward_negative()); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -124,7 +124,7 @@ extern "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()); + Z3_ast r = of_ast(ctx->fpa_util().mk_round_toward_zero()); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -134,7 +134,7 @@ extern "C" { 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()); + Z3_ast r = of_ast(ctx->fpa_util().mk_round_toward_zero()); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -148,7 +148,7 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); } api::context * ctx = mk_c(c); - Z3_sort r = of_sort(ctx->float_util().mk_float_sort(ebits, sbits)); + Z3_sort r = of_sort(ctx->fpa_util().mk_float_sort(ebits, sbits)); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -190,7 +190,7 @@ extern "C" { LOG_Z3_mk_fpa_nan(c, s); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_nan(to_sort(s))); + Z3_ast r = of_ast(ctx->fpa_util().mk_nan(to_sort(s))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -200,7 +200,7 @@ extern "C" { LOG_Z3_mk_fpa_inf(c, s, negative); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(negative != 0 ? ctx->float_util().mk_ninf(to_sort(s)) : ctx->float_util().mk_pinf(to_sort(s))); + Z3_ast r = of_ast(negative != 0 ? ctx->fpa_util().mk_ninf(to_sort(s)) : ctx->fpa_util().mk_pinf(to_sort(s))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -210,7 +210,7 @@ extern "C" { LOG_Z3_mk_fpa_inf(c, s, negative); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(negative != 0 ? ctx->float_util().mk_nzero(to_sort(s)) : ctx->float_util().mk_pzero(to_sort(s))); + Z3_ast r = of_ast(negative != 0 ? ctx->fpa_util().mk_nzero(to_sort(s)) : ctx->fpa_util().mk_pzero(to_sort(s))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -220,7 +220,7 @@ extern "C" { 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))); + Z3_ast r = of_ast(ctx->fpa_util().mk_fp(to_expr(sgn), to_expr(sig), to_expr(exp))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -230,9 +230,9 @@ extern "C" { 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)); + scoped_mpf tmp(ctx->fpa_util().fm()); + ctx->fpa_util().fm().set(tmp, ctx->fpa_util().get_ebits(to_sort(ty)), ctx->fpa_util().get_sbits(to_sort(ty)), v); + Z3_ast r = of_ast(ctx->fpa_util().mk_value(tmp)); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -242,9 +242,9 @@ extern "C" { LOG_Z3_mk_fpa_numeral_double(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)); + scoped_mpf tmp(ctx->fpa_util().fm()); + ctx->fpa_util().fm().set(tmp, ctx->fpa_util().get_ebits(to_sort(ty)), ctx->fpa_util().get_sbits(to_sort(ty)), v); + Z3_ast r = of_ast(ctx->fpa_util().mk_value(tmp)); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -254,12 +254,12 @@ extern "C" { 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)), + scoped_mpf tmp(ctx->fpa_util().fm()); + ctx->fpa_util().fm().set(tmp, + ctx->fpa_util().get_ebits(to_sort(ty)), + ctx->fpa_util().get_sbits(to_sort(ty)), v); - Z3_ast r = of_ast(ctx->float_util().mk_value(tmp)); + Z3_ast r = of_ast(ctx->fpa_util().mk_value(tmp)); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -269,12 +269,12 @@ extern "C" { 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)), + scoped_mpf tmp(ctx->fpa_util().fm()); + ctx->fpa_util().fm().set(tmp, + ctx->fpa_util().get_ebits(to_sort(ty)), + ctx->fpa_util().get_sbits(to_sort(ty)), sgn != 0, sig, exp); - Z3_ast r = of_ast(ctx->float_util().mk_value(tmp)); + Z3_ast r = of_ast(ctx->fpa_util().mk_value(tmp)); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -284,12 +284,12 @@ extern "C" { 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)), + scoped_mpf tmp(ctx->fpa_util().fm()); + ctx->fpa_util().fm().set(tmp, + ctx->fpa_util().get_ebits(to_sort(ty)), + ctx->fpa_util().get_sbits(to_sort(ty)), sgn != 0, sig, exp); - Z3_ast r = of_ast(ctx->float_util().mk_value(tmp)); + Z3_ast r = of_ast(ctx->fpa_util().mk_value(tmp)); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -299,7 +299,7 @@ extern "C" { LOG_Z3_mk_fpa_abs(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_abs(to_expr(t))); + Z3_ast r = of_ast(ctx->fpa_util().mk_abs(to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -309,7 +309,7 @@ extern "C" { LOG_Z3_mk_fpa_neg(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_neg(to_expr(t))); + Z3_ast r = of_ast(ctx->fpa_util().mk_neg(to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -319,7 +319,7 @@ extern "C" { LOG_Z3_mk_fpa_add(c, rm, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_add(to_expr(rm), to_expr(t1), to_expr(t2))); + Z3_ast r = of_ast(ctx->fpa_util().mk_add(to_expr(rm), to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -329,7 +329,7 @@ extern "C" { LOG_Z3_mk_fpa_add(c, rm, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_sub(to_expr(rm), to_expr(t1), to_expr(t2))); + Z3_ast r = of_ast(ctx->fpa_util().mk_sub(to_expr(rm), to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -339,7 +339,7 @@ extern "C" { LOG_Z3_mk_fpa_add(c, rm, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_mul(to_expr(rm), to_expr(t1), to_expr(t2))); + Z3_ast r = of_ast(ctx->fpa_util().mk_mul(to_expr(rm), to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -349,7 +349,7 @@ extern "C" { LOG_Z3_mk_fpa_add(c, rm, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_div(to_expr(rm), to_expr(t1), to_expr(t2))); + Z3_ast r = of_ast(ctx->fpa_util().mk_div(to_expr(rm), to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -359,7 +359,7 @@ extern "C" { LOG_Z3_mk_fpa_fma(c, rm, t1, t2, t3); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_fma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3))); + Z3_ast r = of_ast(ctx->fpa_util().mk_fma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -369,7 +369,7 @@ extern "C" { LOG_Z3_mk_fpa_sqrt(c, rm, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_sqrt(to_expr(rm), to_expr(t))); + Z3_ast r = of_ast(ctx->fpa_util().mk_sqrt(to_expr(rm), to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -379,7 +379,7 @@ extern "C" { LOG_Z3_mk_fpa_rem(c, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_rem(to_expr(t1), to_expr(t2))); + Z3_ast r = of_ast(ctx->fpa_util().mk_rem(to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -389,7 +389,7 @@ extern "C" { 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_round_to_integral(to_expr(rm), to_expr(t))); + Z3_ast r = of_ast(ctx->fpa_util().mk_round_to_integral(to_expr(rm), to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -399,7 +399,7 @@ extern "C" { 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))); + Z3_ast r = of_ast(ctx->fpa_util().mk_min(to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -409,7 +409,7 @@ extern "C" { 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->fpa_util().mk_max(to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -419,7 +419,7 @@ extern "C" { 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))); + Z3_ast r = of_ast(ctx->fpa_util().mk_le(to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -429,7 +429,7 @@ extern "C" { LOG_Z3_mk_fpa_lt(c, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_lt(to_expr(t1), to_expr(t2))); + Z3_ast r = of_ast(ctx->fpa_util().mk_lt(to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -439,7 +439,7 @@ extern "C" { 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))); + Z3_ast r = of_ast(ctx->fpa_util().mk_ge(to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -449,7 +449,7 @@ extern "C" { LOG_Z3_mk_fpa_gt(c, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_gt(to_expr(t1), to_expr(t2))); + Z3_ast r = of_ast(ctx->fpa_util().mk_gt(to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -459,7 +459,7 @@ extern "C" { 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))); + Z3_ast r = of_ast(ctx->fpa_util().mk_float_eq(to_expr(t1), to_expr(t2))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -469,7 +469,7 @@ extern "C" { LOG_Z3_mk_fpa_is_normal(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_is_normal(to_expr(t))); + Z3_ast r = of_ast(ctx->fpa_util().mk_is_normal(to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -479,7 +479,7 @@ extern "C" { LOG_Z3_mk_fpa_is_subnormal(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_is_subnormal(to_expr(t))); + Z3_ast r = of_ast(ctx->fpa_util().mk_is_subnormal(to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -489,7 +489,7 @@ extern "C" { LOG_Z3_mk_fpa_is_zero(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_is_zero(to_expr(t))); + Z3_ast r = of_ast(ctx->fpa_util().mk_is_zero(to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -499,7 +499,7 @@ extern "C" { 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))); + Z3_ast r = of_ast(ctx->fpa_util().mk_is_inf(to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -509,7 +509,7 @@ extern "C" { LOG_Z3_mk_fpa_is_nan(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_is_nan(to_expr(t))); + Z3_ast r = of_ast(ctx->fpa_util().mk_is_nan(to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -519,7 +519,7 @@ extern "C" { 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_is_negative(to_expr(t))); + Z3_ast r = of_ast(ctx->fpa_util().mk_is_negative(to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -529,7 +529,7 @@ extern "C" { LOG_Z3_mk_fpa_is_positive(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_is_positive(to_expr(t))); + Z3_ast r = of_ast(ctx->fpa_util().mk_is_positive(to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -540,7 +540,7 @@ extern "C" { 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(); + fpa_util & fu = ctx->fpa_util(); if (!ctx->bvutil().is_bv(to_expr(bv)) || !fu.is_float(to_sort(s))) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -556,7 +556,7 @@ extern "C" { 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(); + fpa_util & fu = ctx->fpa_util(); if (!fu.is_rm(to_expr(rm)) || !fu.is_float(to_expr(t)) || !fu.is_float(to_sort(s))) { @@ -573,7 +573,7 @@ extern "C" { 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(); + fpa_util & fu = ctx->fpa_util(); if (!fu.is_rm(to_expr(rm)) || !ctx->autil().is_real(to_expr(t)) || !fu.is_float(to_sort(s))) { @@ -590,7 +590,7 @@ extern "C" { 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(); + fpa_util & fu = ctx->fpa_util(); if (!fu.is_rm(to_expr(rm)) || !ctx->bvutil().is_bv(to_expr(t)) || !fu.is_float(to_sort(s))) { @@ -607,7 +607,7 @@ extern "C" { 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(); + fpa_util & fu = ctx->fpa_util(); if (!fu.is_rm(to_expr(rm)) || !ctx->bvutil().is_bv(to_expr(t)) || !fu.is_float(to_sort(s))) { @@ -624,7 +624,7 @@ extern "C" { 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)); + Z3_ast r = of_ast(ctx->fpa_util().mk_to_ubv(to_expr(rm), to_expr(t), sz)); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -634,7 +634,7 @@ extern "C" { 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)); + Z3_ast r = of_ast(ctx->fpa_util().mk_to_sbv(to_expr(rm), to_expr(t), sz)); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -644,7 +644,7 @@ extern "C" { 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))); + Z3_ast r = of_ast(ctx->fpa_util().mk_to_real(to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -654,7 +654,7 @@ extern "C" { LOG_Z3_fpa_get_ebits(c, s); RESET_ERROR_CODE(); CHECK_NON_NULL(s, 0); - return mk_c(c)->float_util().get_ebits(to_sort(s)); + return mk_c(c)->fpa_util().get_ebits(to_sort(s)); Z3_CATCH_RETURN(0); } @@ -663,7 +663,7 @@ extern "C" { LOG_Z3_fpa_get_ebits(c, s); RESET_ERROR_CODE(); CHECK_NON_NULL(s, 0); - return mk_c(c)->float_util().get_sbits(to_sort(s)); + return mk_c(c)->fpa_util().get_sbits(to_sort(s)); Z3_CATCH_RETURN(0); } @@ -672,7 +672,7 @@ extern "C" { LOG_Z3_mk_fpa_to_ieee_bv(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->float_util().mk_float_to_ieee_bv(to_expr(t))); + Z3_ast r = of_ast(ctx->fpa_util().mk_float_to_ieee_bv(to_expr(t))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } @@ -682,7 +682,7 @@ extern "C" { 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(); + fpa_util & fu = ctx->fpa_util(); if (!fu.is_rm(to_expr(rm)) || !ctx->autil().is_real(to_expr(sig)) || !ctx->autil().is_int(to_expr(exp)) || diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index 17a743880..89f01707e 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -59,7 +59,7 @@ extern "C" { RETURN_Z3(0); } sort * _ty = to_sort(ty); - bool is_float = mk_c(c)->float_util().is_float(_ty); + bool is_float = mk_c(c)->fpa_util().is_float(_ty); std::string fixed_num; char const* m = n; while (*m) { @@ -79,7 +79,7 @@ extern "C" { if (_ty->get_family_id() == mk_c(c)->get_fpa_fid()) { // avoid expanding floats into huge rationals. - float_util & fu = mk_c(c)->float_util(); + fpa_util & fu = mk_c(c)->fpa_util(); scoped_mpf t(fu.fm()); fu.fm().set(t, fu.get_ebits(_ty), fu.get_sbits(_ty), MPF_ROUND_TOWARD_ZERO, n); a = fu.mk_value(t); @@ -149,7 +149,7 @@ extern "C" { return mk_c(c)->autil().is_numeral(e) || mk_c(c)->bvutil().is_numeral(e) || - mk_c(c)->float_util().is_value(e); + mk_c(c)->fpa_util().is_value(e); Z3_CATCH_RETURN(Z3_FALSE); } @@ -191,9 +191,9 @@ extern "C" { } else { // floats are separated from all others to avoid huge rationals. - float_util & fu = mk_c(c)->float_util(); + fpa_util & fu = mk_c(c)->fpa_util(); scoped_mpf tmp(fu.fm()); - if (mk_c(c)->float_util().is_value(to_expr(a), tmp)) { + if (mk_c(c)->fpa_util().is_value(to_expr(a), tmp)) { return mk_c(c)->mk_external_string(fu.fm().to_string(tmp)); } else { diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h index bc62448c7..8aac71b8c 100644 --- a/src/ast/ast_smt2_pp.h +++ b/src/ast/ast_smt2_pp.h @@ -46,7 +46,7 @@ public: virtual arith_util & get_autil() = 0; virtual bv_util & get_bvutil() = 0; virtual array_util & get_arutil() = 0; - virtual float_util & get_futil() = 0; + virtual fpa_util & get_futil() = 0; virtual datalog::dl_decl_util& get_dlutil() = 0; virtual bool uses(symbol const & s) const = 0; virtual format_ns::format * pp_fdecl(func_decl * f, unsigned & len); @@ -69,7 +69,7 @@ class smt2_pp_environment_dbg : public smt2_pp_environment { arith_util m_autil; bv_util m_bvutil; array_util m_arutil; - float_util m_futil; + fpa_util m_futil; datalog::dl_decl_util m_dlutil; public: smt2_pp_environment_dbg(ast_manager & m):m_manager(m), m_autil(m), m_bvutil(m), m_arutil(m), m_futil(m), m_dlutil(m) {} @@ -77,7 +77,7 @@ public: virtual arith_util & get_autil() { return m_autil; } virtual bv_util & get_bvutil() { return m_bvutil; } virtual array_util & get_arutil() { return m_arutil; } - virtual float_util & get_futil() { return m_futil; } + virtual fpa_util & get_futil() { return m_futil; } virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; } virtual bool uses(symbol const & s) const { return false; } }; diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index be3e5f3ec..90bbd4901 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -906,7 +906,7 @@ bool fpa_decl_plugin::is_unique_value(app* e) const { } } -float_util::float_util(ast_manager & m): +fpa_util::fpa_util(ast_manager & m): m_manager(m), m_fid(m.mk_family_id("fpa")), m_a_util(m), @@ -914,67 +914,67 @@ float_util::float_util(ast_manager & m): m_plugin = static_cast(m.get_plugin(m_fid)); } -float_util::~float_util() { +fpa_util::~fpa_util() { } -sort * float_util::mk_float_sort(unsigned ebits, unsigned sbits) { +sort * fpa_util::mk_float_sort(unsigned ebits, unsigned sbits) { parameter ps[2] = { parameter(ebits), parameter(sbits) }; return m().mk_sort(m_fid, FLOATING_POINT_SORT, 2, ps); } -unsigned float_util::get_ebits(sort * s) { +unsigned fpa_util::get_ebits(sort * s) { SASSERT(is_float(s)); return static_cast(s->get_parameter(0).get_int()); } -unsigned float_util::get_sbits(sort * s) { +unsigned fpa_util::get_sbits(sort * s) { SASSERT(is_float(s)); return static_cast(s->get_parameter(1).get_int()); } -app * float_util::mk_nan(unsigned ebits, unsigned sbits) { +app * fpa_util::mk_nan(unsigned ebits, unsigned sbits) { scoped_mpf v(fm()); fm().mk_nan(ebits, sbits, v); return mk_value(v); } -app * float_util::mk_pinf(unsigned ebits, unsigned sbits) { +app * fpa_util::mk_pinf(unsigned ebits, unsigned sbits) { scoped_mpf v(fm()); fm().mk_pinf(ebits, sbits, v); return mk_value(v); } -app * float_util::mk_ninf(unsigned ebits, unsigned sbits) { +app * fpa_util::mk_ninf(unsigned ebits, unsigned sbits) { scoped_mpf v(fm()); fm().mk_ninf(ebits, sbits, v); return mk_value(v); } -app * float_util::mk_pzero(unsigned ebits, unsigned sbits) { +app * fpa_util::mk_pzero(unsigned ebits, unsigned sbits) { scoped_mpf v(fm()); fm().mk_pzero(ebits, sbits, v); return mk_value(v); } -app * float_util::mk_nzero(unsigned ebits, unsigned sbits) { +app * fpa_util::mk_nzero(unsigned ebits, unsigned sbits) { scoped_mpf v(fm()); fm().mk_nzero(ebits, sbits, v); return mk_value(v); } -app * float_util::mk_internal_to_ubv_unspecified(unsigned width) { +app * fpa_util::mk_internal_to_ubv_unspecified(unsigned width) { parameter ps[] = { parameter(width) }; sort * range = m_bv_util.mk_sort(width); return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED, 1, ps, 0, 0, range); } -app * float_util::mk_internal_to_sbv_unspecified(unsigned width) { +app * fpa_util::mk_internal_to_sbv_unspecified(unsigned width) { parameter ps[] = { parameter(width) }; sort * range = m_bv_util.mk_sort(width); return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED, 1, ps, 0, 0, range); } -app * float_util::mk_internal_to_real_unspecified() { +app * fpa_util::mk_internal_to_real_unspecified() { sort * range = m_a_util.mk_real(); return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED, 0, 0, 0, 0, range); } \ No newline at end of file diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index b7d59a6af..b8d0c0c3e 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -207,15 +207,15 @@ public: virtual parameter translate(parameter const & p, decl_plugin & target); }; -class float_util { +class fpa_util { ast_manager & m_manager; fpa_decl_plugin * m_plugin; family_id m_fid; arith_util m_a_util; bv_util m_bv_util; public: - float_util(ast_manager & m); - ~float_util(); + fpa_util(ast_manager & m); + ~fpa_util(); ast_manager & m() const { return m_manager; } mpf_manager & fm() const { return m_plugin->fm(); } diff --git a/src/ast/rewriter/fpa_rewriter.h b/src/ast/rewriter/fpa_rewriter.h index 34a34b293..a10df95ca 100644 --- a/src/ast/rewriter/fpa_rewriter.h +++ b/src/ast/rewriter/fpa_rewriter.h @@ -26,7 +26,7 @@ Notes: #include"mpf.h" class fpa_rewriter { - float_util m_util; + fpa_util m_util; mpf_manager m_fm; app * mk_eq_nan(expr * arg); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index d5ee9ff88..f5937955d 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -240,7 +240,7 @@ protected: arith_util m_autil; bv_util m_bvutil; array_util m_arutil; - float_util m_futil; + fpa_util m_futil; datalog::dl_decl_util m_dlutil; format_ns::format * pp_fdecl_name(symbol const & s, func_decls const & fs, func_decl * f, unsigned & len) { @@ -267,7 +267,7 @@ public: virtual arith_util & get_autil() { return m_autil; } virtual bv_util & get_bvutil() { return m_bvutil; } virtual array_util & get_arutil() { return m_arutil; } - virtual float_util & get_futil() { return m_futil; } + virtual fpa_util & get_futil() { return m_futil; } virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; } virtual bool uses(symbol const & s) const { return diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 7c4fce5cd..055f79b9d 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -51,8 +51,8 @@ namespace smt { expr_ref bv(m); 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(s); - unsigned sbits = m_th.m_float_util.get_sbits(s); + unsigned ebits = m_th.m_fpa_util.get_ebits(s); + unsigned sbits = m_th.m_fpa_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), @@ -87,7 +87,7 @@ namespace smt { m_rw(m, m_converter, params_ref()), m_th_rw(m), m_trail_stack(*this), - m_float_util(m_converter.fu()), + m_fpa_util(m_converter.fu()), m_bv_util(m_converter.bu()), m_arith_util(m_converter.au()) { @@ -189,7 +189,7 @@ namespace smt { } app_ref theory_fpa::wrap(expr * e) { - SASSERT(!m_float_util.is_wrap(e)); + SASSERT(!m_fpa_util.is_wrap(e)); ast_manager & m = get_manager(); context & ctx = get_context(); sort * e_srt = m.get_sort(e); @@ -205,8 +205,8 @@ namespace smt { bv_srt = m_bv_util.mk_sort(3); else { 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); + unsigned ebits = m_fpa_util.get_ebits(e_srt); + unsigned sbits = m_fpa_util.get_sbits(e_srt); bv_srt = m_bv_util.mk_sort(ebits + sbits); } @@ -219,7 +219,7 @@ namespace smt { } app_ref theory_fpa::unwrap(expr * e, sort * s) { - SASSERT(!m_float_util.is_unwrap(e)); + SASSERT(!m_fpa_util.is_unwrap(e)); ast_manager & m = get_manager(); context & ctx = get_context(); sort * e_srt = m.get_sort(e); @@ -261,7 +261,7 @@ namespace smt { 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)) { + if (m_fpa_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;); @@ -269,7 +269,7 @@ namespace smt { SASSERT(m_bv_util.get_bv_size(bv_rm) == 3); m_th_rw(bv_rm, res); } - else if (m_float_util.is_float(e)) { + else if (m_fpa_util.is_float(e)) { SASSERT(eca->get_family_id() == get_family_id()); fpa_op_kind k = (fpa_op_kind)(eca->get_decl_kind()); SASSERT(k == OP_FPA_TO_FP || k == OP_FPA_INTERNAL_BVUNWRAP); @@ -316,17 +316,17 @@ namespace smt { } expr_ref theory_fpa::convert_unwrap(expr * e) { - SASSERT(m_float_util.is_unwrap(e)); + SASSERT(m_fpa_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)) { + if (m_fpa_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); + SASSERT(m_fpa_util.is_float(srt)); + unsigned ebits = m_fpa_util.get_ebits(srt); + unsigned sbits = m_fpa_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), @@ -351,11 +351,11 @@ namespace smt { return res; } else { - if (m_float_util.is_unwrap(e)) + if (m_fpa_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)) + else if (m_fpa_util.is_float(e) || m_fpa_util.is_rm(e)) res = convert_term(e); else if (m_arith_util.is_real(e) || m_bv_util.is_bv(e)) res = convert_conversion_term(e); @@ -499,10 +499,10 @@ namespace smt { owner = n->get_owner(); owner_sort = m.get_sort(owner); - if (m_float_util.is_rm(owner_sort)) { + if (m_fpa_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. - if (!m_float_util.is_unwrap(owner)) + if (!m_fpa_util.is_unwrap(owner)) { expr_ref valid(m), limit(m); limit = m_bv_util.mk_numeral(4, 3); @@ -511,7 +511,7 @@ namespace smt { } } - if (!ctx.relevancy() && !m_float_util.is_unwrap(owner)) + if (!ctx.relevancy() && !m_fpa_util.is_unwrap(owner)) assert_cnstr(m.mk_eq(unwrap(wrap(owner), owner_sort), owner)); } @@ -523,7 +523,7 @@ namespace smt { mk_ismt2_pp(get_enode(y)->get_owner(), m) << std::endl;); context & ctx = get_context(); - float_util & fu = m_float_util; + fpa_util & fu = m_fpa_util; bv_util & bu = m_bv_util; mpf_manager & mpfm = fu.fm(); @@ -570,7 +570,7 @@ namespace smt { mk_ismt2_pp(get_enode(y)->get_owner(), m) << std::endl;); context & ctx = get_context(); - mpf_manager & mpfm = m_float_util.fm(); + mpf_manager & mpfm = m_fpa_util.fm(); app * xe = get_enode(x)->get_owner(); app * ye = get_enode(y)->get_owner(); @@ -587,7 +587,7 @@ namespace smt { expr_ref c(m); - if (m_float_util.is_float(xe) && m_float_util.is_float(ye)) + if (m_fpa_util.is_float(xe) && m_fpa_util.is_float(ye)) { expr *x_sgn, *x_sig, *x_exp; m_converter.split_triple(xc, x_sgn, x_sig, x_exp); @@ -636,22 +636,22 @@ namespace smt { ast_manager & m = get_manager(); TRACE("t_fpa", tout << "relevant_eh for: " << mk_ismt2_pp(n, m) << "\n";); - mpf_manager & mpfm = m_float_util.fm(); + mpf_manager & mpfm = m_fpa_util.fm(); unsynch_mpq_manager & mpqm = mpfm.mpq_manager(); - if (m_float_util.is_float(n) || m_float_util.is_rm(n)) { + if (m_fpa_util.is_float(n) || m_fpa_util.is_rm(n)) { sort * s = m.get_sort(n); - if (!m_float_util.is_unwrap(n)) { + if (!m_fpa_util.is_unwrap(n)) { expr_ref wrapped(m), c(m); wrapped = wrap(n); mpf_rounding_mode rm; scoped_mpf val(mpfm); - if (m_float_util.is_rm_value(n, rm)) { + if (m_fpa_util.is_rm_value(n, rm)) { c = m.mk_eq(wrapped, m_bv_util.mk_numeral(rm, 3)); assert_cnstr(c); } - else if (m_float_util.is_value(n, val)) { + else if (m_fpa_util.is_value(n, val)) { unsigned sz = val.get().get_ebits() + val.get().get_sbits(); expr_ref bv_val_e(m); bv_val_e = convert(n); @@ -670,7 +670,7 @@ namespace smt { } } else if (n->get_family_id() == get_family_id()) { - SASSERT(!m_float_util.is_float(n) && !m_float_util.is_rm(n)); + SASSERT(!m_fpa_util.is_float(n) && !m_fpa_util.is_rm(n)); // These are the conversion functions fp.to_* */ } else @@ -714,8 +714,8 @@ namespace smt { // If the owner is not internalized, it doesn't have an enode associated. SASSERT(ctx.e_internalized(owner)); - if (m_float_util.is_rm_value(owner) || - m_float_util.is_value(owner)) + if (m_fpa_util.is_rm_value(owner) || + m_fpa_util.is_value(owner)) return alloc(expr_wrapper_proc, owner); model_value_proc * res = 0; @@ -729,14 +729,14 @@ namespace smt { " (owner " << (!ctx.e_internalized(owner) ? "not" : "is") << " internalized)" << std::endl;); - if (m_float_util.is_rm(owner)) { + if (m_fpa_util.is_rm(owner)) { fpa_rm_value_proc * vp = alloc(fpa_rm_value_proc, this); vp->add_dependency(ctx.get_enode(wrapped)); res = vp; } - else if (m_float_util.is_float(owner)) { - unsigned ebits = m_float_util.get_ebits(m.get_sort(owner)); - unsigned sbits = m_float_util.get_sbits(m.get_sort(owner)); + else if (m_fpa_util.is_float(owner)) { + unsigned ebits = m_fpa_util.get_ebits(m.get_sort(owner)); + unsigned sbits = m_fpa_util.get_sbits(m.get_sort(owner)); fpa_value_proc * vp = alloc(fpa_value_proc, this, ebits, sbits); vp->add_dependency(ctx.get_enode(wrapped)); res = vp; diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index c51b02c28..58af5ad1c 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -29,8 +29,8 @@ Revision History: namespace smt { - class fpa_factory : public value_factory { - float_util m_util; + class fpa_value_actory : public value_factory { + fpa_util m_util; virtual app * mk_value_core(mpf const & val, sort * s) { SASSERT(m_util.get_ebits(s) == val.get_ebits()); @@ -39,11 +39,11 @@ namespace smt { } public: - fpa_factory(ast_manager & m, family_id fid) : + fpa_value_actory(ast_manager & m, family_id fid) : value_factory(m, fid), m_util(m) {} - virtual ~fpa_factory() {} + virtual ~fpa_value_actory() {} virtual expr * get_some_value(sort * s) { mpf_manager & mpfm = m_util.fm(); @@ -87,10 +87,10 @@ namespace smt { class fpa_value_proc : public model_value_proc { protected: - theory_fpa & m_th; + theory_fpa & m_th; ast_manager & m; - float_util & m_fu; - bv_util & m_bu; + fpa_util & m_fu; + bv_util & m_bu; buffer m_deps; unsigned m_ebits; unsigned m_sbits; diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index 78ba64111..dfddfd12f 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -85,7 +85,7 @@ model_converter * fpa2bv_model_converter::translate(ast_translation & translator } void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { - float_util fu(m); + fpa_util fu(m); bv_util bu(m); mpf fp_val; unsynch_mpz_manager & mpzm = fu.fm().mpz_manager(); diff --git a/src/tactic/fpa/qffpa_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp similarity index 96% rename from src/tactic/fpa/qffpa_tactic.cpp rename to src/tactic/fpa/qffp_tactic.cpp index c02166c18..e205a6c5e 100644 --- a/src/tactic/fpa/qffpa_tactic.cpp +++ b/src/tactic/fpa/qffp_tactic.cpp @@ -7,7 +7,7 @@ Module Name: Abstract: - Tactic for QF_FPA benchmarks. + Tactic for QF_FP benchmarks. Author: @@ -23,7 +23,7 @@ Notes: #include"fpa2bv_tactic.h" #include"smt_tactic.h" -#include"qffpa_tactic.h" +#include"qffp_tactic.h" tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) { params_ref simp_p = p; @@ -52,7 +52,7 @@ struct is_non_qffp_predicate { struct found {}; ast_manager & m; bv_util bu; - float_util fu; + fpa_util fu; arith_util au; is_non_qffp_predicate(ast_manager & _m) : m(_m), bu(m), fu(m), au(m) {} @@ -89,4 +89,4 @@ public: probe * mk_is_qffp_probe() { return alloc(is_qffp_probe); } - \ No newline at end of file + diff --git a/src/tactic/fpa/qffpa_tactic.h b/src/tactic/fpa/qffp_tactic.h similarity index 82% rename from src/tactic/fpa/qffpa_tactic.h rename to src/tactic/fpa/qffp_tactic.h index 3ab95798f..2842e3f73 100644 --- a/src/tactic/fpa/qffpa_tactic.h +++ b/src/tactic/fpa/qffp_tactic.h @@ -17,8 +17,8 @@ Notes: --*/ -#ifndef _QFFPA_TACTIC_H_ -#define _QFFPA_TACTIC_H_ +#ifndef _QFFP_TACTIC_H_ +#define _QFFP_TACTIC_H_ #include"params.h" class ast_manager; @@ -27,14 +27,14 @@ class tactic; tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p = params_ref()); /* ADD_TACTIC("qffp", "(try to) solve goal using the tactic for QF_FP.", "mk_qffp_tactic(m, p)") - ADD_TACTIC("qffpbv", "(try to) solve goal using the tactic for QF_FPBV (floats+bit-vectors).", "mk_qffp_tactic(m, p)") + ADD_TACTIC("qffpbv", "(try to) solve goal using the tactic for QF_FPBV (floats+bit-vectors).", "mk_qffpbv_tactic(m, p)") */ probe * mk_is_qffp_probe(); probe * mk_is_qffpbv_probe(); /* ADD_PROBE("is-qffp", "true if the goal is in QF_FP (floats).", "mk_is_qffp_probe()") - ADD_PROBE("is-qffpbv", "true if the goal is in QF_FPBV (floats+bit-vectors).", "mk_is_qffp_probe()") + ADD_PROBE("is-qffpbv", "true if the goal is in QF_FPBV (floats+bit-vectors).", "mk_is_qffpbv_probe()") */ #endif diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index a01b547df..79b3e0e95 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -27,7 +27,7 @@ Notes: #include"nra_tactic.h" #include"probe_arith.h" #include"quant_tactics.h" -#include"qffpa_tactic.h" +#include"qffp_tactic.h" tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { tactic * st = using_params(and_then(mk_simplify_tactic(m), diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 9e0ce6e89..3c62bc80c 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -33,7 +33,7 @@ Notes: #include"qfidl_tactic.h" #include"default_tactic.h" #include"ufbv_tactic.h" -#include"qffpa_tactic.h" +#include"qffp_tactic.h" #include"horn_tactic.h" #include"smt_solver.h" @@ -78,8 +78,10 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const return mk_ufbv_tactic(m, p); else if (logic=="BV") return mk_ufbv_tactic(m, p); - else if (logic=="QF_FP" || logic=="QF_FPBV") + else if (logic=="QF_FP") return mk_qffp_tactic(m, p); + else if (logic == "QF_FPBV") + return mk_qffpbv_tactic(m, p); else if (logic=="HORN") return mk_horn_tactic(m, p); else