Skip to content

Commit 061876e

Browse files
authored
Merge pull request #3793 from tautschnig/deprecation-or_exprt
Construct or_exprt in a non-deprecated way
2 parents 73ebbb4 + 115d145 commit 061876e

File tree

5 files changed

+12
-13
lines changed

5 files changed

+12
-13
lines changed

src/goto-symex/memory_model.cpp

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

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

src/solvers/floatbv/float_bv.cpp

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -789,11 +789,7 @@ 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{{less_than3, both_zero, bitwise_equal}};
797793

798794
return and_exprt(or_bv, not_exprt(nan));
799795
}

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
@@ -2583,6 +2583,11 @@ class or_exprt:public multi_ary_exprt
25832583
: multi_ary_exprt(ID_or, {op0, op1, op2, op3}, bool_typet())
25842584
{
25852585
}
2586+
2587+
explicit or_exprt(exprt::operandst &&_operands)
2588+
: multi_ary_exprt(ID_or, std::move(_operands), bool_typet())
2589+
{
2590+
}
25862591
};
25872592

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

0 commit comments

Comments
 (0)