mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

Internal consistency: FP exponents are always passed before significands.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-01-04 18:57:15 +00:00
parent 758c9cd7a0
commit 677ff221f8
9 changed files with 256 additions and 256 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/api/api_fpa.cpp
View file

@ -275,7 +275,7 @@ extern "C" {
RETURN_Z3(0); RETURN_Z3(0);
} }
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
expr * a = ctx->fpautil().mk_fp(to_expr(sgn), to_expr(sig), to_expr(exp)); expr * a = ctx->fpautil().mk_fp(to_expr(sgn), to_expr(exp), to_expr(sig));
ctx->save_ast_trail(a); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a)); RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
@ -351,7 +351,7 @@ extern "C" {
ctx->fpautil().fm().set(tmp, ctx->fpautil().fm().set(tmp,
ctx->fpautil().get_ebits(to_sort(ty)), ctx->fpautil().get_ebits(to_sort(ty)),
ctx->fpautil().get_sbits(to_sort(ty)), ctx->fpautil().get_sbits(to_sort(ty)),
sgn != 0, sig, exp); sgn != 0, exp, sig);
expr * a = ctx->fpautil().mk_value(tmp); expr * a = ctx->fpautil().mk_value(tmp);
ctx->save_ast_trail(a); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a)); RETURN_Z3(of_expr(a));
@ -371,7 +371,7 @@ extern "C" {
ctx->fpautil().fm().set(tmp, ctx->fpautil().fm().set(tmp,
ctx->fpautil().get_ebits(to_sort(ty)), ctx->fpautil().get_ebits(to_sort(ty)),
ctx->fpautil().get_sbits(to_sort(ty)), ctx->fpautil().get_sbits(to_sort(ty)),
sgn != 0, sig, exp); sgn != 0, exp, sig);
expr * a = ctx->fpautil().mk_value(tmp); expr * a = ctx->fpautil().mk_value(tmp);
ctx->save_ast_trail(a); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a)); RETURN_Z3(of_expr(a));

