Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_flattening_3_test / flattening_3_test.smt2 @ 6c3ea955

History | View | Annotate | Download (10.2 KB)

1
; flattening_3_test_Atomic
2
(declare-var flattening_3_test_Atomic.In1_1_1 Real)
3
(declare-var flattening_3_test_Atomic.Out1_1_1 Real)
4
(declare-var flattening_3_test_Atomic.__flattening_3_test_Atomic_2_c Real)
5
(declare-var flattening_3_test_Atomic.ni_2._arrow._first_c Bool)
6
(declare-var flattening_3_test_Atomic.__flattening_3_test_Atomic_2_m Real)
7
(declare-var flattening_3_test_Atomic.ni_2._arrow._first_m Bool)
8
(declare-var flattening_3_test_Atomic.__flattening_3_test_Atomic_2_x Real)
9
(declare-var flattening_3_test_Atomic.ni_2._arrow._first_x Bool)
10
(declare-var flattening_3_test_Atomic.UnitDelay_1_1 Real)
11
(declare-var flattening_3_test_Atomic.__flattening_3_test_Atomic_1 Bool)
12
(declare-rel flattening_3_test_Atomic_reset (Real Bool Real Bool))
13
(declare-rel flattening_3_test_Atomic_step (Real Real Real Bool Real Bool))
14

    
15
(rule (=> 
16
  (and 
17
       (= flattening_3_test_Atomic.__flattening_3_test_Atomic_2_m flattening_3_test_Atomic.__flattening_3_test_Atomic_2_c)
18
       (= flattening_3_test_Atomic.ni_2._arrow._first_m true)
19
  )
20
  (flattening_3_test_Atomic_reset flattening_3_test_Atomic.__flattening_3_test_Atomic_2_c
21
                                  flattening_3_test_Atomic.ni_2._arrow._first_c
22
                                  flattening_3_test_Atomic.__flattening_3_test_Atomic_2_m
23
                                  flattening_3_test_Atomic.ni_2._arrow._first_m)
24
))
25

    
26
(rule (=> 
27
  (and (= flattening_3_test_Atomic.ni_2._arrow._first_m flattening_3_test_Atomic.ni_2._arrow._first_c)
28
       (and (= flattening_3_test_Atomic.__flattening_3_test_Atomic_1 (ite flattening_3_test_Atomic.ni_2._arrow._first_m true false))
29
            (= flattening_3_test_Atomic.ni_2._arrow._first_x false))
30
       (and (or (not (= flattening_3_test_Atomic.__flattening_3_test_Atomic_1 true))
31
               (= flattening_3_test_Atomic.UnitDelay_1_1 0.00000000))
32
            (or (not (= flattening_3_test_Atomic.__flattening_3_test_Atomic_1 false))
33
               (= flattening_3_test_Atomic.UnitDelay_1_1 flattening_3_test_Atomic.__flattening_3_test_Atomic_2_c))
34
       )
35
       (= flattening_3_test_Atomic.__flattening_3_test_Atomic_2_x flattening_3_test_Atomic.In1_1_1)
36
       (= flattening_3_test_Atomic.Out1_1_1 flattening_3_test_Atomic.UnitDelay_1_1)
37
       )
38
  (flattening_3_test_Atomic_step flattening_3_test_Atomic.In1_1_1
39
                                 flattening_3_test_Atomic.Out1_1_1
40
                                 flattening_3_test_Atomic.__flattening_3_test_Atomic_2_c
41
                                 flattening_3_test_Atomic.ni_2._arrow._first_c
42
                                 flattening_3_test_Atomic.__flattening_3_test_Atomic_2_x
43
                                 flattening_3_test_Atomic.ni_2._arrow._first_x)
44
))
45

    
46
; flattening_3_test_SubVirtual_SubAtomic
47
(declare-var flattening_3_test_SubVirtual_SubAtomic.SubIn1_1_1 Real)
48
(declare-var flattening_3_test_SubVirtual_SubAtomic.SubOut1_1_1 Real)
49
(declare-var flattening_3_test_SubVirtual_SubAtomic.SubOut2_2_1 Real)
50
(declare-var flattening_3_test_SubVirtual_SubAtomic.Product_1_1 Real)
51
(declare-var flattening_3_test_SubVirtual_SubAtomic.SubSubVirtua2_Product2_1_1 Real)
52
(declare-var flattening_3_test_SubVirtual_SubAtomic.SubSubVirtual1_Product2_1_1 Real)
53
(declare-var flattening_3_test_SubVirtual_SubAtomic.SubSubVirtual3_Product2_1_1 Real)
54
(declare-var flattening_3_test_SubVirtual_SubAtomic.SubSubVirtual_Product2_1_1 Real)
55
(declare-rel flattening_3_test_SubVirtual_SubAtomic (Real Real Real))
56
(rule (=> 
57
  (and (= flattening_3_test_SubVirtual_SubAtomic.SubSubVirtual1_Product2_1_1 (* flattening_3_test_SubVirtual_SubAtomic.SubIn1_1_1 flattening_3_test_SubVirtual_SubAtomic.SubIn1_1_1))
58
       (= flattening_3_test_SubVirtual_SubAtomic.Product_1_1 (* flattening_3_test_SubVirtual_SubAtomic.SubIn1_1_1 flattening_3_test_SubVirtual_SubAtomic.SubIn1_1_1))
59
       (= flattening_3_test_SubVirtual_SubAtomic.SubSubVirtual_Product2_1_1 (* flattening_3_test_SubVirtual_SubAtomic.Product_1_1 flattening_3_test_SubVirtual_SubAtomic.SubSubVirtual1_Product2_1_1))
60
       (= flattening_3_test_SubVirtual_SubAtomic.SubSubVirtual3_Product2_1_1 (* (* flattening_3_test_SubVirtual_SubAtomic.SubSubVirtual_Product2_1_1 flattening_3_test_SubVirtual_SubAtomic.SubSubVirtual_Product2_1_1) flattening_3_test_SubVirtual_SubAtomic.SubSubVirtual_Product2_1_1))
61
       (= flattening_3_test_SubVirtual_SubAtomic.SubSubVirtua2_Product2_1_1 (* (* flattening_3_test_SubVirtual_SubAtomic.SubSubVirtual_Product2_1_1 flattening_3_test_SubVirtual_SubAtomic.SubSubVirtual_Product2_1_1) flattening_3_test_SubVirtual_SubAtomic.SubSubVirtual_Product2_1_1))
62
       (= flattening_3_test_SubVirtual_SubAtomic.SubOut2_2_1 flattening_3_test_SubVirtual_SubAtomic.SubSubVirtual3_Product2_1_1)
63
       (= flattening_3_test_SubVirtual_SubAtomic.SubOut1_1_1 flattening_3_test_SubVirtual_SubAtomic.SubSubVirtua2_Product2_1_1)
64
       )
65
  (flattening_3_test_SubVirtual_SubAtomic flattening_3_test_SubVirtual_SubAtomic.SubIn1_1_1 flattening_3_test_SubVirtual_SubAtomic.SubOut1_1_1 flattening_3_test_SubVirtual_SubAtomic.SubOut2_2_1)
66
))
67

    
68
; flattening_3_test
69
(declare-var flattening_3_test.In1_1_1 Real)
70
(declare-var flattening_3_test.In2_1_1 Real)
71
(declare-var flattening_3_test.Out1_1_1 Real)
72
(declare-var flattening_3_test.Out2_2_1 Real)
73
(declare-var flattening_3_test.Out3_3_1 Real)
74
(declare-var flattening_3_test.ni_0.flattening_3_test_Atomic.__flattening_3_test_Atomic_2_c Real)
75
(declare-var flattening_3_test.ni_0.flattening_3_test_Atomic.ni_2._arrow._first_c Bool)
76
(declare-var flattening_3_test.ni_1._arrow._first_c Bool)
77
(declare-var flattening_3_test.ni_0.flattening_3_test_Atomic.__flattening_3_test_Atomic_2_m Real)
78
(declare-var flattening_3_test.ni_0.flattening_3_test_Atomic.ni_2._arrow._first_m Bool)
79
(declare-var flattening_3_test.ni_1._arrow._first_m Bool)
80
(declare-var flattening_3_test.ni_0.flattening_3_test_Atomic.__flattening_3_test_Atomic_2_x Real)
81
(declare-var flattening_3_test.ni_0.flattening_3_test_Atomic.ni_2._arrow._first_x Bool)
82
(declare-var flattening_3_test.ni_1._arrow._first_x Bool)
83
(declare-var flattening_3_test.Atomic_1_1 Real)
84
(declare-var flattening_3_test.SubVirtual_SubAtomic_1_1 Real)
85
(declare-var flattening_3_test.SubVirtual_SubAtomic_2_1 Real)
86
(declare-var flattening_3_test.SubVirtual_Sum_1_1 Real)
87
(declare-var flattening_3_test.__flattening_3_test_1 Bool)
88
(declare-var flattening_3_test.i_virtual_local Real)
89
(declare-rel flattening_3_test_reset (Real Bool Bool Real Bool Bool))
90
(declare-rel flattening_3_test_step (Real Real Real Real Real Real Bool Bool Real Bool Bool))
91

    
92
(rule (=> 
93
  (and 
94
       
95
       (= flattening_3_test.ni_1._arrow._first_m true)
96
       (flattening_3_test_Atomic_reset flattening_3_test.ni_0.flattening_3_test_Atomic.__flattening_3_test_Atomic_2_c
97
                                       flattening_3_test.ni_0.flattening_3_test_Atomic.ni_2._arrow._first_c
98
                                       flattening_3_test.ni_0.flattening_3_test_Atomic.__flattening_3_test_Atomic_2_m
99
                                       flattening_3_test.ni_0.flattening_3_test_Atomic.ni_2._arrow._first_m)
100
  )
101
  (flattening_3_test_reset flattening_3_test.ni_0.flattening_3_test_Atomic.__flattening_3_test_Atomic_2_c
102
                           flattening_3_test.ni_0.flattening_3_test_Atomic.ni_2._arrow._first_c
103
                           flattening_3_test.ni_1._arrow._first_c
104
                           flattening_3_test.ni_0.flattening_3_test_Atomic.__flattening_3_test_Atomic_2_m
105
                           flattening_3_test.ni_0.flattening_3_test_Atomic.ni_2._arrow._first_m
106
                           flattening_3_test.ni_1._arrow._first_m)
107
))
108

    
109
(rule (=> 
110
  (and (= flattening_3_test.ni_1._arrow._first_m flattening_3_test.ni_1._arrow._first_c)
111
       (and (= flattening_3_test.__flattening_3_test_1 (ite flattening_3_test.ni_1._arrow._first_m true false))
112
            (= flattening_3_test.ni_1._arrow._first_x false))
113
       (and (or (not (= flattening_3_test.__flattening_3_test_1 true))
114
               (= flattening_3_test.i_virtual_local 0.0))
115
            (or (not (= flattening_3_test.__flattening_3_test_1 false))
116
               (= flattening_3_test.i_virtual_local 1.0))
117
       )
118
       (= flattening_3_test.SubVirtual_Sum_1_1 (+ flattening_3_test.In1_1_1 flattening_3_test.In1_1_1))
119
       (flattening_3_test_SubVirtual_SubAtomic flattening_3_test.SubVirtual_Sum_1_1
120
                                               flattening_3_test.SubVirtual_SubAtomic_1_1
121
                                               flattening_3_test.SubVirtual_SubAtomic_2_1)
122
       (= flattening_3_test.Out3_3_1 flattening_3_test.SubVirtual_SubAtomic_2_1)
123
       (and (= flattening_3_test.ni_0.flattening_3_test_Atomic.__flattening_3_test_Atomic_2_m flattening_3_test.ni_0.flattening_3_test_Atomic.__flattening_3_test_Atomic_2_c)
124
            (= flattening_3_test.ni_0.flattening_3_test_Atomic.ni_2._arrow._first_m flattening_3_test.ni_0.flattening_3_test_Atomic.ni_2._arrow._first_c)
125
            )
126
       (flattening_3_test_Atomic_step flattening_3_test.In2_1_1
127
                                      flattening_3_test.Atomic_1_1
128
                                      flattening_3_test.ni_0.flattening_3_test_Atomic.__flattening_3_test_Atomic_2_m
129
                                      flattening_3_test.ni_0.flattening_3_test_Atomic.ni_2._arrow._first_m
130
                                      flattening_3_test.ni_0.flattening_3_test_Atomic.__flattening_3_test_Atomic_2_x
131
                                      flattening_3_test.ni_0.flattening_3_test_Atomic.ni_2._arrow._first_x)
132
       (= flattening_3_test.Out2_2_1 flattening_3_test.Atomic_1_1)
133
       (= flattening_3_test.Out1_1_1 flattening_3_test.SubVirtual_SubAtomic_1_1)
134
       )
135
  (flattening_3_test_step flattening_3_test.In1_1_1
136
                          flattening_3_test.In2_1_1
137
                          flattening_3_test.Out1_1_1
138
                          flattening_3_test.Out2_2_1
139
                          flattening_3_test.Out3_3_1
140
                          flattening_3_test.ni_0.flattening_3_test_Atomic.__flattening_3_test_Atomic_2_c
141
                          flattening_3_test.ni_0.flattening_3_test_Atomic.ni_2._arrow._first_c
142
                          flattening_3_test.ni_1._arrow._first_c
143
                          flattening_3_test.ni_0.flattening_3_test_Atomic.__flattening_3_test_Atomic_2_x
144
                          flattening_3_test.ni_0.flattening_3_test_Atomic.ni_2._arrow._first_x
145
                          flattening_3_test.ni_1._arrow._first_x)
146
))
147