Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_product_matrix_multiple_test / product_matrix_multiple_test.smt2 @ 6c3ea955

History | View | Annotate | Download (19.2 KB)

1
; product_matrix_multiple_test
2
(declare-var product_matrix_multiple_test.In4_1_1 Real)
3
(declare-var product_matrix_multiple_test.In4_1_2 Real)
4
(declare-var product_matrix_multiple_test.In4_1_3 Real)
5
(declare-var product_matrix_multiple_test.In4_1_4 Real)
6
(declare-var product_matrix_multiple_test.In4_1_5 Real)
7
(declare-var product_matrix_multiple_test.In4_1_6 Real)
8
(declare-var product_matrix_multiple_test.In5_1_1 Real)
9
(declare-var product_matrix_multiple_test.In5_1_2 Real)
10
(declare-var product_matrix_multiple_test.In5_1_3 Real)
11
(declare-var product_matrix_multiple_test.In5_1_4 Real)
12
(declare-var product_matrix_multiple_test.In5_1_5 Real)
13
(declare-var product_matrix_multiple_test.In5_1_6 Real)
14
(declare-var product_matrix_multiple_test.In1_1_1 Real)
15
(declare-var product_matrix_multiple_test.In1_1_2 Real)
16
(declare-var product_matrix_multiple_test.In2_1_1 Real)
17
(declare-var product_matrix_multiple_test.In2_1_2 Real)
18
(declare-var product_matrix_multiple_test.In2_1_3 Real)
19
(declare-var product_matrix_multiple_test.In2_1_4 Real)
20
(declare-var product_matrix_multiple_test.In2_1_5 Real)
21
(declare-var product_matrix_multiple_test.In2_1_6 Real)
22
(declare-var product_matrix_multiple_test.In2_1_7 Real)
23
(declare-var product_matrix_multiple_test.In2_1_8 Real)
24
(declare-var product_matrix_multiple_test.In3_1_1 Real)
25
(declare-var product_matrix_multiple_test.In3_1_2 Real)
26
(declare-var product_matrix_multiple_test.In3_1_3 Real)
27
(declare-var product_matrix_multiple_test.In3_1_4 Real)
28
(declare-var product_matrix_multiple_test.In3_1_5 Real)
29
(declare-var product_matrix_multiple_test.In3_1_6 Real)
30
(declare-var product_matrix_multiple_test.In3_1_7 Real)
31
(declare-var product_matrix_multiple_test.In3_1_8 Real)
32
(declare-var product_matrix_multiple_test.In6_1_1 Real)
33
(declare-var product_matrix_multiple_test.In6_1_2 Real)
34
(declare-var product_matrix_multiple_test.In6_1_3 Real)
35
(declare-var product_matrix_multiple_test.In6_1_4 Real)
36
(declare-var product_matrix_multiple_test.In6_1_5 Real)
37
(declare-var product_matrix_multiple_test.In6_1_6 Real)
38
(declare-var product_matrix_multiple_test.In7_1_1 Real)
39
(declare-var product_matrix_multiple_test.In7_1_2 Real)
40
(declare-var product_matrix_multiple_test.In7_1_3 Real)
41
(declare-var product_matrix_multiple_test.In7_1_4 Real)
42
(declare-var product_matrix_multiple_test.In7_1_5 Real)
43
(declare-var product_matrix_multiple_test.In7_1_6 Real)
44
(declare-var product_matrix_multiple_test.In7_1_7 Real)
45
(declare-var product_matrix_multiple_test.In7_1_8 Real)
46
(declare-var product_matrix_multiple_test.In7_1_9 Real)
47
(declare-var product_matrix_multiple_test.In8_1_1 Real)
48
(declare-var product_matrix_multiple_test.In8_1_2 Real)
49
(declare-var product_matrix_multiple_test.In8_1_3 Real)
50
(declare-var product_matrix_multiple_test.In8_1_4 Real)
51
(declare-var product_matrix_multiple_test.In8_1_5 Real)
52
(declare-var product_matrix_multiple_test.In8_1_6 Real)
53
(declare-var product_matrix_multiple_test.In9_1_1 Real)
54
(declare-var product_matrix_multiple_test.In9_1_2 Real)
55
(declare-var product_matrix_multiple_test.Out4_1_1 Real)
56
(declare-var product_matrix_multiple_test.Out4_1_2 Real)
57
(declare-var product_matrix_multiple_test.Out1_2_1 Real)
58
(declare-var product_matrix_multiple_test.Out1_2_2 Real)
59
(declare-var product_matrix_multiple_test.ni_0._arrow._first_c Bool)
60
(declare-var product_matrix_multiple_test.ni_0._arrow._first_m Bool)
61
(declare-var product_matrix_multiple_test.ni_0._arrow._first_x Bool)
62
(declare-var product_matrix_multiple_test.Product1_1_1 Real)
63
(declare-var product_matrix_multiple_test.Product1_1_2 Real)
64
(declare-var product_matrix_multiple_test.Product1_tmp_1 Real)
65
(declare-var product_matrix_multiple_test.Product1_tmp_10 Real)
66
(declare-var product_matrix_multiple_test.Product1_tmp_11 Real)
67
(declare-var product_matrix_multiple_test.Product1_tmp_12 Real)
68
(declare-var product_matrix_multiple_test.Product1_tmp_13 Real)
69
(declare-var product_matrix_multiple_test.Product1_tmp_14 Real)
70
(declare-var product_matrix_multiple_test.Product1_tmp_15 Real)
71
(declare-var product_matrix_multiple_test.Product1_tmp_16 Real)
72
(declare-var product_matrix_multiple_test.Product1_tmp_17 Real)
73
(declare-var product_matrix_multiple_test.Product1_tmp_18 Real)
74
(declare-var product_matrix_multiple_test.Product1_tmp_19 Real)
75
(declare-var product_matrix_multiple_test.Product1_tmp_2 Real)
76
(declare-var product_matrix_multiple_test.Product1_tmp_20 Real)
77
(declare-var product_matrix_multiple_test.Product1_tmp_3 Real)
78
(declare-var product_matrix_multiple_test.Product1_tmp_4 Real)
79
(declare-var product_matrix_multiple_test.Product1_tmp_5 Real)
80
(declare-var product_matrix_multiple_test.Product1_tmp_6 Real)
81
(declare-var product_matrix_multiple_test.Product1_tmp_7 Real)
82
(declare-var product_matrix_multiple_test.Product1_tmp_8 Real)
83
(declare-var product_matrix_multiple_test.Product1_tmp_9 Real)
84
(declare-var product_matrix_multiple_test.Product3_1_1 Real)
85
(declare-var product_matrix_multiple_test.Product3_1_2 Real)
86
(declare-var product_matrix_multiple_test.Product3_tmp_1 Real)
87
(declare-var product_matrix_multiple_test.Product3_tmp_2 Real)
88
(declare-var product_matrix_multiple_test.Product3_tmp_3 Real)
89
(declare-var product_matrix_multiple_test.Product3_tmp_4 Real)
90
(declare-var product_matrix_multiple_test.__product_matrix_multiple_test_1 Bool)
91
(declare-var product_matrix_multiple_test.i_virtual_local Real)
92
(declare-rel product_matrix_multiple_test_reset (Bool Bool))
93
(declare-rel product_matrix_multiple_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 Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Bool Bool))
94

    
95
(rule (=> 
96
  (and 
97
       
98
       (= product_matrix_multiple_test.ni_0._arrow._first_m true)
99
  )
100
  (product_matrix_multiple_test_reset product_matrix_multiple_test.ni_0._arrow._first_c
101
                                      product_matrix_multiple_test.ni_0._arrow._first_m)
102
))
103

    
104
(rule (=> 
105
  (and (= product_matrix_multiple_test.ni_0._arrow._first_m product_matrix_multiple_test.ni_0._arrow._first_c)
106
       (and (= product_matrix_multiple_test.__product_matrix_multiple_test_1 (ite product_matrix_multiple_test.ni_0._arrow._first_m true false))
107
            (= product_matrix_multiple_test.ni_0._arrow._first_x false))
108
       (and (or (not (= product_matrix_multiple_test.__product_matrix_multiple_test_1 true))
109
               (= product_matrix_multiple_test.i_virtual_local 0.0))
110
            (or (not (= product_matrix_multiple_test.__product_matrix_multiple_test_1 false))
111
               (= product_matrix_multiple_test.i_virtual_local 1.0))
112
       )
113
       (= product_matrix_multiple_test.Product3_tmp_4 (+ (+ (* product_matrix_multiple_test.In4_1_4 product_matrix_multiple_test.In5_1_2) (* product_matrix_multiple_test.In4_1_5 product_matrix_multiple_test.In5_1_4)) (* product_matrix_multiple_test.In4_1_6 product_matrix_multiple_test.In5_1_6)))
114
       (= product_matrix_multiple_test.Product3_tmp_3 (+ (+ (* product_matrix_multiple_test.In4_1_4 product_matrix_multiple_test.In5_1_1) (* product_matrix_multiple_test.In4_1_5 product_matrix_multiple_test.In5_1_3)) (* product_matrix_multiple_test.In4_1_6 product_matrix_multiple_test.In5_1_5)))
115
       (= product_matrix_multiple_test.Product3_tmp_2 (+ (+ (* product_matrix_multiple_test.In4_1_1 product_matrix_multiple_test.In5_1_2) (* product_matrix_multiple_test.In4_1_2 product_matrix_multiple_test.In5_1_4)) (* product_matrix_multiple_test.In4_1_3 product_matrix_multiple_test.In5_1_6)))
116
       (= product_matrix_multiple_test.Product3_tmp_1 (+ (+ (* product_matrix_multiple_test.In4_1_1 product_matrix_multiple_test.In5_1_1) (* product_matrix_multiple_test.In4_1_2 product_matrix_multiple_test.In5_1_3)) (* product_matrix_multiple_test.In4_1_3 product_matrix_multiple_test.In5_1_5)))
117
       (= product_matrix_multiple_test.Product3_1_2 (+ (* product_matrix_multiple_test.Product3_tmp_3 product_matrix_multiple_test.In1_1_1) (* product_matrix_multiple_test.Product3_tmp_4 product_matrix_multiple_test.In1_1_2)))
118
       (= product_matrix_multiple_test.Product3_1_1 (+ (* product_matrix_multiple_test.Product3_tmp_1 product_matrix_multiple_test.In1_1_1) (* product_matrix_multiple_test.Product3_tmp_2 product_matrix_multiple_test.In1_1_2)))
119
       (= product_matrix_multiple_test.Product1_tmp_4 (+ (+ (+ (* product_matrix_multiple_test.In2_1_5 product_matrix_multiple_test.In3_1_2) (* product_matrix_multiple_test.In2_1_6 product_matrix_multiple_test.In3_1_4)) (* product_matrix_multiple_test.In2_1_7 product_matrix_multiple_test.In3_1_6)) (* product_matrix_multiple_test.In2_1_8 product_matrix_multiple_test.In3_1_8)))
120
       (= product_matrix_multiple_test.Product1_tmp_3 (+ (+ (+ (* product_matrix_multiple_test.In2_1_5 product_matrix_multiple_test.In3_1_1) (* product_matrix_multiple_test.In2_1_6 product_matrix_multiple_test.In3_1_3)) (* product_matrix_multiple_test.In2_1_7 product_matrix_multiple_test.In3_1_5)) (* product_matrix_multiple_test.In2_1_8 product_matrix_multiple_test.In3_1_7)))
121
       (= product_matrix_multiple_test.Product1_tmp_9 (+ (* product_matrix_multiple_test.Product1_tmp_3 product_matrix_multiple_test.In6_1_2) (* product_matrix_multiple_test.Product1_tmp_4 product_matrix_multiple_test.In6_1_5)))
122
       (= product_matrix_multiple_test.Product1_tmp_8 (+ (* product_matrix_multiple_test.Product1_tmp_3 product_matrix_multiple_test.In6_1_1) (* product_matrix_multiple_test.Product1_tmp_4 product_matrix_multiple_test.In6_1_4)))
123
       (= product_matrix_multiple_test.Product1_tmp_2 (+ (+ (+ (* product_matrix_multiple_test.In2_1_1 product_matrix_multiple_test.In3_1_2) (* product_matrix_multiple_test.In2_1_2 product_matrix_multiple_test.In3_1_4)) (* product_matrix_multiple_test.In2_1_3 product_matrix_multiple_test.In3_1_6)) (* product_matrix_multiple_test.In2_1_4 product_matrix_multiple_test.In3_1_8)))
124
       (= product_matrix_multiple_test.Product1_tmp_1 (+ (+ (+ (* product_matrix_multiple_test.In2_1_1 product_matrix_multiple_test.In3_1_1) (* product_matrix_multiple_test.In2_1_2 product_matrix_multiple_test.In3_1_3)) (* product_matrix_multiple_test.In2_1_3 product_matrix_multiple_test.In3_1_5)) (* product_matrix_multiple_test.In2_1_4 product_matrix_multiple_test.In3_1_7)))
125
       (= product_matrix_multiple_test.Product1_tmp_7 (+ (* product_matrix_multiple_test.Product1_tmp_1 product_matrix_multiple_test.In6_1_3) (* product_matrix_multiple_test.Product1_tmp_2 product_matrix_multiple_test.In6_1_6)))
126
       (= product_matrix_multiple_test.Product1_tmp_6 (+ (* product_matrix_multiple_test.Product1_tmp_1 product_matrix_multiple_test.In6_1_2) (* product_matrix_multiple_test.Product1_tmp_2 product_matrix_multiple_test.In6_1_5)))
127
       (= product_matrix_multiple_test.Product1_tmp_5 (+ (* product_matrix_multiple_test.Product1_tmp_1 product_matrix_multiple_test.In6_1_1) (* product_matrix_multiple_test.Product1_tmp_2 product_matrix_multiple_test.In6_1_4)))
128
       (= product_matrix_multiple_test.Product1_tmp_10 (+ (* product_matrix_multiple_test.Product1_tmp_3 product_matrix_multiple_test.In6_1_3) (* product_matrix_multiple_test.Product1_tmp_4 product_matrix_multiple_test.In6_1_6)))
129
       (= product_matrix_multiple_test.Product1_tmp_16 (+ (+ (* product_matrix_multiple_test.Product1_tmp_8 product_matrix_multiple_test.In7_1_3) (* product_matrix_multiple_test.Product1_tmp_9 product_matrix_multiple_test.In7_1_6)) (* product_matrix_multiple_test.Product1_tmp_10 product_matrix_multiple_test.In7_1_9)))
130
       (= product_matrix_multiple_test.Product1_tmp_15 (+ (+ (* product_matrix_multiple_test.Product1_tmp_8 product_matrix_multiple_test.In7_1_2) (* product_matrix_multiple_test.Product1_tmp_9 product_matrix_multiple_test.In7_1_5)) (* product_matrix_multiple_test.Product1_tmp_10 product_matrix_multiple_test.In7_1_8)))
131
       (= product_matrix_multiple_test.Product1_tmp_14 (+ (+ (* product_matrix_multiple_test.Product1_tmp_8 product_matrix_multiple_test.In7_1_1) (* product_matrix_multiple_test.Product1_tmp_9 product_matrix_multiple_test.In7_1_4)) (* product_matrix_multiple_test.Product1_tmp_10 product_matrix_multiple_test.In7_1_7)))
132
       (= product_matrix_multiple_test.Product1_tmp_20 (+ (+ (* product_matrix_multiple_test.Product1_tmp_14 product_matrix_multiple_test.In8_1_2) (* product_matrix_multiple_test.Product1_tmp_15 product_matrix_multiple_test.In8_1_4)) (* product_matrix_multiple_test.Product1_tmp_16 product_matrix_multiple_test.In8_1_6)))
133
       (= product_matrix_multiple_test.Product1_tmp_19 (+ (+ (* product_matrix_multiple_test.Product1_tmp_14 product_matrix_multiple_test.In8_1_1) (* product_matrix_multiple_test.Product1_tmp_15 product_matrix_multiple_test.In8_1_3)) (* product_matrix_multiple_test.Product1_tmp_16 product_matrix_multiple_test.In8_1_5)))
134
       (= product_matrix_multiple_test.Product1_tmp_13 (+ (+ (* product_matrix_multiple_test.Product1_tmp_5 product_matrix_multiple_test.In7_1_3) (* product_matrix_multiple_test.Product1_tmp_6 product_matrix_multiple_test.In7_1_6)) (* product_matrix_multiple_test.Product1_tmp_7 product_matrix_multiple_test.In7_1_9)))
135
       (= product_matrix_multiple_test.Product1_tmp_12 (+ (+ (* product_matrix_multiple_test.Product1_tmp_5 product_matrix_multiple_test.In7_1_2) (* product_matrix_multiple_test.Product1_tmp_6 product_matrix_multiple_test.In7_1_5)) (* product_matrix_multiple_test.Product1_tmp_7 product_matrix_multiple_test.In7_1_8)))
136
       (= product_matrix_multiple_test.Product1_tmp_11 (+ (+ (* product_matrix_multiple_test.Product1_tmp_5 product_matrix_multiple_test.In7_1_1) (* product_matrix_multiple_test.Product1_tmp_6 product_matrix_multiple_test.In7_1_4)) (* product_matrix_multiple_test.Product1_tmp_7 product_matrix_multiple_test.In7_1_7)))
137
       (= product_matrix_multiple_test.Product1_tmp_18 (+ (+ (* product_matrix_multiple_test.Product1_tmp_11 product_matrix_multiple_test.In8_1_2) (* product_matrix_multiple_test.Product1_tmp_12 product_matrix_multiple_test.In8_1_4)) (* product_matrix_multiple_test.Product1_tmp_13 product_matrix_multiple_test.In8_1_6)))
138
       (= product_matrix_multiple_test.Product1_tmp_17 (+ (+ (* product_matrix_multiple_test.Product1_tmp_11 product_matrix_multiple_test.In8_1_1) (* product_matrix_multiple_test.Product1_tmp_12 product_matrix_multiple_test.In8_1_3)) (* product_matrix_multiple_test.Product1_tmp_13 product_matrix_multiple_test.In8_1_5)))
139
       (= product_matrix_multiple_test.Product1_1_2 (+ (* product_matrix_multiple_test.Product1_tmp_19 product_matrix_multiple_test.In9_1_1) (* product_matrix_multiple_test.Product1_tmp_20 product_matrix_multiple_test.In9_1_2)))
140
       (= product_matrix_multiple_test.Product1_1_1 (+ (* product_matrix_multiple_test.Product1_tmp_17 product_matrix_multiple_test.In9_1_1) (* product_matrix_multiple_test.Product1_tmp_18 product_matrix_multiple_test.In9_1_2)))
141
       (= product_matrix_multiple_test.Out4_1_2 product_matrix_multiple_test.Product3_1_2)
142
       (= product_matrix_multiple_test.Out4_1_1 product_matrix_multiple_test.Product3_1_1)
143
       (= product_matrix_multiple_test.Out1_2_2 product_matrix_multiple_test.Product1_1_2)
144
       (= product_matrix_multiple_test.Out1_2_1 product_matrix_multiple_test.Product1_1_1)
145
       )
146
  (product_matrix_multiple_test_step product_matrix_multiple_test.In4_1_1
147
                                     product_matrix_multiple_test.In4_1_2
148
                                     product_matrix_multiple_test.In4_1_3
149
                                     product_matrix_multiple_test.In4_1_4
150
                                     product_matrix_multiple_test.In4_1_5
151
                                     product_matrix_multiple_test.In4_1_6
152
                                     product_matrix_multiple_test.In5_1_1
153
                                     product_matrix_multiple_test.In5_1_2
154
                                     product_matrix_multiple_test.In5_1_3
155
                                     product_matrix_multiple_test.In5_1_4
156
                                     product_matrix_multiple_test.In5_1_5
157
                                     product_matrix_multiple_test.In5_1_6
158
                                     product_matrix_multiple_test.In1_1_1
159
                                     product_matrix_multiple_test.In1_1_2
160
                                     product_matrix_multiple_test.In2_1_1
161
                                     product_matrix_multiple_test.In2_1_2
162
                                     product_matrix_multiple_test.In2_1_3
163
                                     product_matrix_multiple_test.In2_1_4
164
                                     product_matrix_multiple_test.In2_1_5
165
                                     product_matrix_multiple_test.In2_1_6
166
                                     product_matrix_multiple_test.In2_1_7
167
                                     product_matrix_multiple_test.In2_1_8
168
                                     product_matrix_multiple_test.In3_1_1
169
                                     product_matrix_multiple_test.In3_1_2
170
                                     product_matrix_multiple_test.In3_1_3
171
                                     product_matrix_multiple_test.In3_1_4
172
                                     product_matrix_multiple_test.In3_1_5
173
                                     product_matrix_multiple_test.In3_1_6
174
                                     product_matrix_multiple_test.In3_1_7
175
                                     product_matrix_multiple_test.In3_1_8
176
                                     product_matrix_multiple_test.In6_1_1
177
                                     product_matrix_multiple_test.In6_1_2
178
                                     product_matrix_multiple_test.In6_1_3
179
                                     product_matrix_multiple_test.In6_1_4
180
                                     product_matrix_multiple_test.In6_1_5
181
                                     product_matrix_multiple_test.In6_1_6
182
                                     product_matrix_multiple_test.In7_1_1
183
                                     product_matrix_multiple_test.In7_1_2
184
                                     product_matrix_multiple_test.In7_1_3
185
                                     product_matrix_multiple_test.In7_1_4
186
                                     product_matrix_multiple_test.In7_1_5
187
                                     product_matrix_multiple_test.In7_1_6
188
                                     product_matrix_multiple_test.In7_1_7
189
                                     product_matrix_multiple_test.In7_1_8
190
                                     product_matrix_multiple_test.In7_1_9
191
                                     product_matrix_multiple_test.In8_1_1
192
                                     product_matrix_multiple_test.In8_1_2
193
                                     product_matrix_multiple_test.In8_1_3
194
                                     product_matrix_multiple_test.In8_1_4
195
                                     product_matrix_multiple_test.In8_1_5
196
                                     product_matrix_multiple_test.In8_1_6
197
                                     product_matrix_multiple_test.In9_1_1
198
                                     product_matrix_multiple_test.In9_1_2
199
                                     product_matrix_multiple_test.Out4_1_1
200
                                     product_matrix_multiple_test.Out4_1_2
201
                                     product_matrix_multiple_test.Out1_2_1
202
                                     product_matrix_multiple_test.Out1_2_2
203
                                     product_matrix_multiple_test.ni_0._arrow._first_c
204
                                     product_matrix_multiple_test.ni_0._arrow._first_x)
205
))
206