10
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -2505,11 +2505,11 @@ void fpa2bv_converter::mk_to_fp_real_int(func_decl * f, unsigned num, expr * con
return mk_pzero(f, result); return mk_pzero(f, result);
else { else {
scoped_mpf nte(m_mpf_manager), nta(m_mpf_manager), tp(m_mpf_manager), tn(m_mpf_manager), tz(m_mpf_manager); scoped_mpf nte(m_mpf_manager), nta(m_mpf_manager), tp(m_mpf_manager), tn(m_mpf_manager), tz(m_mpf_manager);
m_mpf_manager.set(nte, ebits, sbits, MPF_ROUND_NEAREST_TEVEN, q.to_mpq(), e.to_mpq().numerator()); m_mpf_manager.set(nte, ebits, sbits, MPF_ROUND_NEAREST_TEVEN, e.to_mpq().numerator(), q.to_mpq());
m_mpf_manager.set(nta, ebits, sbits, MPF_ROUND_NEAREST_TAWAY, q.to_mpq(), e.to_mpq().numerator()); m_mpf_manager.set(nta, ebits, sbits, MPF_ROUND_NEAREST_TAWAY, e.to_mpq().numerator(), q.to_mpq());
m_mpf_manager.set(tp, ebits, sbits, MPF_ROUND_TOWARD_POSITIVE, q.to_mpq(), e.to_mpq().numerator()); m_mpf_manager.set(tp, ebits, sbits, MPF_ROUND_TOWARD_POSITIVE, e.to_mpq().numerator(), q.to_mpq());
m_mpf_manager.set(tn, ebits, sbits, MPF_ROUND_TOWARD_NEGATIVE, q.to_mpq(), e.to_mpq().numerator()); m_mpf_manager.set(tn, ebits, sbits, MPF_ROUND_TOWARD_NEGATIVE, e.to_mpq().numerator(), q.to_mpq());
m_mpf_manager.set(tz, ebits, sbits, MPF_ROUND_TOWARD_ZERO, q.to_mpq(), e.to_mpq().numerator()); m_mpf_manager.set(tz, ebits, sbits, MPF_ROUND_TOWARD_ZERO, e.to_mpq().numerator(), q.to_mpq());
app_ref a_nte(m), a_nta(m), a_tp(m), a_tn(m), a_tz(m); app_ref a_nte(m), a_nta(m), a_tp(m), a_tn(m), a_tz(m);
a_nte = m_plugin->mk_numeral(nte); a_nte = m_plugin->mk_numeral(nte);

44
src/ast/fpa_decl_plugin.h
View file

@ -24,7 +24,7 @@ Revision History:
#include"arith_decl_plugin.h" #include"arith_decl_plugin.h"
#include"bv_decl_plugin.h" #include"bv_decl_plugin.h"
#include"mpf.h" #include"mpf.h"
enum fpa_sort_kind { enum fpa_sort_kind {
FLOATING_POINT_SORT, FLOATING_POINT_SORT,
ROUNDING_MODE_SORT, ROUNDING_MODE_SORT,
@ -89,16 +89,16 @@ enum fpa_op_kind {
/* Internal use only */ /* Internal use only */
OP_FPA_INTERNAL_RM, // Internal conversion from (_ BitVec 3) to RoundingMode OP_FPA_INTERNAL_RM, // Internal conversion from (_ BitVec 3) to RoundingMode
OP_FPA_INTERNAL_BVWRAP, OP_FPA_INTERNAL_BVWRAP,
OP_FPA_INTERNAL_BVUNWRAP, OP_FPA_INTERNAL_BVUNWRAP,
OP_FPA_INTERNAL_MIN_I, OP_FPA_INTERNAL_MIN_I,
OP_FPA_INTERNAL_MAX_I, OP_FPA_INTERNAL_MAX_I,
OP_FPA_INTERNAL_MIN_UNSPECIFIED, OP_FPA_INTERNAL_MIN_UNSPECIFIED,
OP_FPA_INTERNAL_MAX_UNSPECIFIED, OP_FPA_INTERNAL_MAX_UNSPECIFIED,
OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED, OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED,
OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED, OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED,
OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED, OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED,
OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED, OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED,
LAST_FLOAT_OP LAST_FLOAT_OP
}; };
@ -115,7 +115,7 @@ class fpa_decl_plugin : public decl_plugin {
mpf_eq_proc(scoped_mpf_vector const & values):m_values(values) {} mpf_eq_proc(scoped_mpf_vector const & values):m_values(values) {}
bool operator()(unsigned id1, unsigned id2) const { return m_values.m().eq_core(m_values[id1], m_values[id2]); } bool operator()(unsigned id1, unsigned id2) const { return m_values.m().eq_core(m_values[id1], m_values[id2]); }
}; };
typedef chashtable<unsigned, mpf_hash_proc, mpf_eq_proc> value_table; typedef chashtable<unsigned, mpf_hash_proc, mpf_eq_proc> value_table;
@ -149,7 +149,7 @@ class fpa_decl_plugin : public decl_plugin {
func_decl * mk_rm_unary_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, func_decl * mk_rm_unary_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range); unsigned arity, sort * const * domain, sort * range);
func_decl * mk_fma(decl_kind k, unsigned num_parameters, parameter const * parameters, func_decl * mk_fma(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range); unsigned arity, sort * const * domain, sort * range);
func_decl * mk_fp(decl_kind k, unsigned num_parameters, parameter const * parameters, func_decl * mk_fp(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range); unsigned arity, sort * const * domain, sort * range);
func_decl * mk_to_fp(decl_kind k, unsigned num_parameters, parameter const * parameters, func_decl * mk_to_fp(decl_kind k, unsigned num_parameters, parameter const * parameters,
@ -184,23 +184,23 @@ class fpa_decl_plugin : public decl_plugin {
public: public:
fpa_decl_plugin(); fpa_decl_plugin();
bool is_float_sort(sort * s) const { return is_sort_of(s, m_family_id, FLOATING_POINT_SORT); } bool is_float_sort(sort * s) const { return is_sort_of(s, m_family_id, FLOATING_POINT_SORT); }
bool is_rm_sort(sort * s) const { return is_sort_of(s, m_family_id, ROUNDING_MODE_SORT); } bool is_rm_sort(sort * s) const { return is_sort_of(s, m_family_id, ROUNDING_MODE_SORT); }
virtual ~fpa_decl_plugin(); virtual ~fpa_decl_plugin();
virtual void finalize(); virtual void finalize();
virtual decl_plugin * mk_fresh(); virtual decl_plugin * mk_fresh();
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters); virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range); unsigned arity, sort * const * domain, sort * range);
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic); virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic); virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
virtual expr * get_some_value(sort * s); virtual expr * get_some_value(sort * s);
virtual bool is_value(app* e) const; virtual bool is_value(app* e) const;
virtual bool is_unique_value(app* e) const; virtual bool is_unique_value(app* e) const;
mpf_manager & fm() { return m_fm; } mpf_manager & fm() { return m_fm; }
func_decl * mk_numeral_decl(mpf const & v); func_decl * mk_numeral_decl(mpf const & v);
app * mk_numeral(mpf const & v); app * mk_numeral(mpf const & v);
@ -209,7 +209,7 @@ public:
bool is_rm_numeral(expr * n, mpf_rounding_mode & val); bool is_rm_numeral(expr * n, mpf_rounding_mode & val);
bool is_rm_numeral(expr * n); bool is_rm_numeral(expr * n);
mpf const & get_value(unsigned id) const { mpf const & get_value(unsigned id) const {
SASSERT(m_value_table.contains(id)); SASSERT(m_value_table.contains(id));
return m_values[id]; return m_values[id];
} }
@ -222,7 +222,7 @@ class fpa_util {
ast_manager & m_manager; ast_manager & m_manager;
fpa_decl_plugin * m_plugin; fpa_decl_plugin * m_plugin;
family_id m_fid; family_id m_fid;
arith_util m_a_util; arith_util m_a_util;
bv_util m_bv_util; bv_util m_bv_util;
public: public:
@ -269,19 +269,19 @@ public:
app * mk_pzero(sort * s) { return mk_pzero(get_ebits(s), get_sbits(s)); } app * mk_pzero(sort * s) { return mk_pzero(get_ebits(s), get_sbits(s)); }
app * mk_nzero(sort * s) { return mk_nzero(get_ebits(s), get_sbits(s)); } app * mk_nzero(sort * s) { return mk_nzero(get_ebits(s), get_sbits(s)); }
bool is_nan(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_nan(v); } bool is_nan(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_nan(v); }
bool is_pinf(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pinf(v); } bool is_pinf(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pinf(v); }
bool is_ninf(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_ninf(v); } bool is_ninf(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_ninf(v); }
bool is_zero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_zero(v); } bool is_zero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_zero(v); }
bool is_pzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pzero(v); } bool is_pzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pzero(v); }
bool is_nzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_nzero(v); } bool is_nzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_nzero(v); }
app * mk_fp(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FPA_FP, arg1, arg2, arg3); } app * mk_fp(expr * sgn, expr * exp, expr * sig) { return m().mk_app(m_fid, OP_FPA_FP, sgn, exp, sig); }
app * mk_to_fp(sort * s, expr * bv_t) { app * mk_to_fp(sort * s, expr * bv_t) {
SASSERT(is_float(s) && s->get_num_parameters() == 2); SASSERT(is_float(s) && s->get_num_parameters() == 2);
return m().mk_app(m_fid, OP_FPA_TO_FP, 2, s->get_parameters(), 1, &bv_t); return m().mk_app(m_fid, OP_FPA_TO_FP, 2, s->get_parameters(), 1, &bv_t);
} }
app * mk_to_fp(sort * s, expr * rm, expr * t) { app * mk_to_fp(sort * s, expr * rm, expr * t) {
SASSERT(is_float(s) && s->get_num_parameters() == 2); SASSERT(is_float(s) && s->get_num_parameters() == 2);
expr * args[] = { rm, t }; expr * args[] = { rm, t };
return m().mk_app(m_fid, OP_FPA_TO_FP, 2, s->get_parameters(), 2, args); return m().mk_app(m_fid, OP_FPA_TO_FP, 2, s->get_parameters(), 2, args);
@ -291,7 +291,7 @@ public:
expr * args[] = { rm, sig, exp }; expr * args[] = { rm, sig, exp };
return m().mk_app(m_fid, OP_FPA_TO_FP, 2, s->get_parameters(), 3, args); return m().mk_app(m_fid, OP_FPA_TO_FP, 2, s->get_parameters(), 3, args);
} }
app * mk_to_fp_unsigned(sort * s, expr * rm, expr * t) { app * mk_to_fp_unsigned(sort * s, expr * rm, expr * t) {
SASSERT(is_float(s) && s->get_num_parameters() == 2); SASSERT(is_float(s) && s->get_num_parameters() == 2);
expr * args[] = { rm, t }; expr * args[] = { rm, t };
return m().mk_app(m_fid, OP_FPA_TO_FP_UNSIGNED, 2, s->get_parameters(), 2, args); return m().mk_app(m_fid, OP_FPA_TO_FP_UNSIGNED, 2, s->get_parameters(), 2, args);
@ -299,11 +299,11 @@ public:
bool is_to_fp(expr * n) { return is_app_of(n, m_fid, OP_FPA_TO_FP); } bool is_to_fp(expr * n) { return is_app_of(n, m_fid, OP_FPA_TO_FP); }
app * mk_to_ubv(expr * rm, expr * t, unsigned sz) { app * mk_to_ubv(expr * rm, expr * t, unsigned sz) {
parameter ps[] = { parameter(sz) }; parameter ps[] = { parameter(sz) };
expr * args[] = { rm, t }; expr * args[] = { rm, t };
return m().mk_app(m_fid, OP_FPA_TO_UBV, 1, ps, 2, args); } return m().mk_app(m_fid, OP_FPA_TO_UBV, 1, ps, 2, args); }
app * mk_to_sbv(expr * rm, expr * t, unsigned sz) { app * mk_to_sbv(expr * rm, expr * t, unsigned sz) {
parameter ps[] = { parameter(sz) }; parameter ps[] = { parameter(sz) };
expr * args[] = { rm, t }; expr * args[] = { rm, t };
return m().mk_app(m_fid, OP_FPA_TO_SBV, 1, ps, 2, args); return m().mk_app(m_fid, OP_FPA_TO_SBV, 1, ps, 2, args);
@ -336,7 +336,7 @@ public:
app * mk_is_inf(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_INF, arg1); } app * mk_is_inf(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_INF, arg1); }
app * mk_is_zero(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_ZERO, arg1); } app * mk_is_zero(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_ZERO, arg1); }
app * mk_is_normal(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_NORMAL, arg1); } app * mk_is_normal(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_NORMAL, arg1); }
app * mk_is_subnormal(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_SUBNORMAL, arg1); } app * mk_is_subnormal(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_SUBNORMAL, arg1); }
app * mk_is_positive(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_POSITIVE, arg1); } app * mk_is_positive(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_POSITIVE, arg1); }
app * mk_is_negative(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_NEGATIVE, arg1); } app * mk_is_negative(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_NEGATIVE, arg1); }

34
src/ast/rewriter/fpa_rewriter.cpp
View file

@ -213,7 +213,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
mpf_exp_t mpf_exp = mpzm.get_int64(exp); mpf_exp_t mpf_exp = mpzm.get_int64(exp);
mpf_exp = m_fm.unbias_exp(ebits, mpf_exp); mpf_exp = m_fm.unbias_exp(ebits, mpf_exp);
m_fm.set(v, ebits, sbits, !mpzm.is_zero(z), sig, mpf_exp); m_fm.set(v, ebits, sbits, !mpzm.is_zero(z), mpf_exp, sig);
TRACE("fp_rewriter", TRACE("fp_rewriter",
tout << "sgn: " << !mpzm.is_zero(z) << std::endl; tout << "sgn: " << !mpzm.is_zero(z) << std::endl;
tout << "sig: " << mpzm.to_string(sig) << std::endl; tout << "sig: " << mpzm.to_string(sig) << std::endl;
@ -267,7 +267,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
return BR_FAILED; return BR_FAILED;
TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";); TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";);
m_fm.set(v, ebits, sbits, rmv, r1.to_mpq(), r2.to_mpq().numerator()); m_fm.set(v, ebits, sbits, rmv, r2.to_mpq().numerator(), r1.to_mpq());
result = m_util.mk_value(v); result = m_util.mk_value(v);
return BR_DONE; return BR_DONE;
} }
@ -281,8 +281,8 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
mpf_exp_t biased_exp = m_fm.mpz_manager().get_int64(r2.to_mpq().numerator()); mpf_exp_t biased_exp = m_fm.mpz_manager().get_int64(r2.to_mpq().numerator());
m_fm.set(v, bvs2, bvs3 + 1, m_fm.set(v, bvs2, bvs3 + 1,
r1.is_one(), r1.is_one(),
r3.to_mpq().numerator(), m_fm.unbias_exp(bvs2, biased_exp),
m_fm.unbias_exp(bvs2, biased_exp)); r3.to_mpq().numerator());
TRACE("fp_rewriter", tout << "v = " << m_fm.to_string(v) << std::endl;); TRACE("fp_rewriter", tout << "v = " << m_fm.to_string(v) << std::endl;);
result = m_util.mk_value(v); result = m_util.mk_value(v);
return BR_DONE; return BR_DONE;
@ -753,23 +753,23 @@ br_status fpa_rewriter::mk_rm(expr * arg, expr_ref & result) {
return BR_FAILED; return BR_FAILED;
} }
br_status fpa_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { br_status fpa_rewriter::mk_fp(expr * sgn, expr * exp, expr * sig, expr_ref & result) {
unsynch_mpz_manager & mpzm = m_fm.mpz_manager(); unsynch_mpz_manager & mpzm = m_fm.mpz_manager();
bv_util bu(m()); bv_util bu(m());
rational r1, r2, r3; rational rsgn, rexp, rsig;
unsigned bvs1, bvs2, bvs3; unsigned bvsz_sgn, bvsz_exp, bvsz_sig;
if (bu.is_numeral(arg1, r1, bvs1) && if (bu.is_numeral(sgn, rsgn, bvsz_sgn) &&
bu.is_numeral(arg2, r2, bvs2) && bu.is_numeral(sig, rsig, bvsz_exp) &&
bu.is_numeral(arg3, r3, bvs3)) { bu.is_numeral(exp, rexp, bvsz_sig)) {
SASSERT(mpzm.is_one(r2.to_mpq().denominator())); SASSERT(mpzm.is_one(rexp.to_mpq().denominator()));
SASSERT(mpzm.is_one(r3.to_mpq().denominator())); SASSERT(mpzm.is_one(rsig.to_mpq().denominator()));
scoped_mpf v(m_fm); scoped_mpf v(m_fm);
mpf_exp_t biased_exp = mpzm.get_int64(r2.to_mpq().numerator()); mpf_exp_t biased_exp = mpzm.get_int64(rexp.to_mpq().numerator());
m_fm.set(v, bvs2, bvs3 + 1, m_fm.set(v, bvsz_exp, bvsz_sig + 1,
r1.is_one(), rsgn.is_one(),
r3.to_mpq().numerator(), m_fm.unbias_exp(bvsz_exp, biased_exp),
m_fm.unbias_exp(bvs2, biased_exp)); rsig.to_mpq().numerator());
TRACE("fp_rewriter", tout << "simplified (fp ...) to " << m_fm.to_string(v) << std::endl;); TRACE("fp_rewriter", tout << "simplified (fp ...) to " << m_fm.to_string(v) << std::endl;);
result = m_util.mk_value(v); result = m_util.mk_value(v);
return BR_DONE; return BR_DONE;

2
src/ast/rewriter/fpa_rewriter.h
View file

@ -79,7 +79,7 @@ public:
br_status mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg2, expr_ref & result); br_status mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);
br_status mk_rm(expr * arg, expr_ref & result); br_status mk_rm(expr * arg, expr_ref & result);
br_status mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); br_status mk_fp(expr * sgn, expr * exp, expr * sig, expr_ref & result);
br_status mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result); br_status mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result); br_status mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);
br_status mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result); br_status mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);

