Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_merge_test / merge_test.smt2 @ 6c3ea955

History | View | Annotate | Download (11.9 KB)

1 6c3ea955 bourbouh
; merge_test
2
(declare-var merge_test.i_virtual Real)
3
(declare-var merge_test.Out1_1_1 Real)
4
(declare-var merge_test.Out1_1_2 Real)
5
(declare-var merge_test.Out1_1_3 Real)
6
(declare-var merge_test.Out1_1_4 Real)
7
(declare-var merge_test.Out1_1_5 Real)
8
(declare-var merge_test.Out1_1_6 Real)
9
(declare-var merge_test.__merge_test_2_c Real)
10
(declare-var merge_test.__merge_test_3_c Real)
11
(declare-var merge_test.__merge_test_4_c Real)
12
(declare-var merge_test.__merge_test_5_c Real)
13
(declare-var merge_test.__merge_test_6_c Real)
14
(declare-var merge_test.__merge_test_7_c Real)
15
(declare-var merge_test.ni_0._arrow._first_c Bool)
16
(declare-var merge_test.__merge_test_2_m Real)
17
(declare-var merge_test.__merge_test_3_m Real)
18
(declare-var merge_test.__merge_test_4_m Real)
19
(declare-var merge_test.__merge_test_5_m Real)
20
(declare-var merge_test.__merge_test_6_m Real)
21
(declare-var merge_test.__merge_test_7_m Real)
22
(declare-var merge_test.ni_0._arrow._first_m Bool)
23
(declare-var merge_test.__merge_test_2_x Real)
24
(declare-var merge_test.__merge_test_3_x Real)
25
(declare-var merge_test.__merge_test_4_x Real)
26
(declare-var merge_test.__merge_test_5_x Real)
27
(declare-var merge_test.__merge_test_6_x Real)
28
(declare-var merge_test.__merge_test_7_x Real)
29
(declare-var merge_test.ni_0._arrow._first_x Bool)
30
(declare-var merge_test.Constant1_1_1 Real)
31
(declare-var merge_test.Constant1_1_2 Real)
32
(declare-var merge_test.Constant1_1_3 Real)
33
(declare-var merge_test.Constant1_1_4 Real)
34
(declare-var merge_test.Constant1_1_5 Real)
35
(declare-var merge_test.Constant1_1_6 Real)
36
(declare-var merge_test.Constant2_1_1 Real)
37
(declare-var merge_test.Constant2_1_2 Real)
38
(declare-var merge_test.Constant2_1_3 Real)
39
(declare-var merge_test.Constant2_1_4 Real)
40
(declare-var merge_test.Constant2_1_5 Real)
41
(declare-var merge_test.Constant2_1_6 Real)
42
(declare-var merge_test.Constant_1_1 Real)
43
(declare-var merge_test.Constant_1_2 Real)
44
(declare-var merge_test.Constant_1_3 Real)
45
(declare-var merge_test.Constant_1_4 Real)
46
(declare-var merge_test.Constant_1_5 Real)
47
(declare-var merge_test.Constant_1_6 Real)
48
(declare-var merge_test.Merge_1_1 Real)
49
(declare-var merge_test.Merge_1_2 Real)
50
(declare-var merge_test.Merge_1_3 Real)
51
(declare-var merge_test.Merge_1_4 Real)
52
(declare-var merge_test.Merge_1_5 Real)
53
(declare-var merge_test.Merge_1_6 Real)
54
(declare-var merge_test.Merge_8_0233_input0_hasChanged Bool)
55
(declare-var merge_test.Merge_8_0233_input1_hasChanged Bool)
56
(declare-var merge_test.Merge_8_0233_input2_hasChanged Bool)
57
(declare-var merge_test.__merge_test_1 Bool)
58
(declare-var merge_test.i_virtual_local Real)
59
(declare-rel merge_test_reset (Real Real Real Real Real Real Bool Real Real Real Real Real Real Bool))
60
(declare-rel merge_test_step (Real Real Real Real Real Real Real Real Real Real Real Real Real Bool Real Real Real Real Real Real Bool))
61
62
(rule (=> 
63
  (and 
64
       (= merge_test.__merge_test_2_m merge_test.__merge_test_2_c)
65
       (= merge_test.__merge_test_3_m merge_test.__merge_test_3_c)
66
       (= merge_test.__merge_test_4_m merge_test.__merge_test_4_c)
67
       (= merge_test.__merge_test_5_m merge_test.__merge_test_5_c)
68
       (= merge_test.__merge_test_6_m merge_test.__merge_test_6_c)
69
       (= merge_test.__merge_test_7_m merge_test.__merge_test_7_c)
70
       (= merge_test.ni_0._arrow._first_m true)
71
  )
72
  (merge_test_reset merge_test.__merge_test_2_c
73
                    merge_test.__merge_test_3_c
74
                    merge_test.__merge_test_4_c
75
                    merge_test.__merge_test_5_c
76
                    merge_test.__merge_test_6_c
77
                    merge_test.__merge_test_7_c
78
                    merge_test.ni_0._arrow._first_c
79
                    merge_test.__merge_test_2_m
80
                    merge_test.__merge_test_3_m
81
                    merge_test.__merge_test_4_m
82
                    merge_test.__merge_test_5_m
83
                    merge_test.__merge_test_6_m
84
                    merge_test.__merge_test_7_m
85
                    merge_test.ni_0._arrow._first_m)
86
))
87
88
(rule (=> 
89
  (and (= merge_test.ni_0._arrow._first_m merge_test.ni_0._arrow._first_c)
90
       (and (= merge_test.__merge_test_1 (ite merge_test.ni_0._arrow._first_m true false))
91
            (= merge_test.ni_0._arrow._first_x false))
92
       (and (or (not (= merge_test.__merge_test_1 true))
93
               (= merge_test.i_virtual_local 0.0))
94
            (or (not (= merge_test.__merge_test_1 false))
95
               (= merge_test.i_virtual_local 1.0))
96
       )
97
       (= merge_test.Merge_8_0233_input2_hasChanged true)
98
       (= merge_test.Merge_8_0233_input1_hasChanged true)
99
       (= merge_test.Merge_8_0233_input0_hasChanged true)
100
       (= merge_test.Constant_1_1 1.00000000)
101
       (= merge_test.Constant2_1_1 1.00000000)
102
       (= merge_test.Constant1_1_1 1.00000000)
103
       (and (or (not (= merge_test.Merge_8_0233_input0_hasChanged true))
104
               (= merge_test.Merge_1_1 merge_test.Constant1_1_1))
105
            (or (not (= merge_test.Merge_8_0233_input0_hasChanged false))
106
               (and (or (not (= merge_test.Merge_8_0233_input1_hasChanged true))
107
                       (= merge_test.Merge_1_1 merge_test.Constant_1_1))
108
                    (or (not (= merge_test.Merge_8_0233_input1_hasChanged false))
109
                       (and (or (not (= merge_test.Merge_8_0233_input2_hasChanged true))
110
                               (= merge_test.Merge_1_1 merge_test.Constant2_1_1))
111
                            (or (not (= merge_test.Merge_8_0233_input2_hasChanged false))
112
                               (= merge_test.Merge_1_1 merge_test.__merge_test_7_c))
113
                       ))
114
               ))
115
       )
116
       (= merge_test.__merge_test_7_x merge_test.Merge_1_1)
117
       (= merge_test.Constant_1_2 2.00000000)
118
       (= merge_test.Constant2_1_2 2.00000000)
119
       (= merge_test.Constant1_1_2 2.00000000)
120
       (and (or (not (= merge_test.Merge_8_0233_input0_hasChanged true))
121
               (= merge_test.Merge_1_2 merge_test.Constant1_1_2))
122
            (or (not (= merge_test.Merge_8_0233_input0_hasChanged false))
123
               (and (or (not (= merge_test.Merge_8_0233_input1_hasChanged true))
124
                       (= merge_test.Merge_1_2 merge_test.Constant_1_2))
125
                    (or (not (= merge_test.Merge_8_0233_input1_hasChanged false))
126
                       (and (or (not (= merge_test.Merge_8_0233_input2_hasChanged true))
127
                               (= merge_test.Merge_1_2 merge_test.Constant2_1_2))
128
                            (or (not (= merge_test.Merge_8_0233_input2_hasChanged false))
129
                               (= merge_test.Merge_1_2 merge_test.__merge_test_6_c))
130
                       ))
131
               ))
132
       )
133
       (= merge_test.__merge_test_6_x merge_test.Merge_1_2)
134
       (= merge_test.Constant_1_3 3.00000000)
135
       (= merge_test.Constant2_1_3 3.00000000)
136
       (= merge_test.Constant1_1_3 3.00000000)
137
       (and (or (not (= merge_test.Merge_8_0233_input0_hasChanged true))
138
               (= merge_test.Merge_1_3 merge_test.Constant1_1_3))
139
            (or (not (= merge_test.Merge_8_0233_input0_hasChanged false))
140
               (and (or (not (= merge_test.Merge_8_0233_input1_hasChanged true))
141
                       (= merge_test.Merge_1_3 merge_test.Constant_1_3))
142
                    (or (not (= merge_test.Merge_8_0233_input1_hasChanged false))
143
                       (and (or (not (= merge_test.Merge_8_0233_input2_hasChanged true))
144
                               (= merge_test.Merge_1_3 merge_test.Constant2_1_3))
145
                            (or (not (= merge_test.Merge_8_0233_input2_hasChanged false))
146
                               (= merge_test.Merge_1_3 merge_test.__merge_test_5_c))
147
                       ))
148
               ))
149
       )
150
       (= merge_test.__merge_test_5_x merge_test.Merge_1_3)
151
       (= merge_test.Constant_1_4 4.00000000)
152
       (= merge_test.Constant2_1_4 4.00000000)
153
       (= merge_test.Constant1_1_4 4.00000000)
154
       (and (or (not (= merge_test.Merge_8_0233_input0_hasChanged true))
155
               (= merge_test.Merge_1_4 merge_test.Constant1_1_4))
156
            (or (not (= merge_test.Merge_8_0233_input0_hasChanged false))
157
               (and (or (not (= merge_test.Merge_8_0233_input1_hasChanged true))
158
                       (= merge_test.Merge_1_4 merge_test.Constant_1_4))
159
                    (or (not (= merge_test.Merge_8_0233_input1_hasChanged false))
160
                       (and (or (not (= merge_test.Merge_8_0233_input2_hasChanged true))
161
                               (= merge_test.Merge_1_4 merge_test.Constant2_1_4))
162
                            (or (not (= merge_test.Merge_8_0233_input2_hasChanged false))
163
                               (= merge_test.Merge_1_4 merge_test.__merge_test_4_c))
164
                       ))
165
               ))
166
       )
167
       (= merge_test.__merge_test_4_x merge_test.Merge_1_4)
168
       (= merge_test.Constant_1_5 5.00000000)
169
       (= merge_test.Constant2_1_5 5.00000000)
170
       (= merge_test.Constant1_1_5 5.00000000)
171
       (and (or (not (= merge_test.Merge_8_0233_input0_hasChanged true))
172
               (= merge_test.Merge_1_5 merge_test.Constant1_1_5))
173
            (or (not (= merge_test.Merge_8_0233_input0_hasChanged false))
174
               (and (or (not (= merge_test.Merge_8_0233_input1_hasChanged true))
175
                       (= merge_test.Merge_1_5 merge_test.Constant_1_5))
176
                    (or (not (= merge_test.Merge_8_0233_input1_hasChanged false))
177
                       (and (or (not (= merge_test.Merge_8_0233_input2_hasChanged true))
178
                               (= merge_test.Merge_1_5 merge_test.Constant2_1_5))
179
                            (or (not (= merge_test.Merge_8_0233_input2_hasChanged false))
180
                               (= merge_test.Merge_1_5 merge_test.__merge_test_3_c))
181
                       ))
182
               ))
183
       )
184
       (= merge_test.__merge_test_3_x merge_test.Merge_1_5)
185
       (= merge_test.Constant_1_6 6.00000000)
186
       (= merge_test.Constant2_1_6 6.00000000)
187
       (= merge_test.Constant1_1_6 6.00000000)
188
       (and (or (not (= merge_test.Merge_8_0233_input0_hasChanged true))
189
               (= merge_test.Merge_1_6 merge_test.Constant1_1_6))
190
            (or (not (= merge_test.Merge_8_0233_input0_hasChanged false))
191
               (and (or (not (= merge_test.Merge_8_0233_input1_hasChanged true))
192
                       (= merge_test.Merge_1_6 merge_test.Constant_1_6))
193
                    (or (not (= merge_test.Merge_8_0233_input1_hasChanged false))
194
                       (and (or (not (= merge_test.Merge_8_0233_input2_hasChanged true))
195
                               (= merge_test.Merge_1_6 merge_test.Constant2_1_6))
196
                            (or (not (= merge_test.Merge_8_0233_input2_hasChanged false))
197
                               (= merge_test.Merge_1_6 merge_test.__merge_test_2_c))
198
                       ))
199
               ))
200
       )
201
       (= merge_test.__merge_test_2_x merge_test.Merge_1_6)
202
       (= merge_test.Out1_1_6 merge_test.Merge_1_6)
203
       (= merge_test.Out1_1_5 merge_test.Merge_1_5)
204
       (= merge_test.Out1_1_4 merge_test.Merge_1_4)
205
       (= merge_test.Out1_1_3 merge_test.Merge_1_3)
206
       (= merge_test.Out1_1_2 merge_test.Merge_1_2)
207
       (= merge_test.Out1_1_1 merge_test.Merge_1_1)
208
       )
209
  (merge_test_step merge_test.i_virtual
210
                   merge_test.Out1_1_1
211
                   merge_test.Out1_1_2
212
                   merge_test.Out1_1_3
213
                   merge_test.Out1_1_4
214
                   merge_test.Out1_1_5
215
                   merge_test.Out1_1_6
216
                   merge_test.__merge_test_2_c
217
                   merge_test.__merge_test_3_c
218
                   merge_test.__merge_test_4_c
219
                   merge_test.__merge_test_5_c
220
                   merge_test.__merge_test_6_c
221
                   merge_test.__merge_test_7_c
222
                   merge_test.ni_0._arrow._first_c
223
                   merge_test.__merge_test_2_x
224
                   merge_test.__merge_test_3_x
225
                   merge_test.__merge_test_4_x
226
                   merge_test.__merge_test_5_x
227
                   merge_test.__merge_test_6_x
228
                   merge_test.__merge_test_7_x
229
                   merge_test.ni_0._arrow._first_x)
230
))