Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_mux_test / mux_test.smt2 @ 6c3ea955

History | View | Annotate | Download (4.04 KB)

1
; mux_test
2
(declare-var mux_test.In1_1_1 Real)
3
(declare-var mux_test.In2_1_1 Real)
4
(declare-var mux_test.In3_1_1 Real)
5
(declare-var mux_test.In4_1_1 Real)
6
(declare-var mux_test.In4_1_2 Real)
7
(declare-var mux_test.In4_1_3 Real)
8
(declare-var mux_test.In5_1_1 Real)
9
(declare-var mux_test.In5_1_2 Real)
10
(declare-var mux_test.In6_1_1 Real)
11
(declare-var mux_test.In6_1_2 Real)
12
(declare-var mux_test.In6_1_3 Real)
13
(declare-var mux_test.Out1_1_1 Real)
14
(declare-var mux_test.Out1_1_2 Real)
15
(declare-var mux_test.Out2_2_1 Real)
16
(declare-var mux_test.Out2_2_2 Real)
17
(declare-var mux_test.Out2_2_3 Real)
18
(declare-var mux_test.Out2_2_4 Real)
19
(declare-var mux_test.Out3_3_1 Real)
20
(declare-var mux_test.Out3_3_2 Real)
21
(declare-var mux_test.Out3_3_3 Real)
22
(declare-var mux_test.Out3_3_4 Real)
23
(declare-var mux_test.Out3_3_5 Real)
24
(declare-var mux_test.ni_0._arrow._first_c Bool)
25
(declare-var mux_test.ni_0._arrow._first_m Bool)
26
(declare-var mux_test.ni_0._arrow._first_x Bool)
27
(declare-var mux_test.Mux1_1_1 Real)
28
(declare-var mux_test.Mux1_1_2 Real)
29
(declare-var mux_test.Mux1_1_3 Real)
30
(declare-var mux_test.Mux1_1_4 Real)
31
(declare-var mux_test.Mux2_1_1 Real)
32
(declare-var mux_test.Mux2_1_2 Real)
33
(declare-var mux_test.Mux2_1_3 Real)
34
(declare-var mux_test.Mux2_1_4 Real)
35
(declare-var mux_test.Mux2_1_5 Real)
36
(declare-var mux_test.Mux_1_1 Real)
37
(declare-var mux_test.Mux_1_2 Real)
38
(declare-var mux_test.__mux_test_1 Bool)
39
(declare-var mux_test.i_virtual_local Real)
40
(declare-rel mux_test_reset (Bool Bool))
41
(declare-rel mux_test_step (Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Bool Bool))
42

    
43
(rule (=> 
44
  (and 
45
       
46
       (= mux_test.ni_0._arrow._first_m true)
47
  )
48
  (mux_test_reset mux_test.ni_0._arrow._first_c
49
                  mux_test.ni_0._arrow._first_m)
50
))
51

    
52
(rule (=> 
53
  (and (= mux_test.ni_0._arrow._first_m mux_test.ni_0._arrow._first_c)
54
       (and (= mux_test.__mux_test_1 (ite mux_test.ni_0._arrow._first_m true false))
55
            (= mux_test.ni_0._arrow._first_x false))
56
       (and (or (not (= mux_test.__mux_test_1 true))
57
               (= mux_test.i_virtual_local 0.0))
58
            (or (not (= mux_test.__mux_test_1 false))
59
               (= mux_test.i_virtual_local 1.0))
60
       )
61
       (= mux_test.Mux2_1_5 mux_test.In6_1_3)
62
       (= mux_test.Out3_3_5 mux_test.Mux2_1_5)
63
       (= mux_test.Mux2_1_4 mux_test.In6_1_2)
64
       (= mux_test.Out3_3_4 mux_test.Mux2_1_4)
65
       (= mux_test.Mux2_1_3 mux_test.In6_1_1)
66
       (= mux_test.Out3_3_3 mux_test.Mux2_1_3)
67
       (= mux_test.Mux2_1_2 mux_test.In5_1_2)
68
       (= mux_test.Out3_3_2 mux_test.Mux2_1_2)
69
       (= mux_test.Mux2_1_1 mux_test.In5_1_1)
70
       (= mux_test.Out3_3_1 mux_test.Mux2_1_1)
71
       (= mux_test.Mux1_1_4 mux_test.In4_1_3)
72
       (= mux_test.Out2_2_4 mux_test.Mux1_1_4)
73
       (= mux_test.Mux1_1_3 mux_test.In4_1_2)
74
       (= mux_test.Out2_2_3 mux_test.Mux1_1_3)
75
       (= mux_test.Mux1_1_2 mux_test.In4_1_1)
76
       (= mux_test.Out2_2_2 mux_test.Mux1_1_2)
77
       (= mux_test.Mux1_1_1 mux_test.In3_1_1)
78
       (= mux_test.Out2_2_1 mux_test.Mux1_1_1)
79
       (= mux_test.Mux_1_2 mux_test.In2_1_1)
80
       (= mux_test.Out1_1_2 mux_test.Mux_1_2)
81
       (= mux_test.Mux_1_1 mux_test.In1_1_1)
82
       (= mux_test.Out1_1_1 mux_test.Mux_1_1)
83
       )
84
  (mux_test_step mux_test.In1_1_1
85
                 mux_test.In2_1_1
86
                 mux_test.In3_1_1
87
                 mux_test.In4_1_1
88
                 mux_test.In4_1_2
89
                 mux_test.In4_1_3
90
                 mux_test.In5_1_1
91
                 mux_test.In5_1_2
92
                 mux_test.In6_1_1
93
                 mux_test.In6_1_2
94
                 mux_test.In6_1_3
95
                 mux_test.Out1_1_1
96
                 mux_test.Out1_1_2
97
                 mux_test.Out2_2_1
98
                 mux_test.Out2_2_2
99
                 mux_test.Out2_2_3
100
                 mux_test.Out2_2_4
101
                 mux_test.Out3_3_1
102
                 mux_test.Out3_3_2
103
                 mux_test.Out3_3_3
104
                 mux_test.Out3_3_4
105
                 mux_test.Out3_3_5
106
                 mux_test.ni_0._arrow._first_c
107
                 mux_test.ni_0._arrow._first_x)
108
))
109