Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_abs_test / abs_test.smt2 @ 6c3ea955

History | View | Annotate | Download (7.64 KB)

1
; abs_test
2
(declare-var abs_test.In1_1_1 Real)
3
(declare-var abs_test.In2_1_1 Int)
4
(declare-var abs_test.In2_1_2 Int)
5
(declare-var abs_test.In2_1_3 Int)
6
(declare-var abs_test.In3_1_1 Real)
7
(declare-var abs_test.In3_1_2 Real)
8
(declare-var abs_test.In3_1_3 Real)
9
(declare-var abs_test.In3_1_4 Real)
10
(declare-var abs_test.In3_1_5 Real)
11
(declare-var abs_test.In3_1_6 Real)
12
(declare-var abs_test.In3_1_7 Real)
13
(declare-var abs_test.In3_1_8 Real)
14
(declare-var abs_test.Out1_1_1 Real)
15
(declare-var abs_test.Out2_2_1 Int)
16
(declare-var abs_test.Out2_2_2 Int)
17
(declare-var abs_test.Out2_2_3 Int)
18
(declare-var abs_test.Out3_3_1 Real)
19
(declare-var abs_test.Out3_3_2 Real)
20
(declare-var abs_test.Out3_3_3 Real)
21
(declare-var abs_test.Out3_3_4 Real)
22
(declare-var abs_test.Out3_3_5 Real)
23
(declare-var abs_test.Out3_3_6 Real)
24
(declare-var abs_test.Out3_3_7 Real)
25
(declare-var abs_test.Out3_3_8 Real)
26
(declare-var abs_test.ni_0._arrow._first_c Bool)
27
(declare-var abs_test.ni_0._arrow._first_m Bool)
28
(declare-var abs_test.ni_0._arrow._first_x Bool)
29
(declare-var abs_test.Abs1_1_1 Int)
30
(declare-var abs_test.Abs1_1_2 Int)
31
(declare-var abs_test.Abs1_1_3 Int)
32
(declare-var abs_test.Abs2_1_1 Real)
33
(declare-var abs_test.Abs2_1_2 Real)
34
(declare-var abs_test.Abs2_1_3 Real)
35
(declare-var abs_test.Abs2_1_4 Real)
36
(declare-var abs_test.Abs2_1_5 Real)
37
(declare-var abs_test.Abs2_1_6 Real)
38
(declare-var abs_test.Abs2_1_7 Real)
39
(declare-var abs_test.Abs2_1_8 Real)
40
(declare-var abs_test.Abs_1_1 Real)
41
(declare-var abs_test.__abs_test_1 Bool)
42
(declare-var abs_test.__abs_test_10 Bool)
43
(declare-var abs_test.__abs_test_11 Bool)
44
(declare-var abs_test.__abs_test_12 Bool)
45
(declare-var abs_test.__abs_test_13 Bool)
46
(declare-var abs_test.__abs_test_2 Bool)
47
(declare-var abs_test.__abs_test_3 Bool)
48
(declare-var abs_test.__abs_test_4 Bool)
49
(declare-var abs_test.__abs_test_5 Bool)
50
(declare-var abs_test.__abs_test_6 Bool)
51
(declare-var abs_test.__abs_test_7 Bool)
52
(declare-var abs_test.__abs_test_8 Bool)
53
(declare-var abs_test.__abs_test_9 Bool)
54
(declare-var abs_test.i_virtual_local Real)
55
(declare-rel abs_test_reset (Bool Bool))
56
(declare-rel abs_test_step (Real Int Int Int Real Real Real Real Real Real Real Real Real Int Int Int Real Real Real Real Real Real Real Real Bool Bool))
57

    
58
(rule (=> 
59
  (and 
60
       
61
       (= abs_test.ni_0._arrow._first_m true)
62
  )
63
  (abs_test_reset abs_test.ni_0._arrow._first_c
64
                  abs_test.ni_0._arrow._first_m)
65
))
66

    
67
(rule (=> 
68
  (and (= abs_test.ni_0._arrow._first_m abs_test.ni_0._arrow._first_c)
69
       (and (= abs_test.__abs_test_1 (ite abs_test.ni_0._arrow._first_m true false))
70
            (= abs_test.ni_0._arrow._first_x false))
71
       (and (or (not (= abs_test.__abs_test_1 true))
72
               (= abs_test.i_virtual_local 0.0))
73
            (or (not (= abs_test.__abs_test_1 false))
74
               (= abs_test.i_virtual_local 1.0))
75
       )
76
       (= abs_test.__abs_test_9 (>= abs_test.In3_1_1 0.0))
77
       (= abs_test.__abs_test_8 (>= abs_test.In3_1_2 0.0))
78
       (= abs_test.__abs_test_7 (>= abs_test.In3_1_3 0.0))
79
       (= abs_test.__abs_test_6 (>= abs_test.In3_1_4 0.0))
80
       (= abs_test.__abs_test_5 (>= abs_test.In3_1_5 0.0))
81
       (= abs_test.__abs_test_4 (>= abs_test.In3_1_6 0.0))
82
       (= abs_test.__abs_test_3 (>= abs_test.In3_1_7 0.0))
83
       (= abs_test.__abs_test_2 (>= abs_test.In3_1_8 0.0))
84
       (= abs_test.__abs_test_13 (>= abs_test.In1_1_1 0.0))
85
       (= abs_test.__abs_test_12 (>= abs_test.In2_1_1 0))
86
       (= abs_test.__abs_test_11 (>= abs_test.In2_1_2 0))
87
       (= abs_test.__abs_test_10 (>= abs_test.In2_1_3 0))
88
       (and (or (not (= abs_test.__abs_test_2 true))
89
               (= abs_test.Abs2_1_8 abs_test.In3_1_8))
90
            (or (not (= abs_test.__abs_test_2 false))
91
               (= abs_test.Abs2_1_8 (- abs_test.In3_1_8)))
92
       )
93
       (= abs_test.Out3_3_8 abs_test.Abs2_1_8)
94
       (and (or (not (= abs_test.__abs_test_3 true))
95
               (= abs_test.Abs2_1_7 abs_test.In3_1_7))
96
            (or (not (= abs_test.__abs_test_3 false))
97
               (= abs_test.Abs2_1_7 (- abs_test.In3_1_7)))
98
       )
99
       (= abs_test.Out3_3_7 abs_test.Abs2_1_7)
100
       (and (or (not (= abs_test.__abs_test_4 true))
101
               (= abs_test.Abs2_1_6 abs_test.In3_1_6))
102
            (or (not (= abs_test.__abs_test_4 false))
103
               (= abs_test.Abs2_1_6 (- abs_test.In3_1_6)))
104
       )
105
       (= abs_test.Out3_3_6 abs_test.Abs2_1_6)
106
       (and (or (not (= abs_test.__abs_test_5 true))
107
               (= abs_test.Abs2_1_5 abs_test.In3_1_5))
108
            (or (not (= abs_test.__abs_test_5 false))
109
               (= abs_test.Abs2_1_5 (- abs_test.In3_1_5)))
110
       )
111
       (= abs_test.Out3_3_5 abs_test.Abs2_1_5)
112
       (and (or (not (= abs_test.__abs_test_6 true))
113
               (= abs_test.Abs2_1_4 abs_test.In3_1_4))
114
            (or (not (= abs_test.__abs_test_6 false))
115
               (= abs_test.Abs2_1_4 (- abs_test.In3_1_4)))
116
       )
117
       (= abs_test.Out3_3_4 abs_test.Abs2_1_4)
118
       (and (or (not (= abs_test.__abs_test_7 true))
119
               (= abs_test.Abs2_1_3 abs_test.In3_1_3))
120
            (or (not (= abs_test.__abs_test_7 false))
121
               (= abs_test.Abs2_1_3 (- abs_test.In3_1_3)))
122
       )
123
       (= abs_test.Out3_3_3 abs_test.Abs2_1_3)
124
       (and (or (not (= abs_test.__abs_test_8 true))
125
               (= abs_test.Abs2_1_2 abs_test.In3_1_2))
126
            (or (not (= abs_test.__abs_test_8 false))
127
               (= abs_test.Abs2_1_2 (- abs_test.In3_1_2)))
128
       )
129
       (= abs_test.Out3_3_2 abs_test.Abs2_1_2)
130
       (and (or (not (= abs_test.__abs_test_9 true))
131
               (= abs_test.Abs2_1_1 abs_test.In3_1_1))
132
            (or (not (= abs_test.__abs_test_9 false))
133
               (= abs_test.Abs2_1_1 (- abs_test.In3_1_1)))
134
       )
135
       (= abs_test.Out3_3_1 abs_test.Abs2_1_1)
136
       (and (or (not (= abs_test.__abs_test_10 true))
137
               (= abs_test.Abs1_1_3 abs_test.In2_1_3))
138
            (or (not (= abs_test.__abs_test_10 false))
139
               (= abs_test.Abs1_1_3 (- abs_test.In2_1_3)))
140
       )
141
       (= abs_test.Out2_2_3 abs_test.Abs1_1_3)
142
       (and (or (not (= abs_test.__abs_test_11 true))
143
               (= abs_test.Abs1_1_2 abs_test.In2_1_2))
144
            (or (not (= abs_test.__abs_test_11 false))
145
               (= abs_test.Abs1_1_2 (- abs_test.In2_1_2)))
146
       )
147
       (= abs_test.Out2_2_2 abs_test.Abs1_1_2)
148
       (and (or (not (= abs_test.__abs_test_12 true))
149
               (= abs_test.Abs1_1_1 abs_test.In2_1_1))
150
            (or (not (= abs_test.__abs_test_12 false))
151
               (= abs_test.Abs1_1_1 (- abs_test.In2_1_1)))
152
       )
153
       (= abs_test.Out2_2_1 abs_test.Abs1_1_1)
154
       (and (or (not (= abs_test.__abs_test_13 true))
155
               (= abs_test.Abs_1_1 abs_test.In1_1_1))
156
            (or (not (= abs_test.__abs_test_13 false))
157
               (= abs_test.Abs_1_1 (- abs_test.In1_1_1)))
158
       )
159
       (= abs_test.Out1_1_1 abs_test.Abs_1_1)
160
       )
161
  (abs_test_step abs_test.In1_1_1
162
                 abs_test.In2_1_1
163
                 abs_test.In2_1_2
164
                 abs_test.In2_1_3
165
                 abs_test.In3_1_1
166
                 abs_test.In3_1_2
167
                 abs_test.In3_1_3
168
                 abs_test.In3_1_4
169
                 abs_test.In3_1_5
170
                 abs_test.In3_1_6
171
                 abs_test.In3_1_7
172
                 abs_test.In3_1_8
173
                 abs_test.Out1_1_1
174
                 abs_test.Out2_2_1
175
                 abs_test.Out2_2_2
176
                 abs_test.Out2_2_3
177
                 abs_test.Out3_3_1
178
                 abs_test.Out3_3_2
179
                 abs_test.Out3_3_3
180
                 abs_test.Out3_3_4
181
                 abs_test.Out3_3_5
182
                 abs_test.Out3_3_6
183
                 abs_test.Out3_3_7
184
                 abs_test.Out3_3_8
185
                 abs_test.ni_0._arrow._first_c
186
                 abs_test.ni_0._arrow._first_x)
187
))
188