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

FPA unified function names

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2014-07-28 19:36:11 +01:00
parent 1abf3beaba
commit 1944283253
3 changed files with 18 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/float_decl_plugin.cpp
View file

@ -106,7 +106,7 @@ bool float_decl_plugin::is_value(expr * n, mpf & val) {
return false; return false;
} }
bool float_decl_plugin::is_rm(expr * n, mpf_rounding_mode & val) { bool float_decl_plugin::is_rm_value(expr * n, mpf_rounding_mode & val) {
if (is_app_of(n, m_family_id, OP_RM_NEAREST_TIES_TO_AWAY)) { if (is_app_of(n, m_family_id, OP_RM_NEAREST_TIES_TO_AWAY)) {
val = MPF_ROUND_NEAREST_TAWAY; val = MPF_ROUND_NEAREST_TAWAY;
return true; return true;

11
src/ast/float_decl_plugin.h
View file

@ -169,7 +169,8 @@ public:
app * mk_value(mpf const & v); app * mk_value(mpf const & v);
bool is_value(expr * n) { return is_app_of(n, m_family_id, OP_FLOAT_VALUE); } bool is_value(expr * n) { return is_app_of(n, m_family_id, OP_FLOAT_VALUE); }
bool is_value(expr * n, mpf & val); bool is_value(expr * n, mpf & val);
bool is_rm(expr * n, mpf_rounding_mode & val); bool is_rm_value(expr * n, mpf_rounding_mode & val);
bool is_rm_value(expr * n) { mpf_rounding_mode t; return is_rm_value(n, t); }
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));
@ -198,7 +199,9 @@ public:
sort * mk_float_sort(unsigned ebits, unsigned sbits); sort * mk_float_sort(unsigned ebits, unsigned sbits);
sort * mk_rm_sort() { return m().mk_sort(m_fid, ROUNDING_MODE_SORT); } sort * mk_rm_sort() { return m().mk_sort(m_fid, ROUNDING_MODE_SORT); }
bool is_float(sort * s) { return is_sort_of(s, m_fid, FLOAT_SORT); } bool is_float(sort * s) { return is_sort_of(s, m_fid, FLOAT_SORT); }
bool is_rm(sort * s) { return is_sort_of(s, m_fid, ROUNDING_MODE_SORT); } bool is_rm(sort * s) { return is_sort_of(s, m_fid, ROUNDING_MODE_SORT); }
bool is_float(expr * e) { return is_float(m_manager.get_sort(e)); }
bool is_rm(expr * e) { return is_rm(m_manager.get_sort(e)); }
unsigned get_ebits(sort * s); unsigned get_ebits(sort * s);
unsigned get_sbits(sort * s); unsigned get_sbits(sort * s);
@ -217,8 +220,8 @@ public:
app * mk_value(mpf const & v) { return m_plugin->mk_value(v); } app * mk_value(mpf const & v) { return m_plugin->mk_value(v); }
bool is_value(expr * n) { return m_plugin->is_value(n); } bool is_value(expr * n) { return m_plugin->is_value(n); }
bool is_value(expr * n, mpf & v) { return m_plugin->is_value(n, v); } bool is_value(expr * n, mpf & v) { return m_plugin->is_value(n, v); }
bool is_rm(expr * n, mpf_rounding_mode & v) { return m_plugin->is_rm(n, v); } bool is_rm_value(expr * n, mpf_rounding_mode & v) { return m_plugin->is_rm_value(n, v); }
app * mk_pzero(unsigned ebits, unsigned sbits); app * mk_pzero(unsigned ebits, unsigned sbits);
app * mk_nzero(unsigned ebits, unsigned sbits); app * mk_nzero(unsigned ebits, unsigned sbits);

21
src/ast/rewriter/float_rewriter.cpp
View file

@ -82,7 +82,7 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
if (num_args == 2) { if (num_args == 2) {
mpf_rounding_mode rm; mpf_rounding_mode rm;
if (!m_util.is_rm(args[0], rm)) if (!m_util.is_rm_value(args[0], rm))
return BR_FAILED; return BR_FAILED;
rational q; rational q;
@ -109,12 +109,12 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
return BR_FAILED; return BR_FAILED;
} }
else if (num_args == 3 && else if (num_args == 3 &&
m_util.is_rm(m().get_sort(args[0])) && m_util.is_rm(args[0]) &&
m_util.au().is_real(args[1]) && m_util.au().is_real(args[1]) &&
m_util.au().is_int(args[2])) { m_util.au().is_int(args[2])) {
mpf_rounding_mode rm; mpf_rounding_mode rm;
if (!m_util.is_rm(args[0], rm)) if (!m_util.is_rm_value(args[0], rm))
return BR_FAILED; return BR_FAILED;
rational q; rational q;
@ -129,8 +129,7 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
mpf v; mpf v;
m_util.fm().set(v, ebits, sbits, rm, q.to_mpq(), e.to_mpq().numerator()); m_util.fm().set(v, ebits, sbits, rm, q.to_mpq(), e.to_mpq().numerator());
result = m_util.mk_value(v); result = m_util.mk_value(v);
m_util.fm().del(v); m_util.fm().del(v);
// TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
return BR_DONE; return BR_DONE;
} }
else { else {
@ -140,7 +139,7 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
br_status float_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { br_status float_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
mpf_rounding_mode rm; mpf_rounding_mode rm;
if (m_util.is_rm(arg1, rm)) { if (m_util.is_rm_value(arg1, rm)) {
scoped_mpf v2(m_util.fm()), v3(m_util.fm()); scoped_mpf v2(m_util.fm()), v3(m_util.fm());
if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) { if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) {
scoped_mpf t(m_util.fm()); scoped_mpf t(m_util.fm());
@ -161,7 +160,7 @@ br_status float_rewriter::mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref
br_status float_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { br_status float_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
mpf_rounding_mode rm; mpf_rounding_mode rm;
if (m_util.is_rm(arg1, rm)) { if (m_util.is_rm_value(arg1, rm)) {
scoped_mpf v2(m_util.fm()), v3(m_util.fm()); scoped_mpf v2(m_util.fm()), v3(m_util.fm());
if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) { if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) {
scoped_mpf t(m_util.fm()); scoped_mpf t(m_util.fm());
@ -176,7 +175,7 @@ br_status float_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref
br_status float_rewriter::mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { br_status float_rewriter::mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
mpf_rounding_mode rm; mpf_rounding_mode rm;
if (m_util.is_rm(arg1, rm)) { if (m_util.is_rm_value(arg1, rm)) {
scoped_mpf v2(m_util.fm()), v3(m_util.fm()); scoped_mpf v2(m_util.fm()), v3(m_util.fm());
if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) { if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) {
scoped_mpf t(m_util.fm()); scoped_mpf t(m_util.fm());
@ -287,7 +286,7 @@ br_status float_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
br_status float_rewriter::mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) { br_status float_rewriter::mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) {
mpf_rounding_mode rm; mpf_rounding_mode rm;
if (m_util.is_rm(arg1, rm)) { if (m_util.is_rm_value(arg1, rm)) {
scoped_mpf v2(m_util.fm()), v3(m_util.fm()), v4(m_util.fm()); scoped_mpf v2(m_util.fm()), v3(m_util.fm()), v4(m_util.fm());
if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3) && m_util.is_value(arg4, v4)) { if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3) && m_util.is_value(arg4, v4)) {
scoped_mpf t(m_util.fm()); scoped_mpf t(m_util.fm());
@ -302,7 +301,7 @@ br_status float_rewriter::mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, exp
br_status float_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) { br_status float_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) {
mpf_rounding_mode rm; mpf_rounding_mode rm;
if (m_util.is_rm(arg1, rm)) { if (m_util.is_rm_value(arg1, rm)) {
scoped_mpf v2(m_util.fm()); scoped_mpf v2(m_util.fm());
if (m_util.is_value(arg2, v2)) { if (m_util.is_value(arg2, v2)) {
scoped_mpf t(m_util.fm()); scoped_mpf t(m_util.fm());
@ -317,7 +316,7 @@ br_status float_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) {
br_status float_rewriter::mk_round(expr * arg1, expr * arg2, expr_ref & result) { br_status float_rewriter::mk_round(expr * arg1, expr * arg2, expr_ref & result) {
mpf_rounding_mode rm; mpf_rounding_mode rm;
if (m_util.is_rm(arg1, rm)) { if (m_util.is_rm_value(arg1, rm)) {
scoped_mpf v2(m_util.fm()); scoped_mpf v2(m_util.fm());
if (m_util.is_value(arg2, v2)) { if (m_util.is_value(arg2, v2)) {
scoped_mpf t(m_util.fm()); scoped_mpf t(m_util.fm());