Skip to content

Construct and_exprt in a non-deprecated way #3786

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.

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
Show file tree
Hide file tree
Changes from all commits
Commits
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
12 changes: 4 additions & 8 deletions src/solvers/flattening/functions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -32,21 +32,17 @@ exprt functionst::arguments_equal(const exprt::operandst &o1,
{
PRECONDITION(o1.size() == o2.size());

if(o1.empty())
return true_exprt();

and_exprt and_expr;
and_exprt::operandst &conjuncts=and_expr.operands();
conjuncts.resize(o1.size());
exprt::operandst conjuncts;
conjuncts.reserve(o1.size());

for(std::size_t i=0; i<o1.size(); i++)
{
exprt lhs=o1[i];
exprt rhs = typecast_exprt::conditional_cast(o2[i], o1[i].type());
conjuncts[i]=equal_exprt(lhs, rhs);
conjuncts.push_back(equal_exprt(lhs, rhs));
}

return std::move(and_expr);
return conjunction(conjuncts);
}

void functionst::add_function_constraints(const function_infot &info)
Expand Down
12 changes: 5 additions & 7 deletions src/solvers/floatbv/float_bv.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -777,13 +777,11 @@ exprt float_bvt::relation(

if(rel==relt::LT)
{
and_exprt and_bv;
and_bv.reserve_operands(4);
and_bv.copy_to_operands(less_than3);
// for the case of two negative numbers
and_bv.copy_to_operands(not_exprt(bitwise_equal));
and_bv.copy_to_operands(not_exprt(both_zero));
and_bv.copy_to_operands(not_exprt(nan));
and_exprt and_bv{{less_than3,
// for the case of two negative numbers
not_exprt(bitwise_equal),
not_exprt(both_zero),
not_exprt(nan)}};

return std::move(and_bv);
}
Expand Down
3 changes: 1 addition & 2 deletions src/util/guard.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -52,8 +52,7 @@ void guardt::add(const exprt &expr)
}
else if(id()!=ID_and)
{
and_exprt a;
a.add_to_operands(*this);
and_exprt a({*this});
*this=a;
}

Expand Down
4 changes: 1 addition & 3 deletions src/util/std_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -55,9 +55,7 @@ exprt conjunction(const exprt::operandst &op)
return op.front();
else
{
and_exprt result;
result.operands()=op;
return std::move(result);
return and_exprt(exprt::operandst(op));
}
Copy link
Member

Choose a reason for hiding this comment

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

The cast appears to be redundant.

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 necessary to as the and_exprt constructor wants an rvalue reference.

}

Expand Down
5 changes: 5 additions & 0 deletions src/util/std_expr.h
Original file line number Diff line number Diff line change
Expand Up @@ -2467,6 +2467,11 @@ class and_exprt:public multi_ary_exprt
: multi_ary_exprt(ID_and, {op0, op1, op2, op3}, bool_typet())
{
}

explicit and_exprt(exprt::operandst &&_operands)
: multi_ary_exprt(ID_and, std::move(_operands), bool_typet())
{
}
};

/// 1) generates a conjunction for two or more operands
Expand Down