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