mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2014-11-12 20:28:36 -08:00
commit 025d6c3108
3 changed files with 24 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2155,15 +2155,15 @@ void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * arg
SASSERT(f->get_num_parameters() == 1);
SASSERT(f->get_parameter(0).is_int());
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
int width = f->get_parameter(0).get_int();
//unsigned ebits = m_util.get_ebits(f->get_range());
//unsigned sbits = m_util.get_sbits(f->get_range());
//int width = f->get_parameter(0).get_int();
expr * rm = args[0];
expr * x = args[1];
//expr * rm = args[0];
//expr * x = args[1];
expr * sgn, *s, *e;
split(x, sgn, s, e);
//expr * sgn, *s, *e;
//split(x, sgn, s, e);
NOT_IMPLEMENTED_YET();
}
@ -2173,15 +2173,15 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
SASSERT(f->get_num_parameters() == 1);
SASSERT(f->get_parameter(0).is_int());
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
int width = f->get_parameter(0).get_int();
//unsigned ebits = m_util.get_ebits(f->get_range());
//unsigned sbits = m_util.get_sbits(f->get_range());
//int width = f->get_parameter(0).get_int();
expr * rm = args[0];
expr * x = args[1];
//expr * rm = args[0];
//expr * x = args[1];
expr * sgn, *s, *e;
split(x, sgn, s, e);
//expr * sgn, *s, *e;
//split(x, sgn, s, e);
NOT_IMPLEMENTED_YET();
}
@ -2189,15 +2189,15 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 1);
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
int width = f->get_parameter(0).get_int();
//unsigned ebits = m_util.get_ebits(f->get_range());
//unsigned sbits = m_util.get_sbits(f->get_range());
//int width = f->get_parameter(0).get_int();
expr * rm = args[0];
expr * x = args[1];
//expr * rm = args[0];
//expr * x = args[1];
expr * sgn, *s, *e;
split(x, sgn, s, e);
//expr * sgn, *s, *e;
//split(x, sgn, s, e);
NOT_IMPLEMENTED_YET();
}