Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_constant_test / constant_test.smt2 @ 6c3ea955

History | View | Annotate | Download (10 KB)

1
; constant_test
2
(declare-var constant_test.In1_1_1 Real)
3
(declare-var constant_test.In2_1_1 Int)
4
(declare-var constant_test.In3_1_1 Bool)
5
(declare-var constant_test.In4_1_1 Real)
6
(declare-var constant_test.In5_1_1 Int)
7
(declare-var constant_test.In6_1_1 Bool)
8
(declare-var constant_test.Out1_1_1 Real)
9
(declare-var constant_test.Out1_1_2 Real)
10
(declare-var constant_test.Out2_2_1 Int)
11
(declare-var constant_test.Out2_2_2 Int)
12
(declare-var constant_test.Out3_3_1 Bool)
13
(declare-var constant_test.Out3_3_2 Bool)
14
(declare-var constant_test.Out4_4_1 Real)
15
(declare-var constant_test.Out4_4_2 Real)
16
(declare-var constant_test.Out4_4_3 Real)
17
(declare-var constant_test.Out4_4_4 Real)
18
(declare-var constant_test.Out5_5_1 Int)
19
(declare-var constant_test.Out5_5_2 Int)
20
(declare-var constant_test.Out5_5_3 Int)
21
(declare-var constant_test.Out5_5_4 Int)
22
(declare-var constant_test.Out6_6_1 Bool)
23
(declare-var constant_test.Out6_6_2 Bool)
24
(declare-var constant_test.Out6_6_3 Bool)
25
(declare-var constant_test.Out6_6_4 Bool)
26
(declare-var constant_test.Out7_7_1 Real)
27
(declare-var constant_test.Out7_7_2 Real)
28
(declare-var constant_test.Out7_7_3 Real)
29
(declare-var constant_test.Out7_7_4 Real)
30
(declare-var constant_test.Out8_8_1 Int)
31
(declare-var constant_test.Out8_8_2 Int)
32
(declare-var constant_test.Out8_8_3 Int)
33
(declare-var constant_test.Out8_8_4 Int)
34
(declare-var constant_test.Out9_9_1 Bool)
35
(declare-var constant_test.Out9_9_2 Bool)
36
(declare-var constant_test.Out9_9_3 Bool)
37
(declare-var constant_test.Out9_9_4 Bool)
38
(declare-var constant_test.ni_0._arrow._first_c Bool)
39
(declare-var constant_test.ni_0._arrow._first_m Bool)
40
(declare-var constant_test.ni_0._arrow._first_x Bool)
41
(declare-var constant_test.Constant1_1_1 Int)
42
(declare-var constant_test.Constant2_1_1 Bool)
43
(declare-var constant_test.Constant3_1_1 Real)
44
(declare-var constant_test.Constant3_1_2 Real)
45
(declare-var constant_test.Constant3_1_3 Real)
46
(declare-var constant_test.Constant4_1_1 Int)
47
(declare-var constant_test.Constant4_1_2 Int)
48
(declare-var constant_test.Constant4_1_3 Int)
49
(declare-var constant_test.Constant5_1_1 Bool)
50
(declare-var constant_test.Constant5_1_2 Bool)
51
(declare-var constant_test.Constant5_1_3 Bool)
52
(declare-var constant_test.Constant6_1_1 Real)
53
(declare-var constant_test.Constant6_1_2 Real)
54
(declare-var constant_test.Constant6_1_3 Real)
55
(declare-var constant_test.Constant6_1_4 Real)
56
(declare-var constant_test.Constant7_1_1 Int)
57
(declare-var constant_test.Constant7_1_2 Int)
58
(declare-var constant_test.Constant7_1_3 Int)
59
(declare-var constant_test.Constant7_1_4 Int)
60
(declare-var constant_test.Constant8_1_1 Bool)
61
(declare-var constant_test.Constant8_1_2 Bool)
62
(declare-var constant_test.Constant8_1_3 Bool)
63
(declare-var constant_test.Constant8_1_4 Bool)
64
(declare-var constant_test.Constant_1_1 Real)
65
(declare-var constant_test.Mux1_1_1 Int)
66
(declare-var constant_test.Mux1_1_2 Int)
67
(declare-var constant_test.Mux2_1_1 Bool)
68
(declare-var constant_test.Mux2_1_2 Bool)
69
(declare-var constant_test.Mux3_1_1 Real)
70
(declare-var constant_test.Mux3_1_2 Real)
71
(declare-var constant_test.Mux3_1_3 Real)
72
(declare-var constant_test.Mux3_1_4 Real)
73
(declare-var constant_test.Mux4_1_1 Int)
74
(declare-var constant_test.Mux4_1_2 Int)
75
(declare-var constant_test.Mux4_1_3 Int)
76
(declare-var constant_test.Mux4_1_4 Int)
77
(declare-var constant_test.Mux5_1_1 Bool)
78
(declare-var constant_test.Mux5_1_2 Bool)
79
(declare-var constant_test.Mux5_1_3 Bool)
80
(declare-var constant_test.Mux5_1_4 Bool)
81
(declare-var constant_test.Mux_1_1 Real)
82
(declare-var constant_test.Mux_1_2 Real)
83
(declare-var constant_test.__constant_test_1 Bool)
84
(declare-var constant_test.i_virtual_local Real)
85
(declare-rel constant_test_reset (Bool Bool))
86
(declare-rel constant_test_step (Real Int Bool Real Int Bool Real Real Int Int Bool Bool Real Real Real Real Int Int Int Int Bool Bool Bool Bool Real Real Real Real Int Int Int Int Bool Bool Bool Bool Bool Bool))
87

    
88
(rule (=> 
89
  (and 
90
       
91
       (= constant_test.ni_0._arrow._first_m true)
92
  )
93
  (constant_test_reset constant_test.ni_0._arrow._first_c
94
                       constant_test.ni_0._arrow._first_m)
95
))
96

    
97
(rule (=> 
98
  (and (= constant_test.ni_0._arrow._first_m constant_test.ni_0._arrow._first_c)
99
       (and (= constant_test.__constant_test_1 (ite constant_test.ni_0._arrow._first_m true false))
100
            (= constant_test.ni_0._arrow._first_x false))
101
       (and (or (not (= constant_test.__constant_test_1 true))
102
               (= constant_test.i_virtual_local 0.0))
103
            (or (not (= constant_test.__constant_test_1 false))
104
               (= constant_test.i_virtual_local 1.0))
105
       )
106
       (= constant_test.Constant8_1_4 true)
107
       (= constant_test.Out9_9_4 constant_test.Constant8_1_4)
108
       (= constant_test.Constant8_1_3 true)
109
       (= constant_test.Out9_9_3 constant_test.Constant8_1_3)
110
       (= constant_test.Constant8_1_2 true)
111
       (= constant_test.Out9_9_2 constant_test.Constant8_1_2)
112
       (= constant_test.Constant8_1_1 true)
113
       (= constant_test.Out9_9_1 constant_test.Constant8_1_1)
114
       (= constant_test.Constant7_1_4 5)
115
       (= constant_test.Out8_8_4 constant_test.Constant7_1_4)
116
       (= constant_test.Constant7_1_3 4)
117
       (= constant_test.Out8_8_3 constant_test.Constant7_1_3)
118
       (= constant_test.Constant7_1_2 3)
119
       (= constant_test.Out8_8_2 constant_test.Constant7_1_2)
120
       (= constant_test.Constant7_1_1 2)
121
       (= constant_test.Out8_8_1 constant_test.Constant7_1_1)
122
       (= constant_test.Constant6_1_4 5.00000000)
123
       (= constant_test.Out7_7_4 constant_test.Constant6_1_4)
124
       (= constant_test.Constant6_1_3 4.00000000)
125
       (= constant_test.Out7_7_3 constant_test.Constant6_1_3)
126
       (= constant_test.Constant6_1_2 3.00000000)
127
       (= constant_test.Out7_7_2 constant_test.Constant6_1_2)
128
       (= constant_test.Constant6_1_1 2.00000000)
129
       (= constant_test.Out7_7_1 constant_test.Constant6_1_1)
130
       (= constant_test.Constant5_1_3 true)
131
       (= constant_test.Mux5_1_4 constant_test.Constant5_1_3)
132
       (= constant_test.Out6_6_4 constant_test.Mux5_1_4)
133
       (= constant_test.Constant5_1_2 true)
134
       (= constant_test.Mux5_1_3 constant_test.Constant5_1_2)
135
       (= constant_test.Out6_6_3 constant_test.Mux5_1_3)
136
       (= constant_test.Constant5_1_1 true)
137
       (= constant_test.Mux5_1_2 constant_test.Constant5_1_1)
138
       (= constant_test.Out6_6_2 constant_test.Mux5_1_2)
139
       (= constant_test.Mux5_1_1 constant_test.In6_1_1)
140
       (= constant_test.Out6_6_1 constant_test.Mux5_1_1)
141
       (= constant_test.Constant4_1_3 5)
142
       (= constant_test.Mux4_1_4 constant_test.Constant4_1_3)
143
       (= constant_test.Out5_5_4 constant_test.Mux4_1_4)
144
       (= constant_test.Constant4_1_2 3)
145
       (= constant_test.Mux4_1_3 constant_test.Constant4_1_2)
146
       (= constant_test.Out5_5_3 constant_test.Mux4_1_3)
147
       (= constant_test.Constant4_1_1 2)
148
       (= constant_test.Mux4_1_2 constant_test.Constant4_1_1)
149
       (= constant_test.Out5_5_2 constant_test.Mux4_1_2)
150
       (= constant_test.Mux4_1_1 constant_test.In5_1_1)
151
       (= constant_test.Out5_5_1 constant_test.Mux4_1_1)
152
       (= constant_test.Constant3_1_3 5.00000000)
153
       (= constant_test.Mux3_1_4 constant_test.Constant3_1_3)
154
       (= constant_test.Out4_4_4 constant_test.Mux3_1_4)
155
       (= constant_test.Constant3_1_2 3.00000000)
156
       (= constant_test.Mux3_1_3 constant_test.Constant3_1_2)
157
       (= constant_test.Out4_4_3 constant_test.Mux3_1_3)
158
       (= constant_test.Constant3_1_1 2.00000000)
159
       (= constant_test.Mux3_1_2 constant_test.Constant3_1_1)
160
       (= constant_test.Out4_4_2 constant_test.Mux3_1_2)
161
       (= constant_test.Mux3_1_1 constant_test.In4_1_1)
162
       (= constant_test.Out4_4_1 constant_test.Mux3_1_1)
163
       (= constant_test.Constant2_1_1 true)
164
       (= constant_test.Mux2_1_2 constant_test.Constant2_1_1)
165
       (= constant_test.Out3_3_2 constant_test.Mux2_1_2)
166
       (= constant_test.Mux2_1_1 constant_test.In3_1_1)
167
       (= constant_test.Out3_3_1 constant_test.Mux2_1_1)
168
       (= constant_test.Constant1_1_1 1)
169
       (= constant_test.Mux1_1_2 constant_test.Constant1_1_1)
170
       (= constant_test.Out2_2_2 constant_test.Mux1_1_2)
171
       (= constant_test.Mux1_1_1 constant_test.In2_1_1)
172
       (= constant_test.Out2_2_1 constant_test.Mux1_1_1)
173
       (= constant_test.Constant_1_1 1.00000000)
174
       (= constant_test.Mux_1_2 constant_test.Constant_1_1)
175
       (= constant_test.Out1_1_2 constant_test.Mux_1_2)
176
       (= constant_test.Mux_1_1 constant_test.In1_1_1)
177
       (= constant_test.Out1_1_1 constant_test.Mux_1_1)
178
       )
179
  (constant_test_step constant_test.In1_1_1
180
                      constant_test.In2_1_1
181
                      constant_test.In3_1_1
182
                      constant_test.In4_1_1
183
                      constant_test.In5_1_1
184
                      constant_test.In6_1_1
185
                      constant_test.Out1_1_1
186
                      constant_test.Out1_1_2
187
                      constant_test.Out2_2_1
188
                      constant_test.Out2_2_2
189
                      constant_test.Out3_3_1
190
                      constant_test.Out3_3_2
191
                      constant_test.Out4_4_1
192
                      constant_test.Out4_4_2
193
                      constant_test.Out4_4_3
194
                      constant_test.Out4_4_4
195
                      constant_test.Out5_5_1
196
                      constant_test.Out5_5_2
197
                      constant_test.Out5_5_3
198
                      constant_test.Out5_5_4
199
                      constant_test.Out6_6_1
200
                      constant_test.Out6_6_2
201
                      constant_test.Out6_6_3
202
                      constant_test.Out6_6_4
203
                      constant_test.Out7_7_1
204
                      constant_test.Out7_7_2
205
                      constant_test.Out7_7_3
206
                      constant_test.Out7_7_4
207
                      constant_test.Out8_8_1
208
                      constant_test.Out8_8_2
209
                      constant_test.Out8_8_3
210
                      constant_test.Out8_8_4
211
                      constant_test.Out9_9_1
212
                      constant_test.Out9_9_2
213
                      constant_test.Out9_9_3
214
                      constant_test.Out9_9_4
215
                      constant_test.ni_0._arrow._first_c
216
                      constant_test.ni_0._arrow._first_x)
217
))
218