Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_sum_collapse_test / sum_collapse_test.smt2 @ 6c3ea955

History | View | Annotate | Download (8.84 KB)

1
; sum_collapse_test
2
(declare-var sum_collapse_test.In1_1_1 Real)
3
(declare-var sum_collapse_test.In2_1_1 Real)
4
(declare-var sum_collapse_test.In3_1_1 Real)
5
(declare-var sum_collapse_test.In3_1_2 Real)
6
(declare-var sum_collapse_test.In3_1_3 Real)
7
(declare-var sum_collapse_test.In4_1_1 Real)
8
(declare-var sum_collapse_test.In4_1_2 Real)
9
(declare-var sum_collapse_test.In4_1_3 Real)
10
(declare-var sum_collapse_test.In5_1_1 Real)
11
(declare-var sum_collapse_test.In5_1_2 Real)
12
(declare-var sum_collapse_test.In5_1_3 Real)
13
(declare-var sum_collapse_test.In5_1_4 Real)
14
(declare-var sum_collapse_test.In5_1_5 Real)
15
(declare-var sum_collapse_test.In5_1_6 Real)
16
(declare-var sum_collapse_test.In6_1_1 Real)
17
(declare-var sum_collapse_test.In6_1_2 Real)
18
(declare-var sum_collapse_test.In6_1_3 Real)
19
(declare-var sum_collapse_test.In6_1_4 Real)
20
(declare-var sum_collapse_test.In6_1_5 Real)
21
(declare-var sum_collapse_test.In6_1_6 Real)
22
(declare-var sum_collapse_test.In7_1_1 Real)
23
(declare-var sum_collapse_test.In7_1_2 Real)
24
(declare-var sum_collapse_test.In7_1_3 Real)
25
(declare-var sum_collapse_test.In7_1_4 Real)
26
(declare-var sum_collapse_test.In7_1_5 Real)
27
(declare-var sum_collapse_test.In7_1_6 Real)
28
(declare-var sum_collapse_test.In8_1_1 Real)
29
(declare-var sum_collapse_test.In8_1_2 Real)
30
(declare-var sum_collapse_test.In8_1_3 Real)
31
(declare-var sum_collapse_test.In8_1_4 Real)
32
(declare-var sum_collapse_test.In8_1_5 Real)
33
(declare-var sum_collapse_test.In8_1_6 Real)
34
(declare-var sum_collapse_test.Out1_1_1 Real)
35
(declare-var sum_collapse_test.Out2_2_1 Real)
36
(declare-var sum_collapse_test.Out3_3_1 Real)
37
(declare-var sum_collapse_test.Out4_4_1 Real)
38
(declare-var sum_collapse_test.Out5_5_1 Real)
39
(declare-var sum_collapse_test.Out5_5_2 Real)
40
(declare-var sum_collapse_test.Out5_5_3 Real)
41
(declare-var sum_collapse_test.Out6_6_1 Real)
42
(declare-var sum_collapse_test.Out6_6_2 Real)
43
(declare-var sum_collapse_test.Out6_6_3 Real)
44
(declare-var sum_collapse_test.Out7_7_1 Real)
45
(declare-var sum_collapse_test.Out7_7_2 Real)
46
(declare-var sum_collapse_test.Out8_8_1 Real)
47
(declare-var sum_collapse_test.Out8_8_2 Real)
48
(declare-var sum_collapse_test.ni_0._arrow._first_c Bool)
49
(declare-var sum_collapse_test.ni_0._arrow._first_m Bool)
50
(declare-var sum_collapse_test.ni_0._arrow._first_x Bool)
51
(declare-var sum_collapse_test.Sum1_1_1 Real)
52
(declare-var sum_collapse_test.Sum2_1_1 Real)
53
(declare-var sum_collapse_test.Sum3_1_1 Real)
54
(declare-var sum_collapse_test.Sum4_1_1 Real)
55
(declare-var sum_collapse_test.Sum4_1_2 Real)
56
(declare-var sum_collapse_test.Sum4_1_3 Real)
57
(declare-var sum_collapse_test.Sum5_1_1 Real)
58
(declare-var sum_collapse_test.Sum5_1_2 Real)
59
(declare-var sum_collapse_test.Sum5_1_3 Real)
60
(declare-var sum_collapse_test.Sum6_1_1 Real)
61
(declare-var sum_collapse_test.Sum6_1_2 Real)
62
(declare-var sum_collapse_test.Sum7_1_1 Real)
63
(declare-var sum_collapse_test.Sum7_1_2 Real)
64
(declare-var sum_collapse_test.Sum_1_1 Real)
65
(declare-var sum_collapse_test.__sum_collapse_test_1 Bool)
66
(declare-var sum_collapse_test.i_virtual_local Real)
67
(declare-rel sum_collapse_test_reset (Bool Bool))
68
(declare-rel sum_collapse_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))
69

    
70
(rule (=> 
71
  (and 
72
       
73
       (= sum_collapse_test.ni_0._arrow._first_m true)
74
  )
75
  (sum_collapse_test_reset sum_collapse_test.ni_0._arrow._first_c
76
                           sum_collapse_test.ni_0._arrow._first_m)
77
))
78

    
79
(rule (=> 
80
  (and (= sum_collapse_test.ni_0._arrow._first_m sum_collapse_test.ni_0._arrow._first_c)
81
       (and (= sum_collapse_test.__sum_collapse_test_1 (ite sum_collapse_test.ni_0._arrow._first_m true false))
82
            (= sum_collapse_test.ni_0._arrow._first_x false))
83
       (and (or (not (= sum_collapse_test.__sum_collapse_test_1 true))
84
               (= sum_collapse_test.i_virtual_local 0.0))
85
            (or (not (= sum_collapse_test.__sum_collapse_test_1 false))
86
               (= sum_collapse_test.i_virtual_local 1.0))
87
       )
88
       (= sum_collapse_test.Sum_1_1 sum_collapse_test.In1_1_1)
89
       (= sum_collapse_test.Sum7_1_2 (- (- (- sum_collapse_test.In8_1_4) sum_collapse_test.In8_1_5) sum_collapse_test.In8_1_6))
90
       (= sum_collapse_test.Sum7_1_1 (- (- (- sum_collapse_test.In8_1_1) sum_collapse_test.In8_1_2) sum_collapse_test.In8_1_3))
91
       (= sum_collapse_test.Sum6_1_2 (+ (+ sum_collapse_test.In7_1_4 sum_collapse_test.In7_1_5) sum_collapse_test.In7_1_6))
92
       (= sum_collapse_test.Sum6_1_1 (+ (+ sum_collapse_test.In7_1_1 sum_collapse_test.In7_1_2) sum_collapse_test.In7_1_3))
93
       (= sum_collapse_test.Sum5_1_3 (- (- sum_collapse_test.In6_1_3) sum_collapse_test.In6_1_6))
94
       (= sum_collapse_test.Sum5_1_2 (- (- sum_collapse_test.In6_1_2) sum_collapse_test.In6_1_5))
95
       (= sum_collapse_test.Sum5_1_1 (- (- sum_collapse_test.In6_1_1) sum_collapse_test.In6_1_4))
96
       (= sum_collapse_test.Sum4_1_3 (+ sum_collapse_test.In5_1_3 sum_collapse_test.In5_1_6))
97
       (= sum_collapse_test.Sum4_1_2 (+ sum_collapse_test.In5_1_2 sum_collapse_test.In5_1_5))
98
       (= sum_collapse_test.Sum4_1_1 (+ sum_collapse_test.In5_1_1 sum_collapse_test.In5_1_4))
99
       (= sum_collapse_test.Sum3_1_1 (- (- (- sum_collapse_test.In4_1_1) sum_collapse_test.In4_1_2) sum_collapse_test.In4_1_3))
100
       (= sum_collapse_test.Sum2_1_1 (+ (+ sum_collapse_test.In3_1_1 sum_collapse_test.In3_1_2) sum_collapse_test.In3_1_3))
101
       (= sum_collapse_test.Sum1_1_1 (- sum_collapse_test.In2_1_1))
102
       (= sum_collapse_test.Out8_8_2 sum_collapse_test.Sum7_1_2)
103
       (= sum_collapse_test.Out8_8_1 sum_collapse_test.Sum7_1_1)
104
       (= sum_collapse_test.Out7_7_2 sum_collapse_test.Sum6_1_2)
105
       (= sum_collapse_test.Out7_7_1 sum_collapse_test.Sum6_1_1)
106
       (= sum_collapse_test.Out6_6_3 sum_collapse_test.Sum5_1_3)
107
       (= sum_collapse_test.Out6_6_2 sum_collapse_test.Sum5_1_2)
108
       (= sum_collapse_test.Out6_6_1 sum_collapse_test.Sum5_1_1)
109
       (= sum_collapse_test.Out5_5_3 sum_collapse_test.Sum4_1_3)
110
       (= sum_collapse_test.Out5_5_2 sum_collapse_test.Sum4_1_2)
111
       (= sum_collapse_test.Out5_5_1 sum_collapse_test.Sum4_1_1)
112
       (= sum_collapse_test.Out4_4_1 sum_collapse_test.Sum3_1_1)
113
       (= sum_collapse_test.Out3_3_1 sum_collapse_test.Sum2_1_1)
114
       (= sum_collapse_test.Out2_2_1 sum_collapse_test.Sum1_1_1)
115
       (= sum_collapse_test.Out1_1_1 sum_collapse_test.Sum_1_1)
116
       )
117
  (sum_collapse_test_step sum_collapse_test.In1_1_1
118
                          sum_collapse_test.In2_1_1
119
                          sum_collapse_test.In3_1_1
120
                          sum_collapse_test.In3_1_2
121
                          sum_collapse_test.In3_1_3
122
                          sum_collapse_test.In4_1_1
123
                          sum_collapse_test.In4_1_2
124
                          sum_collapse_test.In4_1_3
125
                          sum_collapse_test.In5_1_1
126
                          sum_collapse_test.In5_1_2
127
                          sum_collapse_test.In5_1_3
128
                          sum_collapse_test.In5_1_4
129
                          sum_collapse_test.In5_1_5
130
                          sum_collapse_test.In5_1_6
131
                          sum_collapse_test.In6_1_1
132
                          sum_collapse_test.In6_1_2
133
                          sum_collapse_test.In6_1_3
134
                          sum_collapse_test.In6_1_4
135
                          sum_collapse_test.In6_1_5
136
                          sum_collapse_test.In6_1_6
137
                          sum_collapse_test.In7_1_1
138
                          sum_collapse_test.In7_1_2
139
                          sum_collapse_test.In7_1_3
140
                          sum_collapse_test.In7_1_4
141
                          sum_collapse_test.In7_1_5
142
                          sum_collapse_test.In7_1_6
143
                          sum_collapse_test.In8_1_1
144
                          sum_collapse_test.In8_1_2
145
                          sum_collapse_test.In8_1_3
146
                          sum_collapse_test.In8_1_4
147
                          sum_collapse_test.In8_1_5
148
                          sum_collapse_test.In8_1_6
149
                          sum_collapse_test.Out1_1_1
150
                          sum_collapse_test.Out2_2_1
151
                          sum_collapse_test.Out3_3_1
152
                          sum_collapse_test.Out4_4_1
153
                          sum_collapse_test.Out5_5_1
154
                          sum_collapse_test.Out5_5_2
155
                          sum_collapse_test.Out5_5_3
156
                          sum_collapse_test.Out6_6_1
157
                          sum_collapse_test.Out6_6_2
158
                          sum_collapse_test.Out6_6_3
159
                          sum_collapse_test.Out7_7_1
160
                          sum_collapse_test.Out7_7_2
161
                          sum_collapse_test.Out8_8_1
162
                          sum_collapse_test.Out8_8_2
163
                          sum_collapse_test.ni_0._arrow._first_c
164
                          sum_collapse_test.ni_0._arrow._first_x)
165
))
166