Skip to content

Remove unused make_free_bv_expr #6860

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
May 18, 2022
Merged

Remove unused make_free_bv_expr #6860

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 0 additions & 42 deletions src/solvers/flattening/boolbv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -121,8 +121,6 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
return convert_bv_typecast(to_typecast_expr(expr));
else if(expr.id()==ID_symbol)
return convert_symbol(to_symbol_expr(expr));
else if(expr.id()==ID_bv_literals)
return convert_bv_literals(expr);
else if(expr.id()==ID_plus || expr.id()==ID_minus ||
expr.id()=="no-overflow-plus" ||
expr.id()=="no-overflow-minus")
Expand Down Expand Up @@ -275,27 +273,6 @@ bvt boolbvt::convert_array_comprehension(const array_comprehension_exprt &expr)
return bv;
}

bvt boolbvt::convert_bv_literals(const exprt &expr)
{
std::size_t width=boolbv_width(expr.type());

if(width==0)
return conversion_failed(expr);

bvt bv;
bv.resize(width);

const irept::subt &bv_sub=expr.find(ID_bv).get_sub();

if(bv_sub.size()!=width)
throw "bv_literals with wrong size";

for(std::size_t i=0; i<width; i++)
bv[i].set(unsafe_string2unsigned(id2string(bv_sub[i].id())));

return bv;
}

bvt boolbvt::convert_symbol(const exprt &expr)
{
const typet &type=expr.type();
Expand Down Expand Up @@ -530,25 +507,6 @@ void boolbvt::set_to(const exprt &expr, bool value)
SUB::set_to(expr, value);
}

exprt boolbvt::make_bv_expr(const typet &type, const bvt &bv)
{
exprt dest(ID_bv_literals, type);
irept::subt &bv_sub=dest.add(ID_bv).get_sub();
bv_sub.resize(bv.size());

for(std::size_t i=0; i<bv.size(); i++)
bv_sub[i].id(std::to_string(bv[i].get()));
return dest;
}

exprt boolbvt::make_free_bv_expr(const typet &type)
{
const std::size_t width = boolbv_width(type);
PRECONDITION(width != 0);
bvt bv = prop.new_variables(width);
return make_bv_expr(type, bv);
}

bool boolbvt::is_unbounded_array(const typet &type) const
{
if(type.id()!=ID_array)
Expand Down
4 changes: 0 additions & 4 deletions src/solvers/flattening/boolbv.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -187,7 +187,6 @@ class boolbvt:public arrayst
virtual bvt convert_abs(const abs_exprt &expr);
virtual bvt convert_concatenation(const concatenation_exprt &expr);
virtual bvt convert_replication(const replication_exprt &expr);
virtual bvt convert_bv_literals(const exprt &expr);
virtual bvt convert_constant(const constant_exprt &expr);
virtual bvt convert_extractbits(const extractbits_exprt &expr);
virtual bvt convert_symbol(const exprt &expr);
Expand All @@ -199,9 +198,6 @@ class boolbvt:public arrayst
virtual bvt convert_bitreverse(const bitreverse_exprt &expr);
virtual bvt convert_saturating_add_sub(const binary_exprt &expr);

virtual exprt make_bv_expr(const typet &type, const bvt &bv);
virtual exprt make_free_bv_expr(const typet &type);

void convert_with(
const typet &type,
const exprt &op1,
Expand Down
1 change: 0 additions & 1 deletion src/util/irep_ids.def
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -300,7 +300,6 @@ IREP_ID_ONE(KnR)
IREP_ID_TWO(C_KnR, #KnR)
IREP_ID_ONE(constraint_select_one)
IREP_ID_ONE(cond)
IREP_ID_ONE(bv_literals)
IREP_ID_ONE(isfinite)
IREP_ID_ONE(isinf)
IREP_ID_ONE(isnormal)
Expand Down