Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_product_matrix_test / product_matrix_test.smt2 @ 6c3ea955

History | View | Annotate | Download (10.5 KB)

1
; product_matrix_test
2
(declare-var product_matrix_test.In1_1_1 Real)
3
(declare-var product_matrix_test.In2_1_1 Real)
4
(declare-var product_matrix_test.In2_1_2 Real)
5
(declare-var product_matrix_test.In2_1_3 Real)
6
(declare-var product_matrix_test.In3_1_1 Real)
7
(declare-var product_matrix_test.In3_1_2 Real)
8
(declare-var product_matrix_test.In3_1_3 Real)
9
(declare-var product_matrix_test.In3_1_4 Real)
10
(declare-var product_matrix_test.In3_1_5 Real)
11
(declare-var product_matrix_test.In3_1_6 Real)
12
(declare-var product_matrix_test.In4_1_1 Real)
13
(declare-var product_matrix_test.In4_1_2 Real)
14
(declare-var product_matrix_test.In4_1_3 Real)
15
(declare-var product_matrix_test.In4_1_4 Real)
16
(declare-var product_matrix_test.In4_1_5 Real)
17
(declare-var product_matrix_test.In4_1_6 Real)
18
(declare-var product_matrix_test.In5_1_1 Real)
19
(declare-var product_matrix_test.In5_1_2 Real)
20
(declare-var product_matrix_test.In5_1_3 Real)
21
(declare-var product_matrix_test.In5_1_4 Real)
22
(declare-var product_matrix_test.In5_1_5 Real)
23
(declare-var product_matrix_test.In5_1_6 Real)
24
(declare-var product_matrix_test.In5_1_7 Real)
25
(declare-var product_matrix_test.In5_1_8 Real)
26
(declare-var product_matrix_test.In5_1_9 Real)
27
(declare-var product_matrix_test.In6_1_1 Real)
28
(declare-var product_matrix_test.In6_1_2 Real)
29
(declare-var product_matrix_test.In7_1_1 Real)
30
(declare-var product_matrix_test.In7_1_2 Real)
31
(declare-var product_matrix_test.Out1_1_1 Real)
32
(declare-var product_matrix_test.Out2_2_1 Real)
33
(declare-var product_matrix_test.Out2_2_2 Real)
34
(declare-var product_matrix_test.Out2_2_3 Real)
35
(declare-var product_matrix_test.Out3_3_1 Real)
36
(declare-var product_matrix_test.Out3_3_2 Real)
37
(declare-var product_matrix_test.Out3_3_3 Real)
38
(declare-var product_matrix_test.Out3_3_4 Real)
39
(declare-var product_matrix_test.Out3_3_5 Real)
40
(declare-var product_matrix_test.Out3_3_6 Real)
41
(declare-var product_matrix_test.Out4_4_1 Real)
42
(declare-var product_matrix_test.Out4_4_2 Real)
43
(declare-var product_matrix_test.Out4_4_3 Real)
44
(declare-var product_matrix_test.Out4_4_4 Real)
45
(declare-var product_matrix_test.Out4_4_5 Real)
46
(declare-var product_matrix_test.Out4_4_6 Real)
47
(declare-var product_matrix_test.Out5_5_1 Real)
48
(declare-var product_matrix_test.ni_0._arrow._first_c Bool)
49
(declare-var product_matrix_test.ni_0._arrow._first_m Bool)
50
(declare-var product_matrix_test.ni_0._arrow._first_x Bool)
51
(declare-var product_matrix_test.Product1_1_1 Real)
52
(declare-var product_matrix_test.Product1_1_2 Real)
53
(declare-var product_matrix_test.Product1_1_3 Real)
54
(declare-var product_matrix_test.Product2_1_1 Real)
55
(declare-var product_matrix_test.Product2_1_2 Real)
56
(declare-var product_matrix_test.Product2_1_3 Real)
57
(declare-var product_matrix_test.Product2_1_4 Real)
58
(declare-var product_matrix_test.Product2_1_5 Real)
59
(declare-var product_matrix_test.Product2_1_6 Real)
60
(declare-var product_matrix_test.Product3_1_1 Real)
61
(declare-var product_matrix_test.Product3_1_2 Real)
62
(declare-var product_matrix_test.Product3_1_3 Real)
63
(declare-var product_matrix_test.Product3_1_4 Real)
64
(declare-var product_matrix_test.Product3_1_5 Real)
65
(declare-var product_matrix_test.Product3_1_6 Real)
66
(declare-var product_matrix_test.Product4_1_1 Real)
67
(declare-var product_matrix_test.Product_1_1 Real)
68
(declare-var product_matrix_test.__product_matrix_test_1 Bool)
69
(declare-var product_matrix_test.i_virtual_local Real)
70
(declare-rel product_matrix_test_reset (Bool Bool))
71
(declare-rel product_matrix_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 Bool Bool))
72

    
73
(rule (=> 
74
  (and 
75
       
76
       (= product_matrix_test.ni_0._arrow._first_m true)
77
  )
78
  (product_matrix_test_reset product_matrix_test.ni_0._arrow._first_c
79
                             product_matrix_test.ni_0._arrow._first_m)
80
))
81

    
82
(rule (=> 
83
  (and (= product_matrix_test.ni_0._arrow._first_m product_matrix_test.ni_0._arrow._first_c)
84
       (and (= product_matrix_test.__product_matrix_test_1 (ite product_matrix_test.ni_0._arrow._first_m true false))
85
            (= product_matrix_test.ni_0._arrow._first_x false))
86
       (and (or (not (= product_matrix_test.__product_matrix_test_1 true))
87
               (= product_matrix_test.i_virtual_local 0.0))
88
            (or (not (= product_matrix_test.__product_matrix_test_1 false))
89
               (= product_matrix_test.i_virtual_local 1.0))
90
       )
91
       (= product_matrix_test.Product_1_1 product_matrix_test.In1_1_1)
92
       (= product_matrix_test.Product4_1_1 (+ (* product_matrix_test.In6_1_1 product_matrix_test.In7_1_1) (* product_matrix_test.In6_1_2 product_matrix_test.In7_1_2)))
93
       (= product_matrix_test.Product3_1_6 (+ (+ (* product_matrix_test.In4_1_4 product_matrix_test.In5_1_3) (* product_matrix_test.In4_1_5 product_matrix_test.In5_1_6)) (* product_matrix_test.In4_1_6 product_matrix_test.In5_1_9)))
94
       (= product_matrix_test.Product3_1_5 (+ (+ (* product_matrix_test.In4_1_4 product_matrix_test.In5_1_2) (* product_matrix_test.In4_1_5 product_matrix_test.In5_1_5)) (* product_matrix_test.In4_1_6 product_matrix_test.In5_1_8)))
95
       (= product_matrix_test.Product3_1_4 (+ (+ (* product_matrix_test.In4_1_4 product_matrix_test.In5_1_1) (* product_matrix_test.In4_1_5 product_matrix_test.In5_1_4)) (* product_matrix_test.In4_1_6 product_matrix_test.In5_1_7)))
96
       (= product_matrix_test.Product3_1_3 (+ (+ (* product_matrix_test.In4_1_1 product_matrix_test.In5_1_3) (* product_matrix_test.In4_1_2 product_matrix_test.In5_1_6)) (* product_matrix_test.In4_1_3 product_matrix_test.In5_1_9)))
97
       (= product_matrix_test.Product3_1_2 (+ (+ (* product_matrix_test.In4_1_1 product_matrix_test.In5_1_2) (* product_matrix_test.In4_1_2 product_matrix_test.In5_1_5)) (* product_matrix_test.In4_1_3 product_matrix_test.In5_1_8)))
98
       (= product_matrix_test.Product3_1_1 (+ (+ (* product_matrix_test.In4_1_1 product_matrix_test.In5_1_1) (* product_matrix_test.In4_1_2 product_matrix_test.In5_1_4)) (* product_matrix_test.In4_1_3 product_matrix_test.In5_1_7)))
99
       (= product_matrix_test.Product2_1_6 product_matrix_test.In3_1_6)
100
       (= product_matrix_test.Product2_1_5 product_matrix_test.In3_1_5)
101
       (= product_matrix_test.Product2_1_4 product_matrix_test.In3_1_4)
102
       (= product_matrix_test.Product2_1_3 product_matrix_test.In3_1_3)
103
       (= product_matrix_test.Product2_1_2 product_matrix_test.In3_1_2)
104
       (= product_matrix_test.Product2_1_1 product_matrix_test.In3_1_1)
105
       (= product_matrix_test.Product1_1_3 product_matrix_test.In2_1_3)
106
       (= product_matrix_test.Product1_1_2 product_matrix_test.In2_1_2)
107
       (= product_matrix_test.Product1_1_1 product_matrix_test.In2_1_1)
108
       (= product_matrix_test.Out5_5_1 product_matrix_test.Product4_1_1)
109
       (= product_matrix_test.Out4_4_6 product_matrix_test.Product3_1_6)
110
       (= product_matrix_test.Out4_4_5 product_matrix_test.Product3_1_5)
111
       (= product_matrix_test.Out4_4_4 product_matrix_test.Product3_1_4)
112
       (= product_matrix_test.Out4_4_3 product_matrix_test.Product3_1_3)
113
       (= product_matrix_test.Out4_4_2 product_matrix_test.Product3_1_2)
114
       (= product_matrix_test.Out4_4_1 product_matrix_test.Product3_1_1)
115
       (= product_matrix_test.Out3_3_6 product_matrix_test.Product2_1_6)
116
       (= product_matrix_test.Out3_3_5 product_matrix_test.Product2_1_5)
117
       (= product_matrix_test.Out3_3_4 product_matrix_test.Product2_1_4)
118
       (= product_matrix_test.Out3_3_3 product_matrix_test.Product2_1_3)
119
       (= product_matrix_test.Out3_3_2 product_matrix_test.Product2_1_2)
120
       (= product_matrix_test.Out3_3_1 product_matrix_test.Product2_1_1)
121
       (= product_matrix_test.Out2_2_3 product_matrix_test.Product1_1_3)
122
       (= product_matrix_test.Out2_2_2 product_matrix_test.Product1_1_2)
123
       (= product_matrix_test.Out2_2_1 product_matrix_test.Product1_1_1)
124
       (= product_matrix_test.Out1_1_1 product_matrix_test.Product_1_1)
125
       )
126
  (product_matrix_test_step product_matrix_test.In1_1_1
127
                            product_matrix_test.In2_1_1
128
                            product_matrix_test.In2_1_2
129
                            product_matrix_test.In2_1_3
130
                            product_matrix_test.In3_1_1
131
                            product_matrix_test.In3_1_2
132
                            product_matrix_test.In3_1_3
133
                            product_matrix_test.In3_1_4
134
                            product_matrix_test.In3_1_5
135
                            product_matrix_test.In3_1_6
136
                            product_matrix_test.In4_1_1
137
                            product_matrix_test.In4_1_2
138
                            product_matrix_test.In4_1_3
139
                            product_matrix_test.In4_1_4
140
                            product_matrix_test.In4_1_5
141
                            product_matrix_test.In4_1_6
142
                            product_matrix_test.In5_1_1
143
                            product_matrix_test.In5_1_2
144
                            product_matrix_test.In5_1_3
145
                            product_matrix_test.In5_1_4
146
                            product_matrix_test.In5_1_5
147
                            product_matrix_test.In5_1_6
148
                            product_matrix_test.In5_1_7
149
                            product_matrix_test.In5_1_8
150
                            product_matrix_test.In5_1_9
151
                            product_matrix_test.In6_1_1
152
                            product_matrix_test.In6_1_2
153
                            product_matrix_test.In7_1_1
154
                            product_matrix_test.In7_1_2
155
                            product_matrix_test.Out1_1_1
156
                            product_matrix_test.Out2_2_1
157
                            product_matrix_test.Out2_2_2
158
                            product_matrix_test.Out2_2_3
159
                            product_matrix_test.Out3_3_1
160
                            product_matrix_test.Out3_3_2
161
                            product_matrix_test.Out3_3_3
162
                            product_matrix_test.Out3_3_4
163
                            product_matrix_test.Out3_3_5
164
                            product_matrix_test.Out3_3_6
165
                            product_matrix_test.Out4_4_1
166
                            product_matrix_test.Out4_4_2
167
                            product_matrix_test.Out4_4_3
168
                            product_matrix_test.Out4_4_4
169
                            product_matrix_test.Out4_4_5
170
                            product_matrix_test.Out4_4_6
171
                            product_matrix_test.Out5_5_1
172
                            product_matrix_test.ni_0._arrow._first_c
173
                            product_matrix_test.ni_0._arrow._first_x)
174
))
175