Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_polyval_test / polyval_test.smt2 @ 6c3ea955

History | View | Annotate | Download (5.59 KB)

1 6c3ea955 bourbouh
; polyval_test
2
(declare-var polyval_test.In1_1_1 Real)
3
(declare-var polyval_test.In2_1_1 Real)
4
(declare-var polyval_test.In2_1_2 Real)
5
(declare-var polyval_test.In2_1_3 Real)
6
(declare-var polyval_test.In3_1_1 Real)
7
(declare-var polyval_test.In3_1_2 Real)
8
(declare-var polyval_test.In3_1_3 Real)
9
(declare-var polyval_test.In3_1_4 Real)
10
(declare-var polyval_test.In3_1_5 Real)
11
(declare-var polyval_test.In3_1_6 Real)
12
(declare-var polyval_test.Out7_1_1 Real)
13
(declare-var polyval_test.Out1_2_1 Real)
14
(declare-var polyval_test.Out1_2_2 Real)
15
(declare-var polyval_test.Out1_2_3 Real)
16
(declare-var polyval_test.Out2_3_1 Real)
17
(declare-var polyval_test.Out2_3_2 Real)
18
(declare-var polyval_test.Out2_3_3 Real)
19
(declare-var polyval_test.Out2_3_4 Real)
20
(declare-var polyval_test.Out2_3_5 Real)
21
(declare-var polyval_test.Out2_3_6 Real)
22
(declare-var polyval_test.ni_0._arrow._first_c Bool)
23
(declare-var polyval_test.ni_0._arrow._first_m Bool)
24
(declare-var polyval_test.ni_0._arrow._first_x Bool)
25
(declare-var polyval_test.Polynomial1_1_1 Real)
26
(declare-var polyval_test.Polynomial1_1_2 Real)
27
(declare-var polyval_test.Polynomial1_1_3 Real)
28
(declare-var polyval_test.Polynomial2_1_1 Real)
29
(declare-var polyval_test.Polynomial2_1_2 Real)
30
(declare-var polyval_test.Polynomial2_1_3 Real)
31
(declare-var polyval_test.Polynomial2_1_4 Real)
32
(declare-var polyval_test.Polynomial2_1_5 Real)
33
(declare-var polyval_test.Polynomial2_1_6 Real)
34
(declare-var polyval_test.Polynomial_1_1 Real)
35
(declare-var polyval_test.__polyval_test_1 Bool)
36
(declare-var polyval_test.i_virtual_local Real)
37
(declare-rel polyval_test_reset (Bool Bool))
38
(declare-rel polyval_test_step (Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Bool Bool))
39
40
(rule (=> 
41
  (and 
42
       
43
       (= polyval_test.ni_0._arrow._first_m true)
44
  )
45
  (polyval_test_reset polyval_test.ni_0._arrow._first_c
46
                      polyval_test.ni_0._arrow._first_m)
47
))
48
49
(rule (=> 
50
  (and (= polyval_test.ni_0._arrow._first_m polyval_test.ni_0._arrow._first_c)
51
       (and (= polyval_test.__polyval_test_1 (ite polyval_test.ni_0._arrow._first_m true false))
52
            (= polyval_test.ni_0._arrow._first_x false))
53
       (and (or (not (= polyval_test.__polyval_test_1 true))
54
               (= polyval_test.i_virtual_local 0.0))
55
            (or (not (= polyval_test.__polyval_test_1 false))
56
               (= polyval_test.i_virtual_local 1.0))
57
       )
58
       (= polyval_test.Polynomial_1_1 (+ (+ (* (* 3.0000000000 polyval_test.In1_1_1) polyval_test.In1_1_1) (* 2.0000000000 polyval_test.In1_1_1)) (- 10.0000000000)))
59
       (= polyval_test.Polynomial2_1_6 (+ (+ (* (* (- 15.8000000000) polyval_test.In3_1_6) polyval_test.In3_1_6) (* 0.0000000000 polyval_test.In3_1_6)) (- 10.0000000000)))
60
       (= polyval_test.Polynomial2_1_5 (+ (+ (* (* (- 15.8000000000) polyval_test.In3_1_5) polyval_test.In3_1_5) (* 0.0000000000 polyval_test.In3_1_5)) (- 10.0000000000)))
61
       (= polyval_test.Polynomial2_1_4 (+ (+ (* (* (- 15.8000000000) polyval_test.In3_1_4) polyval_test.In3_1_4) (* 0.0000000000 polyval_test.In3_1_4)) (- 10.0000000000)))
62
       (= polyval_test.Polynomial2_1_3 (+ (+ (* (* (- 15.8000000000) polyval_test.In3_1_3) polyval_test.In3_1_3) (* 0.0000000000 polyval_test.In3_1_3)) (- 10.0000000000)))
63
       (= polyval_test.Polynomial2_1_2 (+ (+ (* (* (- 15.8000000000) polyval_test.In3_1_2) polyval_test.In3_1_2) (* 0.0000000000 polyval_test.In3_1_2)) (- 10.0000000000)))
64
       (= polyval_test.Polynomial2_1_1 (+ (+ (* (* (- 15.8000000000) polyval_test.In3_1_1) polyval_test.In3_1_1) (* 0.0000000000 polyval_test.In3_1_1)) (- 10.0000000000)))
65
       (= polyval_test.Polynomial1_1_3 (+ (+ (* (* 3.0000000000 polyval_test.In2_1_3) polyval_test.In2_1_3) (* 0.0000025000 polyval_test.In2_1_3)) (- 10.0000000000)))
66
       (= polyval_test.Polynomial1_1_2 (+ (+ (* (* 3.0000000000 polyval_test.In2_1_2) polyval_test.In2_1_2) (* 0.0000025000 polyval_test.In2_1_2)) (- 10.0000000000)))
67
       (= polyval_test.Polynomial1_1_1 (+ (+ (* (* 3.0000000000 polyval_test.In2_1_1) polyval_test.In2_1_1) (* 0.0000025000 polyval_test.In2_1_1)) (- 10.0000000000)))
68
       (= polyval_test.Out7_1_1 polyval_test.Polynomial_1_1)
69
       (= polyval_test.Out2_3_6 polyval_test.Polynomial2_1_6)
70
       (= polyval_test.Out2_3_5 polyval_test.Polynomial2_1_5)
71
       (= polyval_test.Out2_3_4 polyval_test.Polynomial2_1_4)
72
       (= polyval_test.Out2_3_3 polyval_test.Polynomial2_1_3)
73
       (= polyval_test.Out2_3_2 polyval_test.Polynomial2_1_2)
74
       (= polyval_test.Out2_3_1 polyval_test.Polynomial2_1_1)
75
       (= polyval_test.Out1_2_3 polyval_test.Polynomial1_1_3)
76
       (= polyval_test.Out1_2_2 polyval_test.Polynomial1_1_2)
77
       (= polyval_test.Out1_2_1 polyval_test.Polynomial1_1_1)
78
       )
79
  (polyval_test_step polyval_test.In1_1_1
80
                     polyval_test.In2_1_1
81
                     polyval_test.In2_1_2
82
                     polyval_test.In2_1_3
83
                     polyval_test.In3_1_1
84
                     polyval_test.In3_1_2
85
                     polyval_test.In3_1_3
86
                     polyval_test.In3_1_4
87
                     polyval_test.In3_1_5
88
                     polyval_test.In3_1_6
89
                     polyval_test.Out7_1_1
90
                     polyval_test.Out1_2_1
91
                     polyval_test.Out1_2_2
92
                     polyval_test.Out1_2_3
93
                     polyval_test.Out2_3_1
94
                     polyval_test.Out2_3_2
95
                     polyval_test.Out2_3_3
96
                     polyval_test.Out2_3_4
97
                     polyval_test.Out2_3_5
98
                     polyval_test.Out2_3_6
99
                     polyval_test.ni_0._arrow._first_c
100
                     polyval_test.ni_0._arrow._first_x)
101
))