@@ -25,27 +25,75 @@ static exprt n_Xes(mp_integer n, exprt op)
25
25
// Returns a set of match conditions (given as LTL formula)
26
26
struct ltl_sequence_matcht
27
27
{
28
- ltl_sequence_matcht (exprt __cond, mp_integer __length)
29
- : cond(std::move(__cond)), length(std::move(__length) )
28
+ // the empty match
29
+ ltl_sequence_matcht ( )
30
30
{
31
- PRECONDITION (length >= 0 );
32
31
}
33
32
34
- exprt cond; // LTL
35
- mp_integer length; // match_end - match_start + 1
33
+ // a match of length 1
34
+ explicit ltl_sequence_matcht (exprt __cond)
35
+ {
36
+ cond_vector.push_back (std::move (__cond));
37
+ }
38
+
39
+ std::vector<exprt> cond_vector;
40
+
41
+ std::size_t length ()
42
+ {
43
+ return cond_vector.size ();
44
+ }
36
45
37
- bool empty () const
46
+ bool empty_match () const
38
47
{
39
- return length == 0 ;
48
+ return cond_vector.empty ();
49
+ }
50
+
51
+ // c0 ∧ X c1 ∧ XX c2 ....
52
+ exprt cond_expr () const
53
+ {
54
+ exprt::operandst conjuncts;
55
+ conjuncts.reserve (cond_vector.size ());
56
+ for (std::size_t i = 0 ; i < cond_vector.size (); i++)
57
+ conjuncts.push_back (n_Xes (i, cond_vector[i]));
58
+ return conjunction (conjuncts);
59
+ }
60
+
61
+ // generate true ##1 ... ##1 true with length n
62
+ static ltl_sequence_matcht true_match (const mp_integer &n)
63
+ {
64
+ ltl_sequence_matcht result;
65
+ for (mp_integer i; i < n; ++i)
66
+ result.cond_vector .push_back (true_exprt{});
67
+ return result;
40
68
}
41
69
};
42
70
71
+ // nonoverlapping concatenation
72
+ ltl_sequence_matcht concat (ltl_sequence_matcht a, const ltl_sequence_matcht &b)
73
+ {
74
+ a.cond_vector .insert (
75
+ a.cond_vector .end (), b.cond_vector .begin (), b.cond_vector .end ());
76
+ return a;
77
+ }
78
+
79
+ // overlapping concatenation
80
+ ltl_sequence_matcht
81
+ overlapping_concat (ltl_sequence_matcht a, ltl_sequence_matcht b)
82
+ {
83
+ PRECONDITION (!a.empty_match ());
84
+ PRECONDITION (!b.empty_match ());
85
+ auto a_last = a.cond_vector .back ();
86
+ a.cond_vector .pop_back ();
87
+ b.cond_vector .front () = conjunction ({a_last, b.cond_vector .front ()});
88
+ return concat (std::move (a), b);
89
+ }
90
+
43
91
std::vector<ltl_sequence_matcht> LTL_sequence_matches (const exprt &sequence)
44
92
{
45
93
if (sequence.id () == ID_sva_boolean)
46
94
{
47
95
// atomic proposition
48
- return {{to_sva_boolean_expr (sequence).op (), 1 }};
96
+ return {ltl_sequence_matcht {to_sva_boolean_expr (sequence).op ()}};
49
97
}
50
98
else if (sequence.id () == ID_sva_sequence_concatenation)
51
99
{
@@ -57,17 +105,16 @@ std::vector<ltl_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
57
105
return {};
58
106
59
107
std::vector<ltl_sequence_matcht> result;
108
+
60
109
// cross product
61
110
for (auto &match_lhs : matches_lhs)
62
111
for (auto &match_rhs : matches_rhs)
63
112
{
64
- // Concatenation is overlapping, hence deduct one from
65
- // the length.
66
- auto delay = match_lhs.length - 1 ;
67
- auto rhs_delayed = n_Xes (delay, match_rhs.cond );
68
- result.emplace_back (
69
- and_exprt{match_lhs.cond , rhs_delayed},
70
- match_lhs.length + match_rhs.length - 1 );
113
+ // Sequence concatenation is overlapping
114
+ auto new_match = overlapping_concat (match_lhs, match_rhs);
115
+ CHECK_RETURN (
116
+ new_match.length () == match_lhs.length () + match_rhs.length () - 1 );
117
+ result.push_back (std::move (new_match));
71
118
}
72
119
return result;
73
120
}
@@ -82,12 +129,12 @@ std::vector<ltl_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
82
129
83
130
if (delay.to ().is_nil ())
84
131
{
132
+ // delay as instructed
133
+ auto delay_sequence = ltl_sequence_matcht::true_match (from_int);
134
+
85
135
for (auto &match : matches)
86
- {
87
- // delay as instructed
88
- match.length += from_int;
89
- match.cond = n_Xes (from_int, match.cond );
90
- }
136
+ match = concat (delay_sequence, match);
137
+
91
138
return matches;
92
139
}
93
140
else if (delay.to ().id () == ID_infinity)
@@ -101,13 +148,12 @@ std::vector<ltl_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
101
148
102
149
for (mp_integer i = from_int; i <= to_int; ++i)
103
150
{
151
+ // delay as instructed
152
+ auto delay_sequence = ltl_sequence_matcht::true_match (i);
153
+
104
154
for (const auto &match : matches)
105
155
{
106
- // delay as instructed
107
- auto new_match = match;
108
- new_match.length += from_int;
109
- new_match.cond = n_Xes (i, match.cond );
110
- new_matches.push_back (std::move (new_match));
156
+ new_matches.push_back (concat (delay_sequence, match));
111
157
}
112
158
}
113
159
@@ -239,15 +285,15 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
239
285
for (auto &match : matches)
240
286
{
241
287
const auto overlapped = expr.id () == ID_sva_overlapped_implication;
242
- if (match.empty () && overlapped)
288
+ if (match.empty_match () && overlapped)
243
289
{
244
290
// ignore the empty match
245
291
}
246
292
else
247
293
{
248
- auto delay = match.length + (overlapped ? 0 : 1 ) - 1 ;
294
+ auto delay = match.length () + (overlapped ? 0 : 1 ) - 1 ;
249
295
auto delayed_property = n_Xes (delay, property_rec.value ());
250
- conjuncts.push_back (implies_exprt{match.cond , delayed_property});
296
+ conjuncts.push_back (implies_exprt{match.cond_expr () , delayed_property});
251
297
}
252
298
}
253
299
@@ -275,15 +321,15 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
275
321
for (auto &match : matches)
276
322
{
277
323
const auto overlapped = expr.id () == ID_sva_overlapped_followed_by;
278
- if (match.empty () && overlapped)
324
+ if (match.empty_match () && overlapped)
279
325
{
280
326
// ignore the empty match
281
327
}
282
328
else
283
329
{
284
- auto delay = match.length + (overlapped ? 0 : 1 ) - 1 ;
330
+ auto delay = match.length () + (overlapped ? 0 : 1 ) - 1 ;
285
331
auto delayed_property = n_Xes (delay, property_rec.value ());
286
- disjuncts.push_back (and_exprt{match.cond , delayed_property});
332
+ disjuncts.push_back (and_exprt{match.cond_expr () , delayed_property});
287
333
}
288
334
}
289
335
@@ -310,8 +356,8 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
310
356
311
357
for (auto &match : matches)
312
358
{
313
- if (!match.empty ())
314
- disjuncts.push_back (match.cond );
359
+ if (!match.empty_match ())
360
+ disjuncts.push_back (match.cond_expr () );
315
361
}
316
362
317
363
return disjunction (disjuncts);
0 commit comments