Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_integrator_test / integrator_test.smt2 @ 6c3ea955

History | View | Annotate | Download (6.88 KB)

1
; integrator_test
2
(declare-var integrator_test.In1_1_1 Real)
3
(declare-var integrator_test.In2_1_1 Int)
4
(declare-var integrator_test.In3_1_1 Bool)
5
(declare-var integrator_test.Out1_1_1 Real)
6
(declare-var integrator_test.Out2_2_1 Int)
7
(declare-var integrator_test.Out3_3_1 Int)
8
(declare-var integrator_test.__integrator_test_2_c Int)
9
(declare-var integrator_test.__integrator_test_4_c Int)
10
(declare-var integrator_test.__integrator_test_5_c Int)
11
(declare-var integrator_test.__integrator_test_6_c Int)
12
(declare-var integrator_test.__integrator_test_7_c Real)
13
(declare-var integrator_test.__integrator_test_8_c Real)
14
(declare-var integrator_test.ni_0._arrow._first_c Bool)
15
(declare-var integrator_test.__integrator_test_2_m Int)
16
(declare-var integrator_test.__integrator_test_4_m Int)
17
(declare-var integrator_test.__integrator_test_5_m Int)
18
(declare-var integrator_test.__integrator_test_6_m Int)
19
(declare-var integrator_test.__integrator_test_7_m Real)
20
(declare-var integrator_test.__integrator_test_8_m Real)
21
(declare-var integrator_test.ni_0._arrow._first_m Bool)
22
(declare-var integrator_test.__integrator_test_2_x Int)
23
(declare-var integrator_test.__integrator_test_4_x Int)
24
(declare-var integrator_test.__integrator_test_5_x Int)
25
(declare-var integrator_test.__integrator_test_6_x Int)
26
(declare-var integrator_test.__integrator_test_7_x Real)
27
(declare-var integrator_test.__integrator_test_8_x Real)
28
(declare-var integrator_test.ni_0._arrow._first_x Bool)
29
(declare-var integrator_test.Integrator1_1_1 Int)
30
(declare-var integrator_test.Integrator2_1_1 Int)
31
(declare-var integrator_test.Integrator_1_1 Real)
32
(declare-var integrator_test.__integrator_test_1 Bool)
33
(declare-var integrator_test.__integrator_test_3 Int)
34
(declare-var integrator_test.i_virtual_local Real)
35
(declare-rel integrator_test_reset (Int Int Int Int Real Real Bool Int Int Int Int Real Real Bool))
36
(declare-rel integrator_test_step (Real Int Bool Real Int Int Int Int Int Int Real Real Bool Int Int Int Int Real Real Bool))
37

    
38
(rule (=> 
39
  (and 
40
       (= integrator_test.__integrator_test_2_m integrator_test.__integrator_test_2_c)
41
       (= integrator_test.__integrator_test_4_m integrator_test.__integrator_test_4_c)
42
       (= integrator_test.__integrator_test_5_m integrator_test.__integrator_test_5_c)
43
       (= integrator_test.__integrator_test_6_m integrator_test.__integrator_test_6_c)
44
       (= integrator_test.__integrator_test_7_m integrator_test.__integrator_test_7_c)
45
       (= integrator_test.__integrator_test_8_m integrator_test.__integrator_test_8_c)
46
       (= integrator_test.ni_0._arrow._first_m true)
47
  )
48
  (integrator_test_reset integrator_test.__integrator_test_2_c
49
                         integrator_test.__integrator_test_4_c
50
                         integrator_test.__integrator_test_5_c
51
                         integrator_test.__integrator_test_6_c
52
                         integrator_test.__integrator_test_7_c
53
                         integrator_test.__integrator_test_8_c
54
                         integrator_test.ni_0._arrow._first_c
55
                         integrator_test.__integrator_test_2_m
56
                         integrator_test.__integrator_test_4_m
57
                         integrator_test.__integrator_test_5_m
58
                         integrator_test.__integrator_test_6_m
59
                         integrator_test.__integrator_test_7_m
60
                         integrator_test.__integrator_test_8_m
61
                         integrator_test.ni_0._arrow._first_m)
62
))
63

    
64
(rule (=> 
65
  (and (= integrator_test.ni_0._arrow._first_m integrator_test.ni_0._arrow._first_c)
66
       (and (= integrator_test.__integrator_test_1 (ite integrator_test.ni_0._arrow._first_m true false))
67
            (= integrator_test.ni_0._arrow._first_x false))
68
       (and (or (not (= integrator_test.__integrator_test_1 false))
69
               (and (= integrator_test.i_virtual_local 1.0)
70
                    (= integrator_test.Integrator_1_1 (+ (* (* 1.00000000 1.00000000) integrator_test.__integrator_test_8_c) integrator_test.__integrator_test_7_c))
71
                    ))
72
            (or (not (= integrator_test.__integrator_test_1 true))
73
               (and (= integrator_test.i_virtual_local 0.0)
74
                    (= integrator_test.Integrator_1_1 0.00000000)
75
                    ))
76
       )
77
       (= integrator_test.__integrator_test_8_x integrator_test.In1_1_1)
78
       (= integrator_test.__integrator_test_7_x integrator_test.Integrator_1_1)
79
       (and (or (not (= integrator_test.__integrator_test_1 true))
80
               (= integrator_test.Integrator1_1_1 0))
81
            (or (not (= integrator_test.__integrator_test_1 false))
82
               (= integrator_test.Integrator1_1_1 (+ (* (* 1 1) integrator_test.__integrator_test_6_c) integrator_test.__integrator_test_5_c)))
83
       )
84
       (= integrator_test.__integrator_test_6_x integrator_test.In2_1_1)
85
       (= integrator_test.__integrator_test_5_x integrator_test.Integrator1_1_1)
86
       (and (or (not (= integrator_test.In3_1_1 true))
87
               (= integrator_test.__integrator_test_3 1))
88
            (or (not (= integrator_test.In3_1_1 false))
89
               (= integrator_test.__integrator_test_3 0))
90
       )
91
       (and (or (not (= integrator_test.__integrator_test_1 true))
92
               (= integrator_test.Integrator2_1_1 0))
93
            (or (not (= integrator_test.__integrator_test_1 false))
94
               (= integrator_test.Integrator2_1_1 (+ (* (* 1 1) integrator_test.__integrator_test_4_c) integrator_test.__integrator_test_2_c)))
95
       )
96
       (= integrator_test.__integrator_test_4_x integrator_test.__integrator_test_3)
97
       (= integrator_test.__integrator_test_2_x integrator_test.Integrator2_1_1)
98
       (= integrator_test.Out3_3_1 integrator_test.Integrator2_1_1)
99
       (= integrator_test.Out2_2_1 integrator_test.Integrator1_1_1)
100
       (= integrator_test.Out1_1_1 integrator_test.Integrator_1_1)
101
       )
102
  (integrator_test_step integrator_test.In1_1_1
103
                        integrator_test.In2_1_1
104
                        integrator_test.In3_1_1
105
                        integrator_test.Out1_1_1
106
                        integrator_test.Out2_2_1
107
                        integrator_test.Out3_3_1
108
                        integrator_test.__integrator_test_2_c
109
                        integrator_test.__integrator_test_4_c
110
                        integrator_test.__integrator_test_5_c
111
                        integrator_test.__integrator_test_6_c
112
                        integrator_test.__integrator_test_7_c
113
                        integrator_test.__integrator_test_8_c
114
                        integrator_test.ni_0._arrow._first_c
115
                        integrator_test.__integrator_test_2_x
116
                        integrator_test.__integrator_test_4_x
117
                        integrator_test.__integrator_test_5_x
118
                        integrator_test.__integrator_test_6_x
119
                        integrator_test.__integrator_test_7_x
120
                        integrator_test.__integrator_test_8_x
121
                        integrator_test.ni_0._arrow._first_x)
122
))
123