mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

eliminated unused variables

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2014-11-07 16:04:02 +00:00
parent cf8ad072d0
commit 005bb82a17
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();
}

2
src/interp/iz3base.h
View file

@ -161,7 +161,7 @@ class iz3base : public iz3mgr, public scopes {
stl_ext::hash_map<ast,ast> simplify_memo;
stl_ext::hash_map<ast,int> frame_map; // map assertions to frames
int frames; // number of frames
// int frames; // number of frames
protected:
void add_frame_range(int frame, ast t);

3
src/interp/iz3proof_itp.cpp
View file

@ -2747,7 +2747,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast orig_e = e;
pf = make_refl(e); // proof that e = e
prover::range erng = pv->ast_scope(e);
// prover::range erng =
pv->ast_scope(e);
#if 0
if(!(erng.lo > erng.hi) && pv->ranges_intersect(pv->ast_scope(e),rng)){
return e; // this term occurs in range, so it's O.K.