blob: c10cab2f5e661796365da93a1dc9563f18318c1b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status
(set-logic LIA)
(synth-fun fr0 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr1 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr10 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr11 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr12 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr13 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr14 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr15 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr16 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr17 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr18 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr19 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr2 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr20 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr21 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr22 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr23 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr24 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr25 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr26 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr27 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr28 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr29 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr3 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr30 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr31 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr32 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr33 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr34 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr35 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr36 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr4 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr5 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr6 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr7 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr8 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun fr9 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun m0 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun m1 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun m10 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun m11 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun m12 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun m13 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun m14 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun m15 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun m16 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun m17 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun m2 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun m3 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun m4 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun m5 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun m6 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun m7 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun m8 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun m9 ((_v Int) (n Int) (x Int)) Int
)
(synth-fun p0 ((_v Int) (n Int) (x Int)) Int)
(synth-fun p1 ((_v Int) (n Int) (x Int)) Int)
(synth-fun p2 ((_v Int) (n Int) (x Int)) Int)
(synth-fun p3 ((_v Int) (n Int) (x Int)) Int)
(synth-fun p4 ((_v Int) (n Int) (x Int)) Int)
(synth-fun p5 ((_v Int) (n Int) (x Int)) Int)
(declare-var n Int)
(declare-var x Int)
(declare-var x10 Int)
(declare-var x11 Int)
(declare-var x14 Int)
(declare-var x15 Int)
(declare-var x2 Int)
(declare-var x3 Int)
(declare-var x6 Int)
(declare-var x7 Int)
(declare-var _v Int)
(assume (and (= false (<= n 0)) (>= n 0)))
(constraint (>= (p4 _v n x) 0))
(constraint (and (and (and (>= (m6 _v n x) 0) (>= (m8 _v n x) 0)) (>= (m9 _v n x) 0)) (= (m6 _v n x) (+ (m8 _v n x) (m9 _v n x)))))
(constraint (and (and (and (>= (fr17 _v n x) 0) (>= (fr19 _v n x) 0)) (>= (fr20 _v n x) 0)) (= (fr17 _v n x) (+ (fr19 _v n x) (fr20 _v n x)))))
(constraint (and (and (and (>= (fr15 _v n x) 0) (>= (fr17 _v n x) 0)) (>= (fr18 _v n x) 0)) (= (fr15 _v n x) (+ (fr17 _v n x) (fr18 _v n x)))))
(constraint (and (and (and (>= (m1 _v n x) 0) (>= (m6 _v n x) 0)) (>= (m7 _v n x) 0)) (= (m1 _v n x) (+ (m6 _v n x) (m7 _v n x)))))
(constraint (and (and (and (>= (fr13 _v n x) 0) (>= (fr15 _v n x) 0)) (>= (fr16 _v n x) 0)) (= (fr13 _v n x) (+ (fr15 _v n x) (fr16 _v n x)))))
(constraint (and (and (and (>= (fr12 _v n x) 0) (>= (fr13 _v n x) 0)) (>= (fr14 _v n x) 0)) (= (fr12 _v n x) (+ (fr13 _v n x) (fr14 _v n x)))))
(constraint (and (and (and (and (and (and (= (+ (+ (+ 0 (p1 _v n x)) (fr1 _v n x)) 0) (+ (+ (+ 0 0) (fr12 _v n x)) 0)) (>= (fr1 _v n x) 0)) (>= (fr12 _v n x) 0)) (>= 0 0)) (>= 0 0)) (>= 0 0)) (>= 0 0)))
(constraint (=> (and (and (= false (<= n 0)) (= _v x)) (>= n 0)) (>= 0 (+ (p4 _v n x) (- (+ (fr18 _v n x) 0))))))
(constraint (>= 0 (- (+ (fr14 _v n x) 0))))
(constraint (>= (p5 _v n x) (p4 _v n x)))
(constraint (>= (p5 _v n x) 0))
(constraint (and (and (and (>= (m10 _v n x) 0) (>= (m12 _v n x) 0)) (>= (m13 _v n x) 0)) (= (m10 _v n x) (+ (m12 _v n x) (m13 _v n x)))))
(constraint (and (and (and (>= (fr25 _v n x) 0) (>= (fr27 _v n x) 0)) (>= (fr28 _v n x) 0)) (= (fr25 _v n x) (+ (fr27 _v n x) (fr28 _v n x)))))
(constraint (and (and (and (>= (fr23 _v n x) 0) (>= (fr25 _v n x) 0)) (>= (fr26 _v n x) 0)) (= (fr23 _v n x) (+ (fr25 _v n x) (fr26 _v n x)))))
(constraint (and (and (and (>= (m7 _v n x) 0) (>= (m10 _v n x) 0)) (>= (m11 _v n x) 0)) (= (m7 _v n x) (+ (m10 _v n x) (m11 _v n x)))))
(constraint (and (and (and (>= (fr21 _v n x) 0) (>= (fr23 _v n x) 0)) (>= (fr24 _v n x) 0)) (= (fr21 _v n x) (+ (fr23 _v n x) (fr24 _v n x)))))
(constraint (and (and (and (>= (- (fr16 _v n x) 1) 0) (>= (fr21 _v n x) 0)) (>= (fr22 _v n x) 0)) (= (- (fr16 _v n x) 1) (+ (fr21 _v n x) (fr22 _v n x)))))
(constraint (=> false (>= 0 (- (+ (fr26 _v n x) 0)))))
(constraint (and (and (and (>= (m14 _v n x) 0) (>= (m16 _v n x) 0)) (>= (m17 _v n x) 0)) (= (m14 _v n x) (+ (m16 _v n x) (m17 _v n x)))))
(constraint (and (and (and (>= (fr33 _v n x) 0) (>= (fr35 _v n x) 0)) (>= (fr36 _v n x) 0)) (= (fr33 _v n x) (+ (fr35 _v n x) (fr36 _v n x)))))
(constraint (and (and (and (>= (fr31 _v n x) 0) (>= (fr33 _v n x) 0)) (>= (fr34 _v n x) 0)) (= (fr31 _v n x) (+ (fr33 _v n x) (fr34 _v n x)))))
(constraint (and (and (and (>= (m13 _v n x) 0) (>= (m14 _v n x) 0)) (>= (m15 _v n x) 0)) (= (m13 _v n x) (+ (m14 _v n x) (m15 _v n x)))))
(constraint (and (and (and (>= (fr29 _v n x) 0) (>= (fr31 _v n x) 0)) (>= (fr32 _v n x) 0)) (= (fr29 _v n x) (+ (fr31 _v n x) (fr32 _v n x)))))
(constraint (and (and (and (>= (fr28 _v n x) 0) (>= (fr29 _v n x) 0)) (>= (fr30 _v n x) 0)) (= (fr28 _v n x) (+ (fr29 _v n x) (fr30 _v n x)))))
(check-synth)
|
