1off clprlverbose;
2
3
4
5% Choose real closed fields as the domain:
6rlset r;
7
8
9{ofsf}
10
11
12
13% Floor function:
14prog1 := {
15   nat(0) :- true,
16   nat(x+1) :- nat(x),
17   floor(x,y) :- nat(y) & y<=x & y+1>x};
18
19
20prog1 := {nat(0) :- true,
21
22          nat(x + 1) :- nat(x),
23
24          floor(x,y) :- nat(y) & ( - x + y + 1 > 0 and  - x + y <= 0)}
25
26
27goal1 := false :- floor(47.3,y);
28
29
30                         473
31goal1 := false :- floor(-----,y)
32                         10
33
34
35clp(prog1,goal1);
36
37
38y - 47 = 0
39
40
41
42% Loan computations:
43prog2 := {
44   loan(d,t,z,r,s) :- t=0 & d=s,
45   loan(d,t,z,r,s) :- t>0 & loan(d+d*z-r,t-1,z,r,s)};
46
47
48prog2 := {loan(d,t,z,r,s) :- (d - s = 0 and t = 0),
49
50          loan(d,t,z,r,s) :- loan(d*z + d - r,t - 1,z,r,s) & t > 0}
51
52
53goal2a := false :- loan(20000,36,0.01,600,s);
54
55
56                                   1
57goal2a := false :- loan(20000,36,-----,600,s)
58                                  100
59
60goal2b := false :- loan(20000,36,0.01,r,0);
61
62
63                                   1
64goal2b := false :- loan(20000,36,-----,r,0)
65                                  100
66
67goal2c := false :- loan(d,36,0.01,600,0);
68
69
70                               1
71goal2c := false :- loan(d,36,-----,600,0)
72                              100
73
74goal2d := false :- loan(20000,t,0.01,600,s) & s<=0;
75
76
77                                  1
78goal2d := false :- loan(20000,t,-----,600,s) & s <= 0
79                                 100
80
81
82clp(prog2,goal2a);
83
84
8525000000000000000000000000000000000000000000000000000000000000000000*s
86
87 - 69231216408419495739532429807393340691131328733907679880432182353696399 = 0
88
89clp(prog2,goal2b);
90
91
92430768783591580504260467570192606659308868671266092320119567817646303601*r
93
94 - 286153756718316100852093514038521331861773734253218464023913563529260720200
95
96 = 0
97
98clp(prog2,goal2c);
99
100
1011430768783591580504260467570192606659308868671266092320119567817646303601*d
102
103 - 25846127015494830255628054211556399558532120275965539207174069058778216060000
104
105 = 0
106
107clp(prog2,goal2d);
108
109
110t - 41 = 0 and
111
112250000000000000000000000000000000000000000000000000000000000000000000000000000*s
113
114 + 375237092410308372097728439755679164980769356169611980009221001478921176682\
11504101 = 0
116
117
118
119% Pythagorean triplets:
120na := {
121   nat(0) :- true,
122   nat(x+1) :- nat(x) & x>=0};
123
124
125na := {nat(0) :- true,nat(x + 1) :- nat(x) & x >= 0}
126
127
128py := append(na,{
129   pyth(x,y,z) :- nat(x) & nat(y) & nat(z) & 2<=x
130      and x<=y and y<=z and x**2+y**2=z**2});
131
132
133py := {nat(0) :- true,
134
135       nat(x + 1) :- nat(x) & x >= 0,
136
137       pyth(x,y,z) :- nat(z) & nat(y) & nat(x)
138
139                                                            2    2    2
140        & ( - x + 2 <= 0 and x - y <= 0 and y - z <= 0 and x  + y  - z  = 0)}
141
142
143clp(py, false :- pyth(3,4,z));
144
145
146z - 5 = 0
147
148clp(py, false :- pyth(9,y,z));
149
150
151z - 15 = 0 and y - 12 = 0
152
153clp(py, false :- pyth(x,y,9));
154
155
156false
157
158
159
160% Wilkonson's Polynomial:
161wi := {
162   wilk(x,e) :- (for i:=1:20 product x+i) + e*x^19 = 0};
163
164
165                       19    20        19          18            17
166wi := {wilk(x,e) :- e*x   + x   + 210*x   + 20615*x   + 1256850*x
167
168                    16               15                14                 13
169        + 53327946*x   + 1672280820*x   + 40171771630*x   + 756111184500*x
170
171                          12                    11                     10
172        + 11310276995381*x   + 135585182899530*x   + 1307535010540395*x
173
174                             9                      8                       7
175        + 10142299865511450*x  + 63030812099294896*x  + 311333643161390640*x
176
177                               6                        5
178        + 1206647803780373360*x  + 3599979517947607200*x
179
180                               4                         3
181        + 8037811822645051776*x  + 12870931245150988800*x
182
183                                2
184        + 13803759753640704000*x  + 8752948036761600000*x + 2432902008176640000
185
186        = 0}
187
188
189wi1 := clp(wi, false :- wilk(x,0) & -20 <= x <= -10);
190
191
192wi1 := x + 10 <= 0 and x + 20 >= 0 and (x + 10 = 0 or x + 11 = 0 or x + 12 = 0
193
194 or x + 13 = 0 or x + 14 = 0 or x + 15 = 0 or x + 16 = 0 or x + 17 = 0
195
196 or x + 18 = 0 or x + 19 = 0 or x + 20 = 0)
197
198wi2 := clp(wi, false :- wilk(x,2^-23) & -20 <= x <= -10);
199
200
201                                                20               19
202wi2 := x + 10 <= 0 and x + 20 >= 0 and 8388608*x   + 1761607681*x
203
204                 18                   17                    16
205 + 172931153920*x   + 10543221964800*x   + 447347234439168*x
206
207                      15                       14                        13
208 + 14028108264898560*x   + 336985244869591040*x   + 6342720331186176000*x
209
210                         12                           11
211 + 94877480085669019648*x   + 1137370949952460554240*x
212
213                            10                            9
214 + 10968398649699241820160*x   + 85079777790228273561600*x
215
216                             8                              7
217 + 528740774622641958944768*x  + 2611655889692786813829120*x
218
219                               6                               5
220 + 10122095419974470210682880*x  + 30198816984091441338777600*x
221
222                               4                                3
223 + 67426052557934862488567808*x  + 107969196810523545855590400*x
224
225                                2
226 + 115794329499468438700032000*x  + 73425049924762651852800000*x
227
228 + 20408661249006627717120000 = 0
229
230realroots(part(wi2,3,1));
231
232
233{x =  - 20.8469,
234
235 x =  - 8.91725,
236
237 x =  - 8.00727,
238
239 x =  - 6.9997,
240
241 x =  - 6.00001,
242
243 x =  - 5.0,
244
245 x =  - 4.0,
246
247 x =  - 3.0,
248
249 x =  - 2.0,
250
251 x =  - 1}
252
253rlqe rlex wi2;
254
255
256false
257
258
259
260% Minimum (uses disjunction):
261mi := {
262   min(x,y,z) :- x<=y and z=x or x>=y and z=y,
263   max(x,y,z) :- x<=y and z=y or x>=y and z=x};
264
265
266mi := {min(x,y,z)
267
268        :- ((x - y <= 0 and  - x + z = 0) or (x - y >= 0 and  - y + z = 0)),
269
270       max(x,y,z)
271
272        :- ((x - y <= 0 and  - y + z = 0) or (x - y >= 0 and  - x + z = 0))}
273
274
275clp(mi, false :- min(3,4,z));
276
277
278z - 3 = 0
279
280clp(mi, false :- min(x,y,3));
281
282
283(y - 3 >= 0 and x - 3 = 0) or (y - 3 = 0 and x - 3 >= 0)
284
285
286
287% Central projection of x on u with light source in c
288% (uses quantified constraints):
289pr := {
290   proj(c1,c2,x1,x2,u1,u2) :-
291      ex(t,t>0 and for i := 1:2 mkand mkid(u,i)=t*(mkid(x,i)-mkid(c,i)))};
292
293
294pr := {proj(c1,c2,x1,x2,u1,u2) :- ex t (t > 0
295
296        and (true and c1*t - t*x1 + u1 = 0 and c2*t - t*x2 + u2 = 0))}
297
298
299clp(pr,false :- proj(42,4711,100,1000,u1,-1));
300
301
3023711*u1 - 58 = 0
303
304
305
306% Linear theory of p-adically valued fields as another domain:
307rlset(padics,101);
308
309
310*** p is set to 101
311
312
313*** turned on switch rlsusi
314
315{r}
316
317
318
319% Detect power of 101:
320va2 := {
321   ppow(1) :- true,
322   ppow(p*x) :- ppow(x) & 1 | x};
323
324
325va2 := {ppow(1) :- true,ppow(101*x) :- ppow(x) & 1 | x}
326
327
328clp(va2, false :- ppow(12201900399479668244827490915525641902001));
329
330
331true
332
333clp(va2, false :- ppow(12201900399479668244827490915525641902002));
334
335
336false
337
338
339end;
340
341Tested on x86_64-pc-windows CSL
342Time (counter 1): 500 ms  plus GC time: 16 ms
343
344End of Lisp run after 0.51+0.10 seconds
345real 0.79
346user 0.01
347sys 0.04
348