Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_minmax_test / minmax_test.smt2 @ 6c3ea955

History | View | Annotate | Download (15 KB)

1
; minmax_test
2
(declare-var minmax_test.In1_1_1 Real)
3
(declare-var minmax_test.In2_1_1 Real)
4
(declare-var minmax_test.In3_1_1 Real)
5
(declare-var minmax_test.In3_1_2 Real)
6
(declare-var minmax_test.In4_1_1 Real)
7
(declare-var minmax_test.In4_1_2 Real)
8
(declare-var minmax_test.In5_1_1 Real)
9
(declare-var minmax_test.In5_1_2 Real)
10
(declare-var minmax_test.In5_1_3 Real)
11
(declare-var minmax_test.In5_1_4 Real)
12
(declare-var minmax_test.In6_1_1 Real)
13
(declare-var minmax_test.In6_1_2 Real)
14
(declare-var minmax_test.In6_1_3 Real)
15
(declare-var minmax_test.In6_1_4 Real)
16
(declare-var minmax_test.In7_1_1 Real)
17
(declare-var minmax_test.In7_1_2 Real)
18
(declare-var minmax_test.In7_1_3 Real)
19
(declare-var minmax_test.In8_1_1 Real)
20
(declare-var minmax_test.In8_1_2 Real)
21
(declare-var minmax_test.In8_1_3 Real)
22
(declare-var minmax_test.In8_1_4 Real)
23
(declare-var minmax_test.In8_1_5 Real)
24
(declare-var minmax_test.In8_1_6 Real)
25
(declare-var minmax_test.In8_1_7 Real)
26
(declare-var minmax_test.Out1_1_1 Real)
27
(declare-var minmax_test.Out2_2_1 Real)
28
(declare-var minmax_test.Out3_3_1 Real)
29
(declare-var minmax_test.Out3_3_2 Real)
30
(declare-var minmax_test.Out4_4_1 Real)
31
(declare-var minmax_test.Out4_4_2 Real)
32
(declare-var minmax_test.Out5_5_1 Real)
33
(declare-var minmax_test.Out5_5_2 Real)
34
(declare-var minmax_test.Out5_5_3 Real)
35
(declare-var minmax_test.Out5_5_4 Real)
36
(declare-var minmax_test.Out6_6_1 Real)
37
(declare-var minmax_test.Out6_6_2 Real)
38
(declare-var minmax_test.Out6_6_3 Real)
39
(declare-var minmax_test.Out6_6_4 Real)
40
(declare-var minmax_test.Out7_7_1 Real)
41
(declare-var minmax_test.Out8_8_1 Real)
42
(declare-var minmax_test.ni_0._arrow._first_c Bool)
43
(declare-var minmax_test.ni_0._arrow._first_m Bool)
44
(declare-var minmax_test.ni_0._arrow._first_x Bool)
45
(declare-var minmax_test.__minmax_test_1 Bool)
46
(declare-var minmax_test.__minmax_test_10 Bool)
47
(declare-var minmax_test.__minmax_test_11 Bool)
48
(declare-var minmax_test.__minmax_test_12 Bool)
49
(declare-var minmax_test.__minmax_test_13 Bool)
50
(declare-var minmax_test.__minmax_test_14 Bool)
51
(declare-var minmax_test.__minmax_test_15 Bool)
52
(declare-var minmax_test.__minmax_test_16 Bool)
53
(declare-var minmax_test.__minmax_test_17 Bool)
54
(declare-var minmax_test.__minmax_test_18 Bool)
55
(declare-var minmax_test.__minmax_test_19 Bool)
56
(declare-var minmax_test.__minmax_test_2 Bool)
57
(declare-var minmax_test.__minmax_test_20 Bool)
58
(declare-var minmax_test.__minmax_test_21 Bool)
59
(declare-var minmax_test.__minmax_test_22 Bool)
60
(declare-var minmax_test.__minmax_test_23 Bool)
61
(declare-var minmax_test.__minmax_test_3 Bool)
62
(declare-var minmax_test.__minmax_test_4 Bool)
63
(declare-var minmax_test.__minmax_test_5 Bool)
64
(declare-var minmax_test.__minmax_test_6 Bool)
65
(declare-var minmax_test.__minmax_test_7 Bool)
66
(declare-var minmax_test.__minmax_test_8 Bool)
67
(declare-var minmax_test.__minmax_test_9 Bool)
68
(declare-var minmax_test.i_virtual_local Real)
69
(declare-var minmax_test.max_block1_1_1 Real)
70
(declare-var minmax_test.max_block1_1_2 Real)
71
(declare-var minmax_test.max_block2_1_1 Real)
72
(declare-var minmax_test.max_block2_1_2 Real)
73
(declare-var minmax_test.max_block2_1_3 Real)
74
(declare-var minmax_test.max_block2_1_4 Real)
75
(declare-var minmax_test.max_block_1_1 Real)
76
(declare-var minmax_test.min_block1_1_1 Real)
77
(declare-var minmax_test.min_block1_1_2 Real)
78
(declare-var minmax_test.min_block2_1_1 Real)
79
(declare-var minmax_test.min_block2_1_2 Real)
80
(declare-var minmax_test.min_block2_1_3 Real)
81
(declare-var minmax_test.min_block2_1_4 Real)
82
(declare-var minmax_test.min_block3_1_1 Real)
83
(declare-var minmax_test.min_block3_tmp_1 Real)
84
(declare-var minmax_test.min_block4_1_1 Real)
85
(declare-var minmax_test.min_block4_tmp_1 Real)
86
(declare-var minmax_test.min_block4_tmp_2 Real)
87
(declare-var minmax_test.min_block4_tmp_3 Real)
88
(declare-var minmax_test.min_block4_tmp_4 Real)
89
(declare-var minmax_test.min_block4_tmp_5 Real)
90
(declare-var minmax_test.min_block_1_1 Real)
91
(declare-rel minmax_test_reset (Bool Bool))
92
(declare-rel minmax_test_step (Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Bool Bool))
93

    
94
(rule (=> 
95
  (and 
96
       
97
       (= minmax_test.ni_0._arrow._first_m true)
98
  )
99
  (minmax_test_reset minmax_test.ni_0._arrow._first_c
100
                     minmax_test.ni_0._arrow._first_m)
101
))
102

    
103
(rule (=> 
104
  (and (= minmax_test.__minmax_test_16 (<= minmax_test.In1_1_1 minmax_test.In2_1_1))
105
       (and (or (not (= minmax_test.__minmax_test_16 true))
106
               (= minmax_test.min_block_1_1 minmax_test.In1_1_1))
107
            (or (not (= minmax_test.__minmax_test_16 false))
108
               (= minmax_test.min_block_1_1 minmax_test.In2_1_1))
109
       )
110
       (= minmax_test.__minmax_test_7 (>= minmax_test.In8_1_1 minmax_test.In8_1_2))
111
       (and (or (not (= minmax_test.__minmax_test_7 true))
112
               (= minmax_test.min_block4_tmp_1 minmax_test.In8_1_1))
113
            (or (not (= minmax_test.__minmax_test_7 false))
114
               (= minmax_test.min_block4_tmp_1 minmax_test.In8_1_2))
115
       )
116
       (= minmax_test.__minmax_test_6 (>= minmax_test.min_block4_tmp_1 minmax_test.In8_1_3))
117
       (and (or (not (= minmax_test.__minmax_test_6 true))
118
               (= minmax_test.min_block4_tmp_2 minmax_test.min_block4_tmp_1))
119
            (or (not (= minmax_test.__minmax_test_6 false))
120
               (= minmax_test.min_block4_tmp_2 minmax_test.In8_1_3))
121
       )
122
       (= minmax_test.__minmax_test_5 (>= minmax_test.min_block4_tmp_2 minmax_test.In8_1_4))
123
       (and (or (not (= minmax_test.__minmax_test_5 true))
124
               (= minmax_test.min_block4_tmp_3 minmax_test.min_block4_tmp_2))
125
            (or (not (= minmax_test.__minmax_test_5 false))
126
               (= minmax_test.min_block4_tmp_3 minmax_test.In8_1_4))
127
       )
128
       (= minmax_test.__minmax_test_4 (>= minmax_test.min_block4_tmp_3 minmax_test.In8_1_5))
129
       (and (or (not (= minmax_test.__minmax_test_4 true))
130
               (= minmax_test.min_block4_tmp_4 minmax_test.min_block4_tmp_3))
131
            (or (not (= minmax_test.__minmax_test_4 false))
132
               (= minmax_test.min_block4_tmp_4 minmax_test.In8_1_5))
133
       )
134
       (= minmax_test.__minmax_test_3 (>= minmax_test.min_block4_tmp_4 minmax_test.In8_1_6))
135
       (and (or (not (= minmax_test.__minmax_test_3 true))
136
               (= minmax_test.min_block4_tmp_5 minmax_test.min_block4_tmp_4))
137
            (or (not (= minmax_test.__minmax_test_3 false))
138
               (= minmax_test.min_block4_tmp_5 minmax_test.In8_1_6))
139
       )
140
       (= minmax_test.__minmax_test_2 (>= minmax_test.min_block4_tmp_5 minmax_test.In8_1_7))
141
       (and (or (not (= minmax_test.__minmax_test_2 true))
142
               (= minmax_test.min_block4_1_1 minmax_test.min_block4_tmp_5))
143
            (or (not (= minmax_test.__minmax_test_2 false))
144
               (= minmax_test.min_block4_1_1 minmax_test.In8_1_7))
145
       )
146
       (= minmax_test.__minmax_test_9 (<= minmax_test.In7_1_1 minmax_test.In7_1_2))
147
       (and (or (not (= minmax_test.__minmax_test_9 true))
148
               (= minmax_test.min_block3_tmp_1 minmax_test.In7_1_1))
149
            (or (not (= minmax_test.__minmax_test_9 false))
150
               (= minmax_test.min_block3_tmp_1 minmax_test.In7_1_2))
151
       )
152
       (= minmax_test.__minmax_test_8 (<= minmax_test.min_block3_tmp_1 minmax_test.In7_1_3))
153
       (and (or (not (= minmax_test.__minmax_test_8 true))
154
               (= minmax_test.min_block3_1_1 minmax_test.min_block3_tmp_1))
155
            (or (not (= minmax_test.__minmax_test_8 false))
156
               (= minmax_test.min_block3_1_1 minmax_test.In7_1_3))
157
       )
158
       (= minmax_test.__minmax_test_10 (<= minmax_test.In5_1_4 minmax_test.In6_1_4))
159
       (and (or (not (= minmax_test.__minmax_test_10 true))
160
               (= minmax_test.min_block2_1_4 minmax_test.In5_1_4))
161
            (or (not (= minmax_test.__minmax_test_10 false))
162
               (= minmax_test.min_block2_1_4 minmax_test.In6_1_4))
163
       )
164
       (= minmax_test.__minmax_test_11 (<= minmax_test.In5_1_3 minmax_test.In6_1_3))
165
       (and (or (not (= minmax_test.__minmax_test_11 true))
166
               (= minmax_test.min_block2_1_3 minmax_test.In5_1_3))
167
            (or (not (= minmax_test.__minmax_test_11 false))
168
               (= minmax_test.min_block2_1_3 minmax_test.In6_1_3))
169
       )
170
       (= minmax_test.__minmax_test_12 (<= minmax_test.In5_1_2 minmax_test.In6_1_2))
171
       (and (or (not (= minmax_test.__minmax_test_12 true))
172
               (= minmax_test.min_block2_1_2 minmax_test.In5_1_2))
173
            (or (not (= minmax_test.__minmax_test_12 false))
174
               (= minmax_test.min_block2_1_2 minmax_test.In6_1_2))
175
       )
176
       (= minmax_test.__minmax_test_13 (<= minmax_test.In5_1_1 minmax_test.In6_1_1))
177
       (and (or (not (= minmax_test.__minmax_test_13 true))
178
               (= minmax_test.min_block2_1_1 minmax_test.In5_1_1))
179
            (or (not (= minmax_test.__minmax_test_13 false))
180
               (= minmax_test.min_block2_1_1 minmax_test.In6_1_1))
181
       )
182
       (= minmax_test.__minmax_test_14 (<= minmax_test.In3_1_2 minmax_test.In4_1_2))
183
       (and (or (not (= minmax_test.__minmax_test_14 true))
184
               (= minmax_test.min_block1_1_2 minmax_test.In3_1_2))
185
            (or (not (= minmax_test.__minmax_test_14 false))
186
               (= minmax_test.min_block1_1_2 minmax_test.In4_1_2))
187
       )
188
       (= minmax_test.__minmax_test_15 (<= minmax_test.In3_1_1 minmax_test.In4_1_1))
189
       (and (or (not (= minmax_test.__minmax_test_15 true))
190
               (= minmax_test.min_block1_1_1 minmax_test.In3_1_1))
191
            (or (not (= minmax_test.__minmax_test_15 false))
192
               (= minmax_test.min_block1_1_1 minmax_test.In4_1_1))
193
       )
194
       (= minmax_test.__minmax_test_23 (>= minmax_test.In1_1_1 minmax_test.In2_1_1))
195
       (and (or (not (= minmax_test.__minmax_test_23 true))
196
               (= minmax_test.max_block_1_1 minmax_test.In1_1_1))
197
            (or (not (= minmax_test.__minmax_test_23 false))
198
               (= minmax_test.max_block_1_1 minmax_test.In2_1_1))
199
       )
200
       (= minmax_test.__minmax_test_17 (>= minmax_test.In5_1_4 minmax_test.In6_1_4))
201
       (and (or (not (= minmax_test.__minmax_test_17 true))
202
               (= minmax_test.max_block2_1_4 minmax_test.In5_1_4))
203
            (or (not (= minmax_test.__minmax_test_17 false))
204
               (= minmax_test.max_block2_1_4 minmax_test.In6_1_4))
205
       )
206
       (= minmax_test.__minmax_test_18 (>= minmax_test.In5_1_3 minmax_test.In6_1_3))
207
       (and (or (not (= minmax_test.__minmax_test_18 true))
208
               (= minmax_test.max_block2_1_3 minmax_test.In5_1_3))
209
            (or (not (= minmax_test.__minmax_test_18 false))
210
               (= minmax_test.max_block2_1_3 minmax_test.In6_1_3))
211
       )
212
       (= minmax_test.__minmax_test_19 (>= minmax_test.In5_1_2 minmax_test.In6_1_2))
213
       (and (or (not (= minmax_test.__minmax_test_19 true))
214
               (= minmax_test.max_block2_1_2 minmax_test.In5_1_2))
215
            (or (not (= minmax_test.__minmax_test_19 false))
216
               (= minmax_test.max_block2_1_2 minmax_test.In6_1_2))
217
       )
218
       (= minmax_test.__minmax_test_20 (>= minmax_test.In5_1_1 minmax_test.In6_1_1))
219
       (and (or (not (= minmax_test.__minmax_test_20 true))
220
               (= minmax_test.max_block2_1_1 minmax_test.In5_1_1))
221
            (or (not (= minmax_test.__minmax_test_20 false))
222
               (= minmax_test.max_block2_1_1 minmax_test.In6_1_1))
223
       )
224
       (= minmax_test.__minmax_test_21 (>= minmax_test.In3_1_2 minmax_test.In4_1_2))
225
       (and (or (not (= minmax_test.__minmax_test_21 true))
226
               (= minmax_test.max_block1_1_2 minmax_test.In3_1_2))
227
            (or (not (= minmax_test.__minmax_test_21 false))
228
               (= minmax_test.max_block1_1_2 minmax_test.In4_1_2))
229
       )
230
       (= minmax_test.__minmax_test_22 (>= minmax_test.In3_1_1 minmax_test.In4_1_1))
231
       (and (or (not (= minmax_test.__minmax_test_22 true))
232
               (= minmax_test.max_block1_1_1 minmax_test.In3_1_1))
233
            (or (not (= minmax_test.__minmax_test_22 false))
234
               (= minmax_test.max_block1_1_1 minmax_test.In4_1_1))
235
       )
236
       (= minmax_test.ni_0._arrow._first_m minmax_test.ni_0._arrow._first_c)
237
       (and (= minmax_test.__minmax_test_1 (ite minmax_test.ni_0._arrow._first_m true false))
238
            (= minmax_test.ni_0._arrow._first_x false))
239
       (and (or (not (= minmax_test.__minmax_test_1 true))
240
               (= minmax_test.i_virtual_local 0.0))
241
            (or (not (= minmax_test.__minmax_test_1 false))
242
               (= minmax_test.i_virtual_local 1.0))
243
       )
244
       (= minmax_test.Out8_8_1 minmax_test.min_block4_1_1)
245
       (= minmax_test.Out7_7_1 minmax_test.min_block3_1_1)
246
       (= minmax_test.Out6_6_4 minmax_test.max_block2_1_4)
247
       (= minmax_test.Out6_6_3 minmax_test.max_block2_1_3)
248
       (= minmax_test.Out6_6_2 minmax_test.max_block2_1_2)
249
       (= minmax_test.Out6_6_1 minmax_test.max_block2_1_1)
250
       (= minmax_test.Out5_5_4 minmax_test.min_block2_1_4)
251
       (= minmax_test.Out5_5_3 minmax_test.min_block2_1_3)
252
       (= minmax_test.Out5_5_2 minmax_test.min_block2_1_2)
253
       (= minmax_test.Out5_5_1 minmax_test.min_block2_1_1)
254
       (= minmax_test.Out4_4_2 minmax_test.max_block1_1_2)
255
       (= minmax_test.Out4_4_1 minmax_test.max_block1_1_1)
256
       (= minmax_test.Out3_3_2 minmax_test.min_block1_1_2)
257
       (= minmax_test.Out3_3_1 minmax_test.min_block1_1_1)
258
       (= minmax_test.Out2_2_1 minmax_test.max_block_1_1)
259
       (= minmax_test.Out1_1_1 minmax_test.min_block_1_1)
260
       )
261
  (minmax_test_step minmax_test.In1_1_1
262
                    minmax_test.In2_1_1
263
                    minmax_test.In3_1_1
264
                    minmax_test.In3_1_2
265
                    minmax_test.In4_1_1
266
                    minmax_test.In4_1_2
267
                    minmax_test.In5_1_1
268
                    minmax_test.In5_1_2
269
                    minmax_test.In5_1_3
270
                    minmax_test.In5_1_4
271
                    minmax_test.In6_1_1
272
                    minmax_test.In6_1_2
273
                    minmax_test.In6_1_3
274
                    minmax_test.In6_1_4
275
                    minmax_test.In7_1_1
276
                    minmax_test.In7_1_2
277
                    minmax_test.In7_1_3
278
                    minmax_test.In8_1_1
279
                    minmax_test.In8_1_2
280
                    minmax_test.In8_1_3
281
                    minmax_test.In8_1_4
282
                    minmax_test.In8_1_5
283
                    minmax_test.In8_1_6
284
                    minmax_test.In8_1_7
285
                    minmax_test.Out1_1_1
286
                    minmax_test.Out2_2_1
287
                    minmax_test.Out3_3_1
288
                    minmax_test.Out3_3_2
289
                    minmax_test.Out4_4_1
290
                    minmax_test.Out4_4_2
291
                    minmax_test.Out5_5_1
292
                    minmax_test.Out5_5_2
293
                    minmax_test.Out5_5_3
294
                    minmax_test.Out5_5_4
295
                    minmax_test.Out6_6_1
296
                    minmax_test.Out6_6_2
297
                    minmax_test.Out6_6_3
298
                    minmax_test.Out6_6_4
299
                    minmax_test.Out7_7_1
300
                    minmax_test.Out8_8_1
301
                    minmax_test.ni_0._arrow._first_c
302
                    minmax_test.ni_0._arrow._first_x)
303
))
304