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

Fix RoundingMode value generation in FPA theory. Fixes #2239.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2019-04-16 12:50:04 +01:00
parent 6158ea61c8
commit c611fbeaee
No known key found for this signature in database
GPG key ID: BCF6360F86294467
1 changed files with 21 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/smt/theory_fpa.h
View file

@ -47,19 +47,31 @@ namespace smt {
expr * get_some_value(sort * s) override { expr * get_some_value(sort * s) override {
mpf_manager & mpfm = m_util.fm(); mpf_manager & mpfm = m_util.fm();
scoped_mpf q(mpfm);
mpfm.set(q, m_util.get_ebits(s), m_util.get_sbits(s), 0); if (m_util.is_rm(s))
return m_util.mk_value(q); return m_util.mk_round_toward_zero();
else
{
scoped_mpf q(mpfm);
mpfm.set(q, m_util.get_ebits(s), m_util.get_sbits(s), 0);
return m_util.mk_value(q);
}
} }
bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) override { bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) override {
mpf_manager & mpfm = m_util.fm(); mpf_manager & mpfm = m_util.fm();
scoped_mpf q(mpfm);
mpfm.set(q, m_util.get_ebits(s), m_util.get_sbits(s), 0); if (m_util.is_rm(s))
v1 = m_util.mk_value(q); v1 = v2 = m_util.mk_round_toward_zero();
mpfm.set(q, m_util.get_ebits(s), m_util.get_sbits(s), 1); else
v2 = m_util.mk_value(q); {
return true; scoped_mpf q(mpfm);
mpfm.set(q, m_util.get_ebits(s), m_util.get_sbits(s), 0);
v1 = m_util.mk_value(q);
mpfm.set(q, m_util.get_ebits(s), m_util.get_sbits(s), 1);
v2 = m_util.mk_value(q);
}
return true;
} }
expr * get_fresh_value(sort * s) override { return get_some_value(s); } expr * get_fresh_value(sort * s) override { return get_some_value(s); }