Skip to content

Commit 352014e

Browse files
committed
Construct or_exprt in a non-deprecated way
The default constructor is deprecated. To facilitate construction with an arbitrary number of operands a new constructor taking a initializer list is added.
1 parent 7106860 commit 352014e

File tree

5 files changed

+15
-13
lines changed

5 files changed

+15
-13
lines changed

src/goto-symex/memory_model.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -119,8 +119,7 @@ void memory_model_baset::read_from(symex_target_equationt &equation)
119119
rf_some=rf_some_operands.front();
120120
else
121121
{
122-
rf_some=or_exprt();
123-
rf_some.operands().swap(rf_some_operands);
122+
rf_some = or_exprt(std::move(rf_some_operands));
124123
}
125124

126125
// Add the read's guard, each of the writes' guards is implied

src/solvers/floatbv/float_bv.cpp

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -789,11 +789,10 @@ exprt float_bvt::relation(
789789
}
790790
else if(rel==relt::LE)
791791
{
792-
or_exprt or_bv;
793-
or_bv.reserve_operands(3);
794-
or_bv.copy_to_operands(less_than3);
795-
or_bv.copy_to_operands(both_zero);
796-
or_bv.copy_to_operands(bitwise_equal);
792+
or_exprt or_bv{{
793+
less_than3,
794+
both_zero,
795+
bitwise_equal}};
797796

798797
return and_exprt(or_bv, not_exprt(nan));
799798
}

src/solvers/prop/minimize.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -81,11 +81,12 @@ literalt prop_minimizet::constraint()
8181
return or_clause.front();
8282
else
8383
{
84-
or_exprt or_expr;
84+
exprt::operandst disjuncts;
85+
disjuncts.reserve(or_clause.size());
8586
forall_literals(it, or_clause)
86-
or_expr.copy_to_operands(literal_exprt(*it));
87+
disjuncts.push_back(literal_exprt(*it));
8788

88-
return prop_conv.convert(or_expr);
89+
return prop_conv.convert(disjunction(disjuncts));
8990
}
9091
}
9192

src/util/std_expr.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -31,9 +31,7 @@ exprt disjunction(const exprt::operandst &op)
3131
return op.front();
3232
else
3333
{
34-
or_exprt result;
35-
result.operands()=op;
36-
return std::move(result);
34+
return or_exprt(exprt::operandst(op));
3735
}
3836
}
3937

src/util/std_expr.h

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2588,6 +2588,11 @@ class or_exprt:public multi_ary_exprt
25882588
: multi_ary_exprt(ID_or, {op0, op1, op2, op3}, bool_typet())
25892589
{
25902590
}
2591+
2592+
or_exprt(exprt::operandst &&_operands)
2593+
: multi_ary_exprt(ID_or, std::move(_operands), bool_typet())
2594+
{
2595+
}
25912596
};
25922597

25932598
/// 1) generates a disjunction for two or more operands

0 commit comments

Comments
 (0)