blob: 8be52a5775ad0e8ca171553d32a218fd9557e29d (
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
|
; EXPECT: unsat
; COMMAND-LINE: --cegqi-si=all --sygus-out=status --decision=justification
( set-logic LIA )
( synth-fun findIdx ( ( y1 Int ) ( y2 Int ) ( y3 Int ) ( y4 Int ) ( y5 Int ) ( k1 Int ) ) Int (
(Start Int ( NT1
NT3
NT4
NT7
NT8
NT9
NT10
NT11
NT13
NT14
))
(NT1 Int ( y5
k1
1
y2
0
y1
2
5
y4
4
y3
3
))
(NT2 Bool ( (< NT1 NT1)
(> NT1 NT1)
(>= NT1 NT1)
(<= NT1 NT1)
))
(NT3 Int ( (ite NT2 NT1 NT1)
))
(NT4 Int ( (ite NT5 NT1 NT1)
(ite NT2 NT3 NT1)
))
(NT5 Bool ( (< NT3 NT1)
(<= NT3 NT1)
(>= NT3 NT1)
(> NT3 NT1)
))
(NT6 Bool ( (<= NT4 NT1)
(> NT4 NT1)
(<= NT3 NT3)
(> NT3 NT3)
(>= NT4 NT1)
(< NT4 NT1)
(< NT3 NT3)
(>= NT3 NT3)
))
(NT7 Int ( (ite NT6 NT1 NT1)
(ite NT2 NT4 NT1)
))
(NT8 Int ( (ite NT2 NT7 NT1)
(ite NT5 NT4 NT1)
(ite NT15 NT1 NT1)
(ite NT5 NT1 NT4)
))
(NT9 Int ( (ite NT2 NT8 NT1)
(ite NT12 NT1 NT1)
(ite NT6 NT1 NT4)
(ite NT6 NT4 NT1)
(ite NT5 NT7 NT1)
))
(NT10 Int ( (ite NT5 NT8 NT1)
(ite NT16 NT1 NT1)
(ite NT2 NT9 NT1)
(ite NT6 NT7 NT1)
(ite NT5 NT4 NT4)
))
(NT11 Int ( (ite NT6 NT8 NT1)
(ite NT2 NT10 NT1)
(ite NT5 NT9 NT1)
(ite NT17 NT1 NT1)
(ite NT6 NT4 NT4)
))
(NT12 Bool ( (< NT4 NT4)
(> NT4 NT4)
(<= NT8 NT1)
(< NT8 NT1)
(<= NT4 NT4)
(> NT8 NT1)
(>= NT8 NT1)
(>= NT4 NT4)
))
(NT13 Int ( (ite NT18 NT1 NT1)
(ite NT12 NT7 NT1)
(ite NT5 NT10 NT1)
(ite NT6 NT9 NT1)
(ite NT12 NT1 NT7)
(ite NT2 NT11 NT1)
))
(NT14 Int ( (ite NT12 NT1 NT8)
(ite NT6 NT10 NT1)
(ite NT5 NT11 NT1)
(ite NT19 NT1 NT1)
(ite NT12 NT8 NT1)
(ite NT2 NT13 NT1)
))
(NT15 Bool ( (>= NT7 NT1)
(< NT7 NT1)
(> NT7 NT1)
(<= NT7 NT1)
))
(NT16 Bool ( (< NT9 NT1)
(>= NT9 NT1)
(> NT9 NT1)
(<= NT9 NT1)
))
(NT17 Bool ( (< NT7 NT7)
(<= NT10 NT1)
(>= NT10 NT1)
(> NT10 NT1)
(< NT10 NT1)
(> NT7 NT7)
(>= NT7 NT7)
(<= NT7 NT7)
))
(NT18 Bool ( (< NT11 NT1)
(> NT11 NT1)
(>= NT11 NT1)
(<= NT11 NT1)
))
(NT19 Bool ( (>= NT13 NT1)
(>= NT8 NT8)
(< NT13 NT1)
(> NT13 NT1)
(< NT8 NT8)
(> NT8 NT8)
(<= NT8 NT8)
(<= NT13 NT1)
))
))
( declare-var x1 Int )
( declare-var x2 Int )
( declare-var x3 Int )
( declare-var x4 Int )
( declare-var x5 Int )
( declare-var k Int )
( constraint ( => ( and ( < x1 x2 ) ( and ( < x2 x3 ) ( and ( < x3 x4 ) ( < x4 x5 ) ) ) ) ( => ( < k x1 ) ( = ( findIdx x1 x2 x3 x4 x5 k ) 0 ) ) ) )
( check-synth )
|