2
src/smt/theory_fpa.cpp
View file

@ -235,7 +235,7 @@ namespace smt {
SASSERT(mpzm.is_int64(exp_u)); SASSERT(mpzm.is_int64(exp_u));
scoped_mpf f(mpfm); scoped_mpf f(mpfm);
mpfm.set(f, m_ebits, m_sbits, mpzm.is_one(sgn_z), sig_z, mpzm.get_int64(exp_u)); mpfm.set(f, m_ebits, m_sbits, mpzm.is_one(sgn_z), mpzm.get_int64(exp_u), sig_z);
result = m_fu.mk_value(f); result = m_fu.mk_value(f);
TRACE("t_fpa", tout << "fpa_value_proc::mk_value [" << TRACE("t_fpa", tout << "fpa_value_proc::mk_value [" <<

2
src/tactic/fpa/fpa2bv_model_converter.cpp
View file

@ -132,7 +132,7 @@ expr_ref fpa2bv_model_converter::convert_bv2fp(sort * s, expr * sgn, expr * exp,
mpzm.set(sig_z, sig_q.to_mpq().numerator()); mpzm.set(sig_z, sig_q.to_mpq().numerator());
exp_z = mpzm.get_int64(exp_unbiased_q.to_mpq().numerator()); exp_z = mpzm.get_int64(exp_unbiased_q.to_mpq().numerator());
fu.fm().set(fp_val, ebits, sbits, !mpqm.is_zero(sgn_q.to_mpq()), sig_z, exp_z); fu.fm().set(fp_val, ebits, sbits, !mpqm.is_zero(sgn_q.to_mpq()), exp_z, sig_z);
mpzm.del(sig_z); mpzm.del(sig_z);

358
src/util/mpf.cpp
View file

File diff suppressed because it is too large Load diff

54
src/util/mpf.h
View file

@ -37,7 +37,7 @@ typedef enum {
typedef int64 mpf_exp_t; typedef int64 mpf_exp_t;
class mpf { class mpf {
friend class mpf_manager; friend class mpf_manager;
friend class scoped_mpf; friend class scoped_mpf;
unsigned ebits:15; unsigned ebits:15;
@ -47,11 +47,11 @@ class mpf {
mpf_exp_t exponent; mpf_exp_t exponent;
mpf & operator=(mpf const & other) { UNREACHABLE(); return *this; } mpf & operator=(mpf const & other) { UNREACHABLE(); return *this; }
void set(unsigned _ebits, unsigned _sbits); void set(unsigned _ebits, unsigned _sbits);
public: public:
mpf(); mpf();
mpf(unsigned ebits, unsigned sbits); mpf(unsigned ebits, unsigned sbits);
mpf(mpf const & other); mpf(mpf const & other);
~mpf(); ~mpf();
unsigned get_ebits() const { return ebits; } unsigned get_ebits() const { return ebits; }
unsigned get_sbits() const { return sbits; } unsigned get_sbits() const { return sbits; }
void swap(mpf & other); void swap(mpf & other);
@ -74,14 +74,14 @@ public:
void set(mpf & o, unsigned ebits, unsigned sbits, double value); void set(mpf & o, unsigned ebits, unsigned sbits, double value);
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, 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, 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, mpf_rounding_mode rm, mpz const & exponent, mpq const & significand);
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, mpf_exp_t exponent, uint64 significand);
void set(mpf & o, unsigned ebits, unsigned sbits, bool sign, mpz const & significand, mpf_exp_t exponent); void set(mpf & o, unsigned ebits, unsigned sbits, bool sign, mpf_exp_t exponent, mpz const & significand);
void set(mpf & o, mpf const & x); void set(mpf & o, mpf const & x);
void set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode rm, mpf const & x); void set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode rm, mpf const & x);
void del(mpf & x) { void del(mpf & x) {
m_mpz_manager.del(x.significand); m_mpz_manager.del(x.significand);
} }
void abs(mpf & o); void abs(mpf & o);
@ -97,14 +97,14 @@ public:
bool is_nzero(mpf const & x); bool is_nzero(mpf const & x);
bool is_pzero(mpf const & x); bool is_pzero(mpf const & x);
// structural eq // structural eq
bool eq_core(mpf const & x, mpf const & y) { bool eq_core(mpf const & x, mpf const & y) {
return return
x.ebits == y.ebits && x.ebits == y.ebits &&
x.sbits == y.sbits && x.sbits == y.sbits &&
x.sign == y.sign && x.sign == y.sign &&
m_mpz_manager.eq(x.significand, y.significand) && m_mpz_manager.eq(x.significand, y.significand) &&
x.exponent == y.exponent; x.exponent == y.exponent;
} }
@ -119,7 +119,7 @@ public:
void add(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf & o); void add(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf & o);
void sub(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf & o); void sub(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf & o);
void mul(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf & o); void mul(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf & o);
void div(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf & o); void div(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf & o);
void fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf const &z, mpf & o); void fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf const &z, mpf & o);
@ -143,10 +143,10 @@ public:
double to_double(mpf const & x); double to_double(mpf const & x);
float to_float(mpf const & x); float to_float(mpf const & x);
bool sgn(mpf const & x) const { return x.sign; } bool sgn(mpf const & x) const { return x.sign; }
const mpz & sig(mpf const & x) const { return x.significand; } const mpz & sig(mpf const & x) const { return x.significand; }
void sig_normalized(mpf const & x, mpz & res) { void sig_normalized(mpf const & x, mpz & res) {
mpf t; mpf t;
set(t, x); set(t, x);
unpack(t, true); unpack(t, true);
@ -154,7 +154,7 @@ public:
del(t); del(t);
} }
const mpf_exp_t & exp(mpf const & x) const { return x.exponent; } const mpf_exp_t & exp(mpf const & x) const { return x.exponent; }
mpf_exp_t exp_normalized(mpf const & x) { mpf_exp_t exp_normalized(mpf const & x) {
mpf t; mpf t;
set(t, x); set(t, x);
unpack(t, true); unpack(t, true);
@ -186,9 +186,9 @@ public:
unsynch_mpz_manager & mpz_manager(void) { return m_mpz_manager; } unsynch_mpz_manager & mpz_manager(void) { return m_mpz_manager; }
unsynch_mpq_manager & mpq_manager(void) { return m_mpq_manager; } unsynch_mpq_manager & mpq_manager(void) { return m_mpq_manager; }
unsigned hash(mpf const & a) { unsigned hash(mpf const & a) {
return hash_u_u(m_mpz_manager.hash(a.significand), return hash_u_u(m_mpz_manager.hash(a.significand),
m_mpz_manager.hash(hash_ull(a.exponent))); m_mpz_manager.hash(hash_ull(a.exponent)));
} }
void mk_max_value(unsigned ebits, unsigned sbits, bool sign, mpf & o); void mk_max_value(unsigned ebits, unsigned sbits, bool sign, mpf & o);
@ -202,7 +202,7 @@ public:
/** /**
\brief Return the biggest k s.t. 2^k <= a. \brief Return the biggest k s.t. 2^k <= a.
\remark Return 0 if a is not positive. \remark Return 0 if a is not positive.
*/ */
unsigned prev_power_of_two(mpf const & a); unsigned prev_power_of_two(mpf const & a);
@ -216,16 +216,16 @@ protected:
bool has_bot_exp(mpf const & x); bool has_bot_exp(mpf const & x);
bool has_top_exp(mpf const & x); bool has_top_exp(mpf const & x);
void unpack(mpf & o, bool normalize); void unpack(mpf & o, bool normalize);
void add_sub(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf & o, bool sub); void add_sub(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf & o, bool sub);
void round(mpf_rounding_mode rm, mpf & o); void round(mpf_rounding_mode rm, mpf & o);
void round_sqrt(mpf_rounding_mode rm, mpf & o); void round_sqrt(mpf_rounding_mode rm, mpf & o);
void mk_round_inf(mpf_rounding_mode rm, mpf & o); void mk_round_inf(mpf_rounding_mode rm, mpf & o);
// Convert x into a mpz numeral. zm is the manager that owns o. // Convert x into a mpz numeral. zm is the manager that owns o.
void to_mpz(mpf const & x, unsynch_mpz_manager & zm, mpz & o); void to_mpz(mpf const & x, unsynch_mpz_manager & zm, mpz & o);
void to_mpz(mpf const & x, scoped_mpz & o) { to_mpz(x, o.m(), o); } void to_mpz(mpf const & x, scoped_mpz & o) { to_mpz(x, o.m(), o); }
class powers2 { class powers2 {
unsynch_mpz_manager & m; unsynch_mpz_manager & m;
@ -239,7 +239,7 @@ protected:
dispose(m_p); dispose(m_p);
dispose(m_pn); dispose(m_pn);
dispose(m_pm1); dispose(m_pm1);
dispose(m_pm1n); dispose(m_pm1n);
} }
void dispose(u_map<mpz*> & map) { void dispose(u_map<mpz*> & map) {
@ -275,7 +275,7 @@ protected:
m.dec(*new_obj); m.dec(*new_obj);
if (negated) m.neg(*new_obj); if (negated) m.neg(*new_obj);
return *new_obj; return *new_obj;
} }
} }
}; };