mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

FPA: reduced number of temporary variables.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-08-04 17:10:56 +01:00
parent 8b40d4a735
commit 4610acca0f
1 changed files with 16 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -136,12 +136,13 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) {
unsigned sbits = m_util.get_sbits(srt);
expr_ref sgn(m), s(m), e(m);
sort_ref s_sgn(m), s_sig(m), s_exp(m);
s_sgn = m_bv_util.mk_sort(1);
s_sig = m_bv_util.mk_sort(sbits-1);
s_exp = m_bv_util.mk_sort(ebits);
#ifdef Z3DEBUG
sort_ref s_sgn(m), s_sig(m), s_exp(m);
s_sgn = m_bv_util.mk_sort(1);
s_sig = m_bv_util.mk_sort(sbits - 1);
s_exp = m_bv_util.mk_sort(ebits);
std::string p("fpa2bv");
std::string name = f->get_name().str();
@ -149,9 +150,17 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) {
s = m.mk_fresh_const((p + "_sig_" + name).c_str(), s_sig);
e = m.mk_fresh_const((p + "_exp_" + name).c_str(), s_exp);
#else
sgn = m.mk_fresh_const(0, s_sgn);
s = m.mk_fresh_const(0, s_sig);
e = m.mk_fresh_const(0, s_exp);
expr_ref bv(m);
unsigned bv_sz = 1 + ebits + (sbits - 1);
bv = m.mk_fresh_const(0, m_bv_util.mk_sort(bv_sz));
sgn = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv);
e = m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv);
s = m_bv_util.mk_extract(sbits - 2, 0, bv);
SASSERT(m_bv_util.get_bv_size(sgn) == 1);
SASSERT(m_bv_util.get_bv_size(s) == sbits-1);
SASSERT(m_bv_util.get_bv_size(e) == ebits);
#endif
mk_triple(sgn, s, e, result);