Skip to content

Construct equal_exprt in a non-deprecated way #3776

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
Jan 14, 2019
Merged

Construct equal_exprt in a non-deprecated way #3776

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
9 changes: 3 additions & 6 deletions src/analyses/invariant_set.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -752,9 +752,8 @@ void invariant_sett::nnf(exprt &expr, bool negate)
typecast_expr.op().type().id() == ID_unsignedbv ||
typecast_expr.op().type().id() == ID_signedbv)
{
equal_exprt tmp;
tmp.lhs() = typecast_expr.op();
tmp.rhs() = from_integer(0, typecast_expr.op().type());
equal_exprt tmp(
typecast_expr.op(), from_integer(0, typecast_expr.op().type()));
nnf(tmp, !negate);
expr.swap(tmp);
}
Expand Down Expand Up @@ -1053,9 +1052,7 @@ void invariant_sett::assignment(
const exprt &lhs,
const exprt &rhs)
{
equal_exprt equality;
equality.lhs()=lhs;
equality.rhs()=rhs;
equal_exprt equality(lhs, rhs);

// first evaluate RHS
simplify(equality.rhs());
Expand Down
4 changes: 2 additions & 2 deletions src/ansi-c/c_typecheck_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2540,8 +2540,8 @@ exprt c_typecheck_baset::do_special_functions(
throw 0;
}

equal_exprt equality_expr;
equality_expr.operands()=expr.arguments();
equal_exprt equality_expr(
expr.arguments().front(), expr.arguments().back());
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are we sure this has two elements?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's check 7 lines earlier so this should be ok.

equality_expr.add_source_location()=source_location;

if(!base_type_eq(equality_expr.lhs().type(),
Expand Down
4 changes: 1 addition & 3 deletions src/goto-programs/goto_convert.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1156,9 +1156,7 @@ exprt goto_convertt::case_guard(

forall_expr(it, case_op)
{
equal_exprt eq_expr;
eq_expr.lhs() = value;
eq_expr.rhs() = *it;
equal_exprt eq_expr(value, *it);
dest.move_to_operands(eq_expr);
}
INVARIANT(
Expand Down
18 changes: 5 additions & 13 deletions src/solvers/flattening/boolbv_byte_extract.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -143,9 +143,6 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)

// add implications

equal_exprt equality;
equality.lhs() = expr.offset(); // index operand

// type of index operand
const typet &constant_type = expr.offset().type();

Expand All @@ -154,8 +151,6 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)

for(std::size_t i=0; i<bytes; i++)
{
equality.rhs()=from_integer(i, constant_type);

std::size_t offset=i*byte_width;

for(std::size_t j=0; j<width; j++)
Expand All @@ -164,23 +159,20 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
else
equal_bv[j]=const_literal(true);

prop.l_set_to_true(
prop.limplies(convert(equality), prop.land(equal_bv)));
prop.l_set_to_true(prop.limplies(
convert(equal_exprt(expr.offset(), from_integer(i, constant_type))),
prop.land(equal_bv)));
}
}
else
{
equal_exprt equality;
equality.lhs() = expr.offset(); // index operand

// type of index operand
const typet &constant_type = expr.offset().type();

for(std::size_t i=0; i<bytes; i++)
{
equality.rhs()=from_integer(i, constant_type);

literalt e=convert(equality);
literalt e =
convert(equal_exprt(expr.offset(), from_integer(i, constant_type)));

std::size_t offset=i*byte_width;

Expand Down
5 changes: 2 additions & 3 deletions src/solvers/flattening/boolbv_byte_update.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,9 +85,8 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
for(std::size_t offset=0; offset<bv.size(); offset+=byte_width)
{
// index condition
equal_exprt equality;
equality.lhs()=offset_expr;
equality.rhs()=from_integer(offset/byte_width, offset_expr.type());
equal_exprt equality(
offset_expr, from_integer(offset / byte_width, offset_expr.type()));
literalt equal=convert(equality);

bv_endianness_mapt map_op(op.type(), little_endian, ns, boolbv_width);
Expand Down
7 changes: 2 additions & 5 deletions src/solvers/flattening/boolbv_extractbit.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,11 +51,8 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
std::max(address_bits(src_bv_width), index_bv_width);
unsignedbv_typet index_type(index_width);

equal_exprt equality;
equality.lhs() = expr.index();

if(index_type!=equality.lhs().type())
equality.lhs().make_typecast(index_type);
equal_exprt equality(
typecast_exprt::conditional_cast(expr.index(), index_type), exprt());

if(prop.has_set_to())
{
Expand Down
35 changes: 8 additions & 27 deletions src/solvers/flattening/boolbv_index.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -144,12 +144,6 @@ bvt boolbvt::convert_index(const index_exprt &expr)

// add implications

equal_exprt index_equality;
index_equality.lhs()=index; // index operand

equal_exprt value_equality;
value_equality.lhs()=result;

#ifdef COMPACT_EQUAL_CONST
bv_utils.equal_const_register(convert_bv(index)); // Definitely
bv_utils.equal_const_register(convert_bv(result)); // Maybe
Expand All @@ -159,19 +153,15 @@ bvt boolbvt::convert_index(const index_exprt &expr)

for(mp_integer i=0; i<array_size; i=i+1)
{
index_equality.rhs()=from_integer(i, index_equality.lhs().type());
CHECK_RETURN(index_equality.rhs().is_not_nil());

INVARIANT(
it != array.operands().end(),
"this loop iterates over the array, so `it` shouldn't be increased "
"past the array's end");

value_equality.rhs()=*it++;

// Cache comparisons and equalities
prop.l_set_to_true(convert(implies_exprt(index_equality,
value_equality)));
prop.l_set_to_true(convert(implies_exprt(
equal_exprt(index, from_integer(i, index.type())),
equal_exprt(result, *it++))));
}

return bv;
Expand Down Expand Up @@ -203,9 +193,6 @@ bvt boolbvt::convert_index(const index_exprt &expr)

// add implications

equal_exprt index_equality;
index_equality.lhs()=index; // index operand

#ifdef COMPACT_EQUAL_CONST
bv_utils.equal_const_register(convert_bv(index)); // Definitely
#endif
Expand All @@ -215,26 +202,21 @@ bvt boolbvt::convert_index(const index_exprt &expr)

for(mp_integer i=0; i<array_size; i=i+1)
{
index_equality.rhs()=from_integer(i, index_equality.lhs().type());
CHECK_RETURN(index_equality.rhs().is_not_nil());

mp_integer offset=i*width;

for(std::size_t j=0; j<width; j++)
equal_bv[j] = prop.lequal(
bv[j], array_bv[numeric_cast_v<std::size_t>(offset + j)]);

prop.l_set_to_true(
prop.limplies(convert(index_equality), prop.land(equal_bv)));
prop.l_set_to_true(prop.limplies(
convert(equal_exprt(index, from_integer(i, index.type()))),
prop.land(equal_bv)));
}
}
else
{
bv.resize(width);

equal_exprt equality;
equality.lhs()=index; // index operand

#ifdef COMPACT_EQUAL_CONST
bv_utils.equal_const_register(convert_bv(index)); // Definitely
#endif
Expand All @@ -247,9 +229,8 @@ bvt boolbvt::convert_index(const index_exprt &expr)

for(mp_integer i=0; i<array_size; i=i+1)
{
equality.op1()=from_integer(i, constant_type);

literalt e=convert(equality);
literalt e =
convert(equal_exprt(index, from_integer(i, constant_type)));

mp_integer offset=i*width;

Expand Down