Skip to content

Commit fdd3bcb

Browse files
committed
Avoid sva_sequence_matcht default constructor
This replaces uses of the sva_sequence_matcht default constructor by uses of the constructor that takes an expression vector as argument.
1 parent 8f220ab commit fdd3bcb

File tree

1 file changed

+11
-12
lines changed

1 file changed

+11
-12
lines changed

src/temporal-logic/sva_sequence_match.cpp

Lines changed: 11 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -15,10 +15,8 @@ Author: Daniel Kroening, [email protected]
1515

1616
sva_sequence_matcht sva_sequence_matcht::true_match(const mp_integer &n)
1717
{
18-
sva_sequence_matcht result;
19-
for(mp_integer i; i < n; ++i)
20-
result.cond_vector.push_back(true_exprt{});
21-
return result;
18+
auto n_size_t = numeric_cast_v<std::size_t>(n);
19+
return sva_sequence_matcht{std::vector<exprt>(n_size_t, true_exprt{})};
2220
}
2321

2422
// nonoverlapping concatenation
@@ -32,11 +30,12 @@ sva_sequence_matcht concat(sva_sequence_matcht a, const sva_sequence_matcht &b)
3230
// nonoverlapping concatenation
3331
sva_sequence_matcht repeat(sva_sequence_matcht m, const mp_integer &n)
3432
{
35-
sva_sequence_matcht result;
33+
std::vector<exprt> cond_vector;
34+
cond_vector.reserve(numeric_cast_v<std::size_t>(n * m.length()));
3635
for(mp_integer i = 0; i < n; ++i)
37-
result.cond_vector.insert(
38-
result.cond_vector.end(), m.cond_vector.begin(), m.cond_vector.end());
39-
return result;
36+
cond_vector.insert(
37+
cond_vector.end(), m.cond_vector.begin(), m.cond_vector.end());
38+
return sva_sequence_matcht{std::move(cond_vector)};
4039
}
4140

4241
// overlapping concatenation
@@ -171,9 +170,9 @@ std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
171170
for(auto &match_lhs : matches_lhs)
172171
for(auto &match_rhs : matches_rhs)
173172
{
174-
sva_sequence_matcht new_match;
173+
std::vector<exprt> cond_vector;
175174
auto new_length = std::max(match_lhs.length(), match_rhs.length());
176-
new_match.cond_vector.resize(new_length);
175+
cond_vector.resize(new_length);
177176
for(std::size_t i = 0; i < new_length; i++)
178177
{
179178
exprt::operandst conjuncts;
@@ -183,10 +182,10 @@ std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
183182
if(i < match_rhs.cond_vector.size())
184183
conjuncts.push_back(match_rhs.cond_vector[i]);
185184

186-
new_match.cond_vector[i] = conjunction(conjuncts);
185+
cond_vector[i] = conjunction(conjuncts);
187186
}
188187

189-
result.push_back(std::move(new_match));
188+
result.emplace_back(std::move(cond_vector));
190189
}
191190

192191
return result;

0 commit comments

Comments
 (0)