Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_logic_expand_test / logic_expand_test.smt2 @ 6c3ea955

History | View | Annotate | Download (7.93 KB)

1
; logic_expand_test
2
(declare-var logic_expand_test.In1_1_1 Bool)
3
(declare-var logic_expand_test.In2_1_1 Bool)
4
(declare-var logic_expand_test.In2_1_2 Bool)
5
(declare-var logic_expand_test.In2_1_3 Bool)
6
(declare-var logic_expand_test.In3_1_1 Bool)
7
(declare-var logic_expand_test.In4_1_1 Bool)
8
(declare-var logic_expand_test.In4_1_2 Bool)
9
(declare-var logic_expand_test.In4_1_3 Bool)
10
(declare-var logic_expand_test.In5_1_1 Bool)
11
(declare-var logic_expand_test.In6_1_1 Bool)
12
(declare-var logic_expand_test.In6_1_2 Bool)
13
(declare-var logic_expand_test.In6_1_3 Bool)
14
(declare-var logic_expand_test.In7_1_1 Bool)
15
(declare-var logic_expand_test.In8_1_1 Bool)
16
(declare-var logic_expand_test.In9_1_1 Bool)
17
(declare-var logic_expand_test.In9_1_2 Bool)
18
(declare-var logic_expand_test.In9_1_3 Bool)
19
(declare-var logic_expand_test.In10_1_1 Bool)
20
(declare-var logic_expand_test.In10_1_2 Bool)
21
(declare-var logic_expand_test.In10_1_3 Bool)
22
(declare-var logic_expand_test.In11_1_1 Bool)
23
(declare-var logic_expand_test.In12_1_1 Bool)
24
(declare-var logic_expand_test.Out1_1_1 Bool)
25
(declare-var logic_expand_test.Out1_1_2 Bool)
26
(declare-var logic_expand_test.Out1_1_3 Bool)
27
(declare-var logic_expand_test.Out2_2_1 Bool)
28
(declare-var logic_expand_test.Out2_2_2 Bool)
29
(declare-var logic_expand_test.Out2_2_3 Bool)
30
(declare-var logic_expand_test.Out3_3_1 Bool)
31
(declare-var logic_expand_test.Out3_3_2 Bool)
32
(declare-var logic_expand_test.Out3_3_3 Bool)
33
(declare-var logic_expand_test.Out4_4_1 Bool)
34
(declare-var logic_expand_test.Out4_4_2 Bool)
35
(declare-var logic_expand_test.Out4_4_3 Bool)
36
(declare-var logic_expand_test.ni_0._arrow._first_c Bool)
37
(declare-var logic_expand_test.ni_0._arrow._first_m Bool)
38
(declare-var logic_expand_test.ni_0._arrow._first_x Bool)
39
(declare-var logic_expand_test.LogicalOperator1_1_1 Bool)
40
(declare-var logic_expand_test.LogicalOperator1_1_2 Bool)
41
(declare-var logic_expand_test.LogicalOperator1_1_3 Bool)
42
(declare-var logic_expand_test.LogicalOperator2_1_1 Bool)
43
(declare-var logic_expand_test.LogicalOperator2_1_2 Bool)
44
(declare-var logic_expand_test.LogicalOperator2_1_3 Bool)
45
(declare-var logic_expand_test.LogicalOperator3_1_1 Bool)
46
(declare-var logic_expand_test.LogicalOperator3_1_2 Bool)
47
(declare-var logic_expand_test.LogicalOperator3_1_3 Bool)
48
(declare-var logic_expand_test.LogicalOperator_1_1 Bool)
49
(declare-var logic_expand_test.LogicalOperator_1_2 Bool)
50
(declare-var logic_expand_test.LogicalOperator_1_3 Bool)
51
(declare-var logic_expand_test.__logic_expand_test_1 Bool)
52
(declare-var logic_expand_test.i_virtual_local Real)
53
(declare-rel logic_expand_test_reset (Bool Bool))
54
(declare-rel logic_expand_test_step (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool))
55

    
56
(rule (=> 
57
  (and 
58
       
59
       (= logic_expand_test.ni_0._arrow._first_m true)
60
  )
61
  (logic_expand_test_reset logic_expand_test.ni_0._arrow._first_c
62
                           logic_expand_test.ni_0._arrow._first_m)
63
))
64

    
65
(rule (=> 
66
  (and (= logic_expand_test.ni_0._arrow._first_m logic_expand_test.ni_0._arrow._first_c)
67
       (and (= logic_expand_test.__logic_expand_test_1 (ite logic_expand_test.ni_0._arrow._first_m true false))
68
            (= logic_expand_test.ni_0._arrow._first_x false))
69
       (and (or (not (= logic_expand_test.__logic_expand_test_1 true))
70
               (= logic_expand_test.i_virtual_local 0.0))
71
            (or (not (= logic_expand_test.__logic_expand_test_1 false))
72
               (= logic_expand_test.i_virtual_local 1.0))
73
       )
74
       (= logic_expand_test.LogicalOperator3_1_3 (and (and logic_expand_test.In10_1_3 logic_expand_test.In11_1_1) logic_expand_test.In12_1_1))
75
       (= logic_expand_test.Out4_4_3 logic_expand_test.LogicalOperator3_1_3)
76
       (= logic_expand_test.LogicalOperator3_1_2 (and (and logic_expand_test.In10_1_2 logic_expand_test.In11_1_1) logic_expand_test.In12_1_1))
77
       (= logic_expand_test.Out4_4_2 logic_expand_test.LogicalOperator3_1_2)
78
       (= logic_expand_test.LogicalOperator3_1_1 (and (and logic_expand_test.In10_1_1 logic_expand_test.In11_1_1) logic_expand_test.In12_1_1))
79
       (= logic_expand_test.Out4_4_1 logic_expand_test.LogicalOperator3_1_1)
80
       (= logic_expand_test.LogicalOperator2_1_3 (and (and logic_expand_test.In7_1_1 logic_expand_test.In8_1_1) logic_expand_test.In9_1_3))
81
       (= logic_expand_test.Out3_3_3 logic_expand_test.LogicalOperator2_1_3)
82
       (= logic_expand_test.LogicalOperator2_1_2 (and (and logic_expand_test.In7_1_1 logic_expand_test.In8_1_1) logic_expand_test.In9_1_2))
83
       (= logic_expand_test.Out3_3_2 logic_expand_test.LogicalOperator2_1_2)
84
       (= logic_expand_test.LogicalOperator2_1_1 (and (and logic_expand_test.In7_1_1 logic_expand_test.In8_1_1) logic_expand_test.In9_1_1))
85
       (= logic_expand_test.Out3_3_1 logic_expand_test.LogicalOperator2_1_1)
86
       (= logic_expand_test.LogicalOperator1_1_3 (and (and logic_expand_test.In4_1_3 logic_expand_test.In5_1_1) logic_expand_test.In6_1_3))
87
       (= logic_expand_test.Out2_2_3 logic_expand_test.LogicalOperator1_1_3)
88
       (= logic_expand_test.LogicalOperator1_1_2 (and (and logic_expand_test.In4_1_2 logic_expand_test.In5_1_1) logic_expand_test.In6_1_2))
89
       (= logic_expand_test.Out2_2_2 logic_expand_test.LogicalOperator1_1_2)
90
       (= logic_expand_test.LogicalOperator1_1_1 (and (and logic_expand_test.In4_1_1 logic_expand_test.In5_1_1) logic_expand_test.In6_1_1))
91
       (= logic_expand_test.Out2_2_1 logic_expand_test.LogicalOperator1_1_1)
92
       (= logic_expand_test.LogicalOperator_1_3 (and (and logic_expand_test.In1_1_1 logic_expand_test.In2_1_3) logic_expand_test.In3_1_1))
93
       (= logic_expand_test.Out1_1_3 logic_expand_test.LogicalOperator_1_3)
94
       (= logic_expand_test.LogicalOperator_1_2 (and (and logic_expand_test.In1_1_1 logic_expand_test.In2_1_2) logic_expand_test.In3_1_1))
95
       (= logic_expand_test.Out1_1_2 logic_expand_test.LogicalOperator_1_2)
96
       (= logic_expand_test.LogicalOperator_1_1 (and (and logic_expand_test.In1_1_1 logic_expand_test.In2_1_1) logic_expand_test.In3_1_1))
97
       (= logic_expand_test.Out1_1_1 logic_expand_test.LogicalOperator_1_1)
98
       )
99
  (logic_expand_test_step logic_expand_test.In1_1_1
100
                          logic_expand_test.In2_1_1
101
                          logic_expand_test.In2_1_2
102
                          logic_expand_test.In2_1_3
103
                          logic_expand_test.In3_1_1
104
                          logic_expand_test.In4_1_1
105
                          logic_expand_test.In4_1_2
106
                          logic_expand_test.In4_1_3
107
                          logic_expand_test.In5_1_1
108
                          logic_expand_test.In6_1_1
109
                          logic_expand_test.In6_1_2
110
                          logic_expand_test.In6_1_3
111
                          logic_expand_test.In7_1_1
112
                          logic_expand_test.In8_1_1
113
                          logic_expand_test.In9_1_1
114
                          logic_expand_test.In9_1_2
115
                          logic_expand_test.In9_1_3
116
                          logic_expand_test.In10_1_1
117
                          logic_expand_test.In10_1_2
118
                          logic_expand_test.In10_1_3
119
                          logic_expand_test.In11_1_1
120
                          logic_expand_test.In12_1_1
121
                          logic_expand_test.Out1_1_1
122
                          logic_expand_test.Out1_1_2
123
                          logic_expand_test.Out1_1_3
124
                          logic_expand_test.Out2_2_1
125
                          logic_expand_test.Out2_2_2
126
                          logic_expand_test.Out2_2_3
127
                          logic_expand_test.Out3_3_1
128
                          logic_expand_test.Out3_3_2
129
                          logic_expand_test.Out3_3_3
130
                          logic_expand_test.Out4_4_1
131
                          logic_expand_test.Out4_4_2
132
                          logic_expand_test.Out4_4_3
133
                          logic_expand_test.ni_0._arrow._first_c
134
                          logic_expand_test.ni_0._arrow._first_x)
135
))
136