Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_integrator_ext_IC_test / integrator_ext_IC_test.smt2 @ 6c3ea955

History | View | Annotate | Download (8.62 KB)

1
; integrator_ext_IC_test
2
(declare-var integrator_ext_IC_test.In4_1_1 Real)
3
(declare-var integrator_ext_IC_test.In7_1_1 Real)
4
(declare-var integrator_ext_IC_test.In11_1_1 Int)
5
(declare-var integrator_ext_IC_test.In14_1_1 Int)
6
(declare-var integrator_ext_IC_test.In18_1_1 Int)
7
(declare-var integrator_ext_IC_test.In21_1_1 Int)
8
(declare-var integrator_ext_IC_test.Out4_1_1 Real)
9
(declare-var integrator_ext_IC_test.Out8_2_1 Int)
10
(declare-var integrator_ext_IC_test.Out12_3_1 Int)
11
(declare-var integrator_ext_IC_test.__integrator_ext_IC_test_2_c Int)
12
(declare-var integrator_ext_IC_test.__integrator_ext_IC_test_3_c Int)
13
(declare-var integrator_ext_IC_test.__integrator_ext_IC_test_4_c Real)
14
(declare-var integrator_ext_IC_test.__integrator_ext_IC_test_5_c Real)
15
(declare-var integrator_ext_IC_test.__integrator_ext_IC_test_6_c Int)
16
(declare-var integrator_ext_IC_test.__integrator_ext_IC_test_7_c Int)
17
(declare-var integrator_ext_IC_test.ni_0._arrow._first_c Bool)
18
(declare-var integrator_ext_IC_test.__integrator_ext_IC_test_2_m Int)
19
(declare-var integrator_ext_IC_test.__integrator_ext_IC_test_3_m Int)
20
(declare-var integrator_ext_IC_test.__integrator_ext_IC_test_4_m Real)
21
(declare-var integrator_ext_IC_test.__integrator_ext_IC_test_5_m Real)
22
(declare-var integrator_ext_IC_test.__integrator_ext_IC_test_6_m Int)
23
(declare-var integrator_ext_IC_test.__integrator_ext_IC_test_7_m Int)
24
(declare-var integrator_ext_IC_test.ni_0._arrow._first_m Bool)
25
(declare-var integrator_ext_IC_test.__integrator_ext_IC_test_2_x Int)
26
(declare-var integrator_ext_IC_test.__integrator_ext_IC_test_3_x Int)
27
(declare-var integrator_ext_IC_test.__integrator_ext_IC_test_4_x Real)
28
(declare-var integrator_ext_IC_test.__integrator_ext_IC_test_5_x Real)
29
(declare-var integrator_ext_IC_test.__integrator_ext_IC_test_6_x Int)
30
(declare-var integrator_ext_IC_test.__integrator_ext_IC_test_7_x Int)
31
(declare-var integrator_ext_IC_test.ni_0._arrow._first_x Bool)
32
(declare-var integrator_ext_IC_test.Integrator11_1_1 Int)
33
(declare-var integrator_ext_IC_test.Integrator3_1_1 Real)
34
(declare-var integrator_ext_IC_test.Integrator7_1_1 Int)
35
(declare-var integrator_ext_IC_test.__integrator_ext_IC_test_1 Bool)
36
(declare-var integrator_ext_IC_test.i_virtual_local Real)
37
(declare-rel integrator_ext_IC_test_reset (Int Int Real Real Int Int Bool Int Int Real Real Int Int Bool))
38
(declare-rel integrator_ext_IC_test_step (Real Real Int Int Int Int Real Int Int Int Int Real Real Int Int Bool Int Int Real Real Int Int Bool))
39

    
40
(rule (=> 
41
  (and 
42
       (= integrator_ext_IC_test.__integrator_ext_IC_test_2_m integrator_ext_IC_test.__integrator_ext_IC_test_2_c)
43
       (= integrator_ext_IC_test.__integrator_ext_IC_test_3_m integrator_ext_IC_test.__integrator_ext_IC_test_3_c)
44
       (= integrator_ext_IC_test.__integrator_ext_IC_test_4_m integrator_ext_IC_test.__integrator_ext_IC_test_4_c)
45
       (= integrator_ext_IC_test.__integrator_ext_IC_test_5_m integrator_ext_IC_test.__integrator_ext_IC_test_5_c)
46
       (= integrator_ext_IC_test.__integrator_ext_IC_test_6_m integrator_ext_IC_test.__integrator_ext_IC_test_6_c)
47
       (= integrator_ext_IC_test.__integrator_ext_IC_test_7_m integrator_ext_IC_test.__integrator_ext_IC_test_7_c)
48
       (= integrator_ext_IC_test.ni_0._arrow._first_m true)
49
  )
50
  (integrator_ext_IC_test_reset integrator_ext_IC_test.__integrator_ext_IC_test_2_c
51
                                integrator_ext_IC_test.__integrator_ext_IC_test_3_c
52
                                integrator_ext_IC_test.__integrator_ext_IC_test_4_c
53
                                integrator_ext_IC_test.__integrator_ext_IC_test_5_c
54
                                integrator_ext_IC_test.__integrator_ext_IC_test_6_c
55
                                integrator_ext_IC_test.__integrator_ext_IC_test_7_c
56
                                integrator_ext_IC_test.ni_0._arrow._first_c
57
                                integrator_ext_IC_test.__integrator_ext_IC_test_2_m
58
                                integrator_ext_IC_test.__integrator_ext_IC_test_3_m
59
                                integrator_ext_IC_test.__integrator_ext_IC_test_4_m
60
                                integrator_ext_IC_test.__integrator_ext_IC_test_5_m
61
                                integrator_ext_IC_test.__integrator_ext_IC_test_6_m
62
                                integrator_ext_IC_test.__integrator_ext_IC_test_7_m
63
                                integrator_ext_IC_test.ni_0._arrow._first_m)
64
))
65

    
66
(rule (=> 
67
  (and (= integrator_ext_IC_test.ni_0._arrow._first_m integrator_ext_IC_test.ni_0._arrow._first_c)
68
       (and (= integrator_ext_IC_test.__integrator_ext_IC_test_1 (ite integrator_ext_IC_test.ni_0._arrow._first_m true false))
69
            (= integrator_ext_IC_test.ni_0._arrow._first_x false))
70
       (and (or (not (= integrator_ext_IC_test.__integrator_ext_IC_test_1 false))
71
               (and (= integrator_ext_IC_test.i_virtual_local 1.0)
72
                    (= integrator_ext_IC_test.Integrator11_1_1 (+ (* (* 1 1) integrator_ext_IC_test.__integrator_ext_IC_test_7_c) integrator_ext_IC_test.__integrator_ext_IC_test_6_c))
73
                    ))
74
            (or (not (= integrator_ext_IC_test.__integrator_ext_IC_test_1 true))
75
               (and (= integrator_ext_IC_test.i_virtual_local 0.0)
76
                    (= integrator_ext_IC_test.Integrator11_1_1 integrator_ext_IC_test.In21_1_1)
77
                    ))
78
       )
79
       (= integrator_ext_IC_test.__integrator_ext_IC_test_7_x integrator_ext_IC_test.In18_1_1)
80
       (= integrator_ext_IC_test.__integrator_ext_IC_test_6_x integrator_ext_IC_test.Integrator11_1_1)
81
       (and (or (not (= integrator_ext_IC_test.__integrator_ext_IC_test_1 true))
82
               (= integrator_ext_IC_test.Integrator3_1_1 integrator_ext_IC_test.In7_1_1))
83
            (or (not (= integrator_ext_IC_test.__integrator_ext_IC_test_1 false))
84
               (= integrator_ext_IC_test.Integrator3_1_1 (+ (* (* 1.00000000 1.00000000) integrator_ext_IC_test.__integrator_ext_IC_test_5_c) integrator_ext_IC_test.__integrator_ext_IC_test_4_c)))
85
       )
86
       (= integrator_ext_IC_test.__integrator_ext_IC_test_5_x integrator_ext_IC_test.In4_1_1)
87
       (= integrator_ext_IC_test.__integrator_ext_IC_test_4_x integrator_ext_IC_test.Integrator3_1_1)
88
       (and (or (not (= integrator_ext_IC_test.__integrator_ext_IC_test_1 true))
89
               (= integrator_ext_IC_test.Integrator7_1_1 integrator_ext_IC_test.In14_1_1))
90
            (or (not (= integrator_ext_IC_test.__integrator_ext_IC_test_1 false))
91
               (= integrator_ext_IC_test.Integrator7_1_1 (+ (* (* 1 1) integrator_ext_IC_test.__integrator_ext_IC_test_3_c) integrator_ext_IC_test.__integrator_ext_IC_test_2_c)))
92
       )
93
       (= integrator_ext_IC_test.__integrator_ext_IC_test_3_x integrator_ext_IC_test.In11_1_1)
94
       (= integrator_ext_IC_test.__integrator_ext_IC_test_2_x integrator_ext_IC_test.Integrator7_1_1)
95
       (= integrator_ext_IC_test.Out8_2_1 integrator_ext_IC_test.Integrator7_1_1)
96
       (= integrator_ext_IC_test.Out4_1_1 integrator_ext_IC_test.Integrator3_1_1)
97
       (= integrator_ext_IC_test.Out12_3_1 integrator_ext_IC_test.Integrator11_1_1)
98
       )
99
  (integrator_ext_IC_test_step integrator_ext_IC_test.In4_1_1
100
                               integrator_ext_IC_test.In7_1_1
101
                               integrator_ext_IC_test.In11_1_1
102
                               integrator_ext_IC_test.In14_1_1
103
                               integrator_ext_IC_test.In18_1_1
104
                               integrator_ext_IC_test.In21_1_1
105
                               integrator_ext_IC_test.Out4_1_1
106
                               integrator_ext_IC_test.Out8_2_1
107
                               integrator_ext_IC_test.Out12_3_1
108
                               integrator_ext_IC_test.__integrator_ext_IC_test_2_c
109
                               integrator_ext_IC_test.__integrator_ext_IC_test_3_c
110
                               integrator_ext_IC_test.__integrator_ext_IC_test_4_c
111
                               integrator_ext_IC_test.__integrator_ext_IC_test_5_c
112
                               integrator_ext_IC_test.__integrator_ext_IC_test_6_c
113
                               integrator_ext_IC_test.__integrator_ext_IC_test_7_c
114
                               integrator_ext_IC_test.ni_0._arrow._first_c
115
                               integrator_ext_IC_test.__integrator_ext_IC_test_2_x
116
                               integrator_ext_IC_test.__integrator_ext_IC_test_3_x
117
                               integrator_ext_IC_test.__integrator_ext_IC_test_4_x
118
                               integrator_ext_IC_test.__integrator_ext_IC_test_5_x
119
                               integrator_ext_IC_test.__integrator_ext_IC_test_6_x
120
                               integrator_ext_IC_test.__integrator_ext_IC_test_7_x
121
                               integrator_ext_IC_test.ni_0._arrow._first_x)
122
))
123