Skip to content

bv_utilst::zeros: code cleanup, use more widely #7122

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
kroening merged 3 commits into from
Sep 12, 2022
Merged

bv_utilst::zeros: code cleanup, use more widely #7122

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
440ea26
Use bv_utilst::zeros
tautschnig Sep 12, 2022
320ab53
Rename variable for clarity
tautschnig Sep 12, 2022
047c065
bv_utilst::zeros: use the most appropriate constructor
tautschnig Sep 12, 2022
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
3 changes: 1 addition & 2 deletions src/solvers/flattening/boolbv_div.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,8 +37,7 @@ bvt boolbvt::convert_div(const div_exprt &expr)
std::size_t fraction_bits=
to_fixedbv_type(expr.type()).get_fraction_bits();

bvt zeros;
zeros.resize(fraction_bits, const_literal(false));
bvt zeros = bv_utils.zeros(fraction_bits);

// add fraction_bits least-significant bits
op0.insert(op0.begin(), zeros.begin(), zeros.end());
Expand Down
20 changes: 6 additions & 14 deletions src/solvers/flattening/bv_utils.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -615,10 +615,10 @@ literalt bv_utilst::overflow_negate(const bvt &bv)
// a overflow on unary- can only happen with the smallest
// representable number 100....0

bvt zeros(bv);
zeros.erase(--zeros.end());
bvt should_be_zeros(bv);
should_be_zeros.pop_back();

return prop.land(bv[bv.size()-1], !prop.lor(zeros));
return prop.land(bv[bv.size() - 1], !prop.lor(should_be_zeros));
}

void bv_utilst::incrementer(
Expand Down Expand Up @@ -715,13 +715,9 @@ bvt bv_utilst::unsigned_multiplier(const bvt &_op0, const bvt &_op1)
for(std::size_t sum=0; sum<op0.size(); sum++)
if(op0[sum]!=const_literal(false))
{
bvt tmpop;

bvt tmpop = zeros(sum);
tmpop.reserve(op0.size());

for(std::size_t idx=0; idx<sum; idx++)
tmpop.push_back(const_literal(false));

for(std::size_t idx=sum; idx<op0.size(); idx++)
tmpop.push_back(prop.land(op1[idx-sum], op0[sum]));

Expand All @@ -746,13 +742,9 @@ bvt bv_utilst::unsigned_multiplier(const bvt &_op0, const bvt &_op1)
for(std::size_t bit=0; bit<op0.size(); bit++)
if(op0[bit]!=const_literal(false))
{
bvt pp;

pp.reserve(op0.size());

// zeros according to weight
for(std::size_t idx=0; idx<bit; idx++)
pp.push_back(const_literal(false));
bvt pp = zeros(bit);
pp.reserve(op0.size());

for(std::size_t idx=bit; idx<op0.size(); idx++)
pp.push_back(prop.land(op1[idx-bit], op0[bit]));
Expand Down
4 changes: 1 addition & 3 deletions src/solvers/flattening/bv_utils.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -191,9 +191,7 @@ class bv_utilst

static bvt zeros(std::size_t new_size)
{
bvt result;
result.resize(new_size, const_literal(false));
return result;
return bvt(new_size, const_literal(false));
}

void set_equal(const bvt &a, const bvt &b);
Expand Down