tests/rtest_sign.mac

   1 (kill(all),0);
   2 0$
   3
   4 /* numbers and constants */
   5
   6 sign(minf);
   7 neg$
   8
   9 sign(-1);
  10 neg$
  11
  12 sign(-1.0);
  13 neg$
  14
  15 sign(-1.0b0);
  16 neg$
  17
  18 sign(0);
  19 zero$
  20
  21 sign(0.0);
  22 zero$
  23
  24 sign(0.0b0);
  25 zero$
  26
  27 sign(1);
  28 pos$
  29
  30 sign(1.0);
  31 pos$
  32
  33 sign(1.0b0);
  34 pos$
  35
  36 sign(inf);
  37 pos$
  38
  39 sign(%pi);
  40 pos$
  41
  42 sign(%e);
  43 pos$
  44
  45 sign(%phi);
  46 pos$
  47
  48 /* polynomials */
  49
  50 sign(x);
  51 pnz$
  52
  53 sign(x^2);
  54 pz$
  55
  56 sign(x^3);
  57 pnz$
  58
  59 sign(x^4);
  60 pz$
  61
  62 sign(x^2 + x);
  63 pnz$
  64
  65 sign(x^2 + x + 42);
  66 pos$
  67
  68 sign(x^2 + sqrt(5) + 101);
  69 pos$
  70
  71 sign(%pi * x^2 + sqrt(5) + 101);
  72 pos$
  73
  74 sign((sqrt(97) - 1) * x^2 + sqrt(5) + 101);
  75 pos$
  76
  77 sign(-x^2 + x - 42);
  78 neg$
  79
  80 sign(x^2 - 2 * x + 1);
  81 pz$
  82
  83 sign(-x^2 + 2 * x - 1);
  84 nz$
  85
  86 sign(x+y);
  87 pnz$
  88
  89 sign(x^2 + 2 * x * y + y^2);
  90 pz$
  91
  92 sign(x^2 + 2 * x * y + y^2 + 1);
  93 pos$
  94
  95 sign((x+y)^2 + (z-x)^2);
  96 pz$
  97
  98 sign(sqrt(2) * (x+y)^2 + %e * (z-x)^2);
  99 pz$
 100
 101 sign(-(x+y)^2 - (z-x)^2);
 102 nz$
 103
 104 sign(-(x+y)^2 - (z-x)^2 - %pi);
 105 neg$
 106
 107 sign(-sqrt(2) * (x+y)^2 - %phi * (z-x)^2 - %pi);
 108 neg$
 109
 110
 111 /* rational */
 112
 113 sign(1/x);
 114 pn$
 115
 116 sign(1/(x-1));
 117 pn$
 118
 119 sign(1/x + 1);
 120 pnz$
 121
 122 sign(x/(1+x^2));
 123 pnz$
 124
 125 sign(1 + x/(1+x^2));
 126 pos$
 127
 128 sign((1+x^2)/x);
 129 pn$
 130
 131 /* assumptions */
 132
 133 (assume(a < b, b < c, c < d),0);
 134 0$
 135
 136 sign(b-a);
 137 pos$
 138
 139 sign(a-b);
 140 neg$
 141
 142 sign(c-a);
 143 pos$
 144
 145 sign(a-c);
 146 neg$
 147
 148 sign(d-b);
 149 pos$
 150
 151 sign(b-d);
 152 neg$
 153
 154 sign(7*(c-a) + %pi * (d-b));
 155 pos$
 156
 157 sign(-7*(c-a) - %pi * (d-b));
 158 neg$
 159
 160 sign((b-a) * (d-a));
 161 pos$
 162
 163 sign((b-a)/(c-b));
 164 pos$
 165
 166 (forget(a < b, b < c, c < d),0);
 167 0$
 168
 169 /* algebraic */
 170
 171 sign(sqrt(x));
 172 pz$
 173
 174 sign(sqrt(x^2 + 1));
 175 pos$
 176
 177 sign(sqrt(a) + sqrt(b));
 178 pz$
 179
 180 sign(x^(1/3));
 181 pnz$
 182
 183 sign(x^(1/4));
 184 pz$
 185
 186 sign(x^(1/4) + 1);
 187 pos$
 188
 189 sign(-(x^(1/4) + 1));
 190 neg$
 191
 192 /* exp-like */
 193
 194 sign(cos(x));
 195 pnz$
 196
 197 sign(cos(x) + 42);
 198 pos$
 199
 200 sign(sin(x) - 42);
 201 neg$
 202
 203 sign(cosh(x));
 204 pos$
 205
 206 sign(cosh(x)-1);
 207 pz$
 208
 209 sign(sinh(x));
 210 pnz$
 211
 212 sign(tanh(x));
 213 pnz$
 214
 215 sign(exp(x));
 216 pos$
 217
 218 sign(exp(-x^2));
 219 pos$
 220
 221 sign(exp(-x) - 1);
 222 pnz$
 223
 224 sign(exp(-x) + 1);
 225 pos$
 226
 227 /* log-like */
 228
 229 sign(acos(x));
 230 pz$
 231
 232 sign(asin(x));
 233 pnz$
 234
 235 sign(atan(x));
 236 pnz$
 237
 238 sign(log(x));
 239 pnz$
 240
 241 (assume(x >= 1),0);
 242 0$
 243
 244 sign(log(x));
 245 pz$
 246
 247 (forget(x >= 1),0);
 248 0$
 249
 250 sign(acosh(x));
 251 pz$
 252
 253 sign(asinh(x));
 254 pnz$
 255
 256 sign(tanh(x));
 257 pnz$
 258
 259 (assume(x >= -1), assume(x < 1),0);
 260 0$
 261
 262 sign(acos(x));
 263 pos$
 264
 265 (forget(x >= -1), forget(x < 1),0);
 266 0$
 267
 268 (assume(x > 0), assume(x <= 1),0);
 269 0$
 270
 271 sign(asin(x));
 272 pos$
 273
 274 sign(atanh(x));
 275 pos$
 276
 277 (forget(x > 0), forget(x <= 1),0);
 278 0$
 279
 280 (assume(x >= -1), assume(x <= 0),0);
 281 0$
 282
 283 sign(asin(x));
 284 nz$
 285
 286 sign(atanh(x));
 287 nz$
 288
 289 (forget(x >= -1), forget(x <= 0),0);
 290 0$
 291
 292 /* expt */
 293 (assume(xpos > 0), assume(xneg < 0), assume(xpz >= 0), assume(xnz <= 0), assume(notequal(xpn, 0)), assume(equal(xzero, 0)), declare(xeven, even), declare(xodd, odd),0);
 294 0$
 295
 296 create_list(errcatch(sign(x^y)),
 297             x, [xpos, xneg, xpz, xnz, xpn, xzero, xpnz],
 298             y, [xpos, xneg, xpz, xnz, xpn, xzero, xpnz, xeven, xodd]);
 299 [[pos], [pos], [pos], [pos], [pos], [pos], [pos], [pos], [pos],   /* xpos^y */
 300  [pn], [pn], [pn], [pn], [pn], [pos], [pn], [pos], [neg],         /* xneg^y */
 301  [pz], [pos], [pz], [pos], [pz], [pos], [pz], [pz], [pz],         /* xpz^y */
 302  [pnz], [pn], [pnz], [pn], [pnz], [pos], [pnz], [pz], [nz],       /* xnz^y */
 303  [pn], [pn], [pn], [pn], [pn], [pos], [pn], [pos], [pn],          /* xpn^y */
 304  [zero], [], [zero], [], [zero], [], [zero], [zero], [zero],      /* xzero^y */
 305  [pnz], [pn], [pnz], [pn], [pnz], [pos], [pnz], [pz], [pnz]]$     /* xpnz^y */
 306
 307 (forget(xpos > 0), forget(xneg < 0), forget(xpz >= 0), forget(xnz <= 0), forget(notequal(xpn, 0)), forget(equal(xzero, 0)), remove(xeven, even), remove(xodd, odd),0);
 308 0$
 309
 310 /* SF bug 798571 */
 311
 312 sign(sqrt(2)/2 - 1/sqrt(2));
 313 zero$
 314
 315 /* SF bug 1045920
 316  * This case is fixed in compar.lisp revision 1.76.
 317  * Adding some more examples.
 318  */
 319
 320 (assume(a > 1, b > 1),0);
 321 0$
 322
 323 sign(a+b-2);
 324 pos;
 325 sign(2*a+b-3);
 326 pos;
 327 sign(2*a+b-4);
 328 pnz;
 329
 330 (forget(a > 1, b > 1),0);
 331 0$
 332
 333 (assume(a < -1, b < -1),0);
 334 0$
 335
 336 sign(a+b+2);
 337 neg;
 338 sign(2*a+b+3);
 339 neg;
 340 sign(2*a+b+4);
 341 pnz;
 342
 343 (forget(x < -1, y < -1),0);
 344 0;
 345
 346 /* SF bug 1724592  */
 347
 348 (aaa : 'bbb, bbb : 'ccc, ccc : 23.5,0);
 349 0$
 350
 351 sign(1.0*aaa);
 352 pnz$
 353
 354 sign(1.0*bbb);
 355 pnz$
 356
 357 (remvalue(aaa, bbb, ccc),0);
 358 0$
 359
 360 assume(x32 > 3/2);
 361 [x32 > 3/2];
 362
 363 kill(all);
 364 done;
 365
 366 assume(x32 < 1);
 367 [x32 < 1];
 368
 369 /* [ 1981623 ] wrong sign of sqrt() */
 370 (assume(xx >= 0, xx <= 1), 0);
 371 0$
 372
 373 sqrt(a/(xx-1)^2);
 374 sqrt(a)/(1-xx);
 375
 376
 377 /*****************************************************************************
 378
 379  Add tests for the function $csign
 380
 381  First: We repeat all tests which give a correct result for $sign.
 382         The tests which are expected to fail are commented out.
 383
 384 ******************************************************************************/
 385
 386 (kill(all),0);
 387 0$
 388
 389 /* numbers and constants */
 390
 391 csign(minf);
 392 neg$
 393
 394 csign(-1);
 395 neg$
 396
 397 csign(-1.0);
 398 neg$
 399
 400 csign(-1.0b0);
 401 neg$
 402
 403 csign(0);
 404 zero$
 405
 406 csign(0.0);
 407 zero$
 408
 409 csign(0.0b0);
 410 zero$
 411
 412 csign(1);
 413 pos$
 414
 415 csign(1.0);
 416 pos$
 417
 418 csign(1.0b0);
 419 pos$
 420
 421 csign(inf);
 422 pos$
 423
 424 csign(%pi);
 425 pos$
 426
 427 csign(%e);
 428 pos$
 429
 430 csign(%phi);
 431 pos$
 432
 433 /* polynomials */
 434
 435 csign(x);
 436 pnz$
 437
 438 csign(x^2);
 439 pz$
 440
 441 csign(x^3);
 442 pnz$
 443
 444 csign(x^4);
 445 pz$
 446
 447 csign(x^2 + x);
 448 pnz$
 449
 450 csign(x^2 + x + 42);
 451 pnz$
 452
 453 csign(x^2 + sqrt(5) + 101);
 454 pos$
 455
 456 csign(%pi * x^2 + sqrt(5) + 101);
 457 pos$
 458
 459 csign((sqrt(97) - 1) * x^2 + sqrt(5) + 101);
 460 pos$
 461
 462 csign(-x^2 + x - 42);
 463 pnz$
 464
 465 csign(x^2 - 2 * x + 1);
 466 pz$
 467
 468 csign(-x^2 + 2 * x - 1);
 469 nz$
 470
 471 csign(x+y);
 472 pnz$
 473
 474 csign(x^2 + 2 * x * y + y^2);
 475 pz$
 476
 477 csign(x^2 + 2 * x * y + y^2 + 1);
 478 pos$
 479
 480 csign((x+y)^2 + (z-x)^2);
 481 pz$
 482
 483 csign(sqrt(2) * (x+y)^2 + %e * (z-x)^2);
 484 pz$
 485
 486 csign(-(x+y)^2 - (z-x)^2);
 487 nz$
 488
 489 csign(-(x+y)^2 - (z-x)^2 - %pi);
 490 neg$
 491
 492 csign(-sqrt(2) * (x+y)^2 - %phi * (z-x)^2 - %pi);
 493 neg$
 494
 495
 496 /* rational */
 497
 498 csign(1/x);
 499 pn$
 500
 501 csign(1/(x-1));
 502 pn$
 503
 504 csign(1/x + 1);
 505 pnz$
 506
 507 csign(x/(1+x^2));
 508 pnz$
 509
 510 csign(1 + x/(1+x^2));
 511 pnz$
 512
 513 csign((1+x^2)/x);
 514 pn$
 515
 516 /* assumptions */
 517
 518 (assume(a < b, b < c, c < d),0);
 519 0$
 520
 521 csign(b-a);
 522 pos$
 523
 524 csign(a-b);
 525 neg$
 526
 527 csign(c-a);
 528 pos$
 529
 530 csign(a-c);
 531 neg$
 532
 533 csign(d-b);
 534 pos$
 535
 536 csign(b-d);
 537 neg$
 538
 539 csign(7*(c-a) + %pi * (d-b));
 540 pos$
 541
 542 csign(-7*(c-a) - %pi * (d-b));
 543 neg$
 544
 545 csign((b-a) * (d-a));
 546 pos$
 547
 548 csign((b-a)/(c-b));
 549 pos$
 550
 551 (forget(a < b, b < c, c < d),0);
 552 0$
 553
 554 /* algebraic */
 555
 556 csign(sqrt(x));
 557 complex$
 558
 559 csign(sqrt(x^2 + 1));
 560 pos$
 561
 562 csign(sqrt(a) + sqrt(b));
 563 complex$
 564
 565 csign(x^(1/3));
 566 pnz$
 567
 568 csign(x^(1/4));
 569 complex$
 570
 571 csign(x^(1/4) + 1);
 572 complex$
 573
 574 csign(-(x^(1/4) + 1));
 575 complex$
 576
 577 /* exp-like */
 578
 579 csign(cos(x));
 580 pnz$
 581
 582 csign(cos(x) + 42);
 583 pos$
 584
 585 csign(sin(x) - 42);
 586 neg$
 587
 588 csign(cosh(x));
 589 pos$
 590
 591 csign(cosh(x)-1);
 592 pz$
 593
 594 csign(sinh(x));
 595 pnz$
 596
 597 csign(tanh(x));
 598 pnz$
 599
 600 csign(exp(x));
 601 pos$
 602
 603 csign(exp(-x^2));
 604 pos$
 605
 606 csign(exp(-x) - 1);
 607 pnz$
 608
 609 csign(exp(-x) + 1);
 610 pos$
 611
 612 /* log-like */
 613
 614 csign(acos(x));
 615 complex$
 616
 617 csign(asin(x));
 618 complex$
 619
 620 csign(atan(x));
 621 pnz$
 622
 623 csign(log(x));
 624 complex$
 625
 626 (assume(x > 0),0);
 627 0$
 628
 629 csign(log(x));
 630 pnz$
 631
 632 (forget(x > 0),0);
 633 0$
 634
 635 (assume(x >= 1),0);
 636 0$
 637
 638 csign(log(x));
 639 pz$
 640
 641 (forget(x >= 1),0);
 642 0$
 643
 644 csign(acosh(x));
 645 complex$
 646
 647 csign(asinh(x));
 648 pnz$
 649
 650 csign(atanh(x));
 651 complex$
 652
 653 (assume(x >= -1), assume(x <= 1),0);
 654 0$
 655
 656 csign(acos(x));
 657 pz$
 658
 659 csign(asin(x));
 660 pnz$
 661
 662 csign(atanh(x));
 663 pnz$
 664
 665 (forget(x >= -1), forget(x <= 1),0);
 666 0$
 667
 668 (assume(x >= -1), assume(x < 1),0);
 669 0$
 670
 671 csign(acos(x));
 672 pos$
 673
 674 (forget(x >= -1), forget(x < 1),0);
 675 0$
 676
 677 (assume(x > 0), assume(x <= 1),0);
 678 0$
 679
 680 csign(asin(x));
 681 pos$
 682
 683 csign(atanh(x));
 684 pos$
 685
 686 (forget(x > 0), forget(x <= 1),0);
 687 0$
 688
 689 (assume(x >= -1), assume(x <= 0),0);
 690 0$
 691
 692 csign(asin(x));
 693 nz$
 694
 695 csign(atanh(x));
 696 nz$
 697
 698 (forget(x >= -1), forget(x <= 0),0);
 699 0$
 700
 701 /* expt */
 702 (assume(xpos > 0), assume(xneg < 0), assume(xpz >= 0), assume(xnz <= 0), assume(notequal(xpn, 0)), assume(equal(xzero, 0)),
 703  declare(xeven, even), declare(xodd, odd), declare(ximag, imaginary), declare(xcomplex, complex),0);
 704 0$
 705
 706 create_list(errcatch(csign(x^y)),
 707             x, [xpos, xneg, xpz, xnz, xpn, xzero, xpnz, ximag, xcomplex],
 708             y, [xpos, xneg, xpz, xnz, xpn, xzero, xpnz, xeven, xodd, ximag, xcomplex]);
 709 [[pos], [pos], [pos], [pos], [pos], [pos], [pos], [pos], [pos], [complex], [complex],                         /* xpos^y */
 710  [complex], [complex], [complex], [complex], [complex], [pos], [complex], [pos], [neg], [complex], [complex], /* xneg^y */
 711  [pz], [pos], [pz], [pos], [pz], [pos], [pz], [pz], [pz], [complex], [complex],                               /* xpz^y */
 712  [complex], [complex], [complex], [complex], [complex], [pos], [complex], [pz], [nz], [complex], [complex],   /* xnz^y */
 713  [complex], [complex], [complex], [complex], [complex], [pos], [complex], [pos], [pn], [complex], [complex],  /* xpn^y */
 714  [zero], [], [zero], [], [zero], [], [zero], [zero], [zero], [zero], [zero],                                  /* xzero^y */
 715  [complex], [complex], [complex], [complex], [complex], [pos], [complex], [pz], [pnz], [complex], [complex],  /* xpnz^y */
 716  [complex], [complex], [complex], [complex], [complex], [pos], [complex], [complex], [complex], [complex], [complex], /* ximag^y */
 717  [complex], [complex], [complex], [complex], [complex], [pos], [complex], [complex], [complex], [complex], [complex]]$  /* xcomplex^y */
 718
 719 (forget(xpos > 0), forget(xneg < 0), forget(xpz >= 0), forget(xnz <= 0), forget(notequal(xpn, 0)), forget(equal(xzero, 0)),
 720  remove(xeven, even), remove(xodd, odd), remove(ximag, imaginary), remove(xcomplex, complex),0);
 721 0$
 722
 723 /* SF bug 798571 */
 724
 725 csign(sqrt(2)/2 - 1/sqrt(2));
 726 zero$
 727
 728 /* SF bug 1045920 */
 729
 730 (assume(a > 1, b > 1),0);
 731 0$
 732
 733 csign(a + b -2);
 734 pos$
 735
 736 (forget(a > 1, b > 1),0);
 737 0$
 738
 739 /* SF bug 1724592  */
 740
 741 (aaa : 'bbb, bbb : 'ccc, ccc : 23.5,0);
 742 0$
 743
 744 csign(1.0*aaa);
 745 pnz$
 746
 747 csign(1.0*bbb);
 748 pnz$
 749
 750 (remvalue(aaa, bbb, ccc),0);
 751 0$
 752
 753 assume(x32 > 3/2);
 754 [x32 > 3/2];
 755
 756 kill(all);
 757 done;
 758
 759 assume(x32 < 1);
 760 [x32 < 1];
 761
 762 /******************************************************************************
 763   Second: $csign with complex expressions.
 764 ******************************************************************************/
 765
 766 declare(n,integer,x,real,j,imaginary,z,complex);
 767 done;
 768
 769 /* We test the constants. UND and IND do not give a result, but an error. */
 770 map(csign, [%e,%gamma,%phi,%i, minf,inf,infinity]);
 771 [pos,pos,pos,imaginary,neg,pos,complex];
 772
 773 /* Symbols declcared as integeger, real, imaginary or complex */
 774 map(csign, [n,x,j,z]);
 775 [pnz,pnz,imaginary,complex];
 776
 777 /* Some arithmetic with pure imaginary numbers and symbols */
 778
 779 map(csign,[%i,sqrt(-1),10*%i,x*%i,%i^2,%i^3,%i^4,%i^5]);
 780 [imaginary,imaginary,imaginary,imaginary,neg,imaginary,pos,imaginary];
 781
 782 map(csign,[j,sqrt(-1),10*j,x*j,j^2,j^3,j^4,j^5]);
 783 [imaginary,imaginary,imaginary,imaginary,nz,imaginary,pz,imaginary];
 784
 785 /* negative base and half integral exponent */
 786 map(csign,[(-1)^(1/2),(-1)^(3/2),(-1)^(5/2), (-1)^(7/2), (-1)^(9/2)]);
 787 [imaginary,imaginary,imaginary,imaginary,imaginary];
 788
 789 /* the same with an negative expression */
 790 (assume(xneg < 0, xpos>0),done);
 791 done;
 792 map(csign,[(xneg)^(1/2),(xneg)^(3/2),(xneg)^(5/2),(xneg)^(7/2)]);
 793 [imaginary,imaginary,imaginary,imaginary];
 794
 795 map(csign,[(-xpos)^(1/2),(-xpos)^(3/2),(-xpos)^(5/2),(-xpos)^(7/2)]);
 796 [imaginary,imaginary,imaginary,imaginary];
 797
 798 map(csign,[(-1)^xpos, (-1)^xneg]);
 799 [complex,complex];
 800
 801 map(sign,[(-1)^xpos, (-1)^xneg]);
 802 [pn,pn];
 803
 804 /* Expressions with an addition */
 805
 806 csign(x+%i*y);
 807 complex;
 808 csign((x+%i*y)^2);
 809 complex;
 810 csign((x+%i*y)^(1/2));
 811 complex;
 812
 813 csign((a+x+%i*y)/(b-y*%i));
 814 complex;
 815
 816 /* More expressions */
 817
 818 csign(1/z);
 819 complex;
 820 csign(1/j);
 821 imaginary;
 822 csign(10*a+c/z);
 823 complex;
 824 csign(10*a+c/j);
 825 complex;
 826 csign((10*a+(c/j)^2)^n);
 827 pnz;
 828 csign((10*a+(c/j)^3)^n);
 829 complex;
 830
 831 /* This does not work correctly.
 832    The answer complex is not really wrong, but could be better.
 833    To achieve this we have first to improve the function rectform. */
 834
 835 csign((1+%i)*(1-%i));
 836 complex; /* should be pos */
 837
 838 csign(expand((1+%i)*(1-%i)));
 839 pos; /* after expansion correct */
 840
 841 /* Functions which are declared to be complex give the sign $complex */
 842
 843 csign(conjugate(z));
 844 complex;
 845 csign(conjugate(x)); /* x is real */
 846 pnz;
 847
 848 declare(f,complex);
 849 done;
 850 csign(f(x));
 851 complex;
 852
 853 /* realpart and imagpart are real valued */
 854
 855 csign(realpart(z));
 856 pnz;
 857 csign(imagpart(z));
 858 pnz;
 859
 860 /*
 861  * Examples for assumptions with abs(x)<a, a is positive
 862  *
 863  */
 864
 865 kill(all);
 866 done;
 867
 868 assume(abs(x)<1);
 869 [abs(x)<1];
 870
 871 sign(1-x);
 872 pos;
 873 sign(2-x);
 874 pos;
 875 sign(x-1);
 876 neg;
 877 sign(x-2);
 878 neg;
 879
 880 forget(abs(x)<1);
 881 [abs(x)<1];
 882
 883 facts();
 884 [];
 885
 886 assume(a>0,abs(x)<a);
 887 [a>0,a>abs(x)];
 888
 889 sign(a-x);
 890 pos;
 891 sign(x-a);
 892 neg;
 893
 894 forget(abs(x)<a);
 895 [a>abs(x)];
 896
 897 facts();
 898 [a>0];
 899
 900 assume(a*abs(x)<1);
 901 [a*abs(x)<1];
 902
 903 sign(1/a-x);
 904 pos;
 905 sign(x-1/a);
 906 neg;
 907
 908 forget(a*abs(x)<1);
 909 [a*abs(x)<1];
 910
 911 assume(abs(x)<2*a+1);
 912 [2*a-abs(x)+1>0];
 913
 914 sign(2*a+1-x);
 915 pos;
 916 sign(2*a+1+x);
 917 pos;
 918 sign(a*(2*a+1-x));
 919 pos;
 920
 921 forget(abs(x)<2*a+1);
 922 [2*a-abs(x)+1>0];
 923
 924 facts();
 925 [a>0];
 926
 927 assume(b>0,b<1);
 928 [b>0,b<1];
 929
 930 assume(abs(x)<b);
 931 [b>abs(x)];
 932
 933 is(x<1);
 934 true;
 935 sign(1-x);
 936 pos;
 937 sign(x-1);
 938 neg;
 939
 940 forget(abs(x)<b);
 941 [b>abs(x)];
 942
 943 facts();
 944 [a>0,b>0,1>b];
 945
 946 assume(sin(abs(x)) < 1);
 947 [sin(abs(x))<1];
 948
 949 sign(1-sin(x));
 950 pos;
 951 sign(2-sin(x));
 952 pos;
 953 sign(sin(x)-1);
 954 neg;
 955 sign(sin(x)-2);
 956 neg;
 957
 958 forget(sin(abs(x)) < 1);
 959 [sin(abs(x))<1];
 960
 961 assume(cos(abs(x)) < 1);
 962 [cos(abs(x))<1];
 963
 964 sign(1-cos(x));
 965 pos;
 966 sign(2-cos(x));
 967 pos;
 968 sign(cos(x)-1);
 969 neg;
 970 sign(cos(x)-2);
 971 neg;
 972
 973 forget(cos(abs(x)) < 1);
 974 [cos(abs(x))<1];
 975
 976 assume(abs(sin(x)) < 1);
 977 [abs(sin(x))<1];
 978
 979 sign(1-sin(x));
 980 pos;
 981 sign(2-sin(x));
 982 pos;
 983 sign(sin(x)-1);
 984 neg;
 985 sign(sin(x)-2);
 986 neg;
 987
 988 forget(abs(sin(x)) < 1);
 989 [abs(sin(x))<1];
 990
 991 assume(abs(cos(x)) < 1);
 992 [abs(cos(x))<1];
 993
 994 sign(1-cos(x));
 995 pos;
 996 sign(2-cos(x));
 997 pos;
 998 sign(cos(x)-1);
 999 neg;
1000 sign(cos(x)-2);
1001 neg;
1002
1003 forget(abs(cos(x)) <1);
1004 [abs(cos(x))<1];
1005
1006 csign(log((1 + %i)/sqrt(2)));
1007 imaginary$
1008
1009 /* Examples to show that learn-numer works
1010  * Related bug report:
1011  * Bug ID: 2477795 - "assume":problems with fractions or multiples of %pi and %e
1012  */
1013 kill(all);
1014 done;
1015 assume(a>0,a<%pi/2);
1016 [a>0,%pi/2>a];
1017
1018 is(a>%pi/2);
1019 false;
1020 is(a>%pi);
1021 false;
1022
1023 assume(b>0,b<2*%pi);
1024 [b>0, 2*%pi>b];
1025 is(b>3*%pi);
1026 false;
1027
1028 /* An example involving a numerical constant, the value of a function
1029  * and the abs function.
1030  * This example no longer works because of revision 1.62 of compar.lisp
1031  */
1032 assume(abs(x) < sin(1)+%e/2);
1033 [sin(1)+%e/2>abs(x)];
1034 is(x<2*%e);
1035 true;
1036 is(x>-2*%e);
1037 true;
1038 (forget(abs(x)<sin(1)+%e/2),done);
1039 done;
1040
1041 /* Bug ID: 2876382 - sign(a+b+sin(1)) unknown */
1042 (assume(a>0,b>0),done);
1043 done;
1044 sign(a+b+sin(1));
1045 pos;
1046 (forget(a>0,b>0),done);
1047 done;
1048
1049 /* Bug ID: 2184396 - Wrong factorization of sqrt()
1050  * This is the example from the bug report which has triggered the bug in sign
1051  *      sqrt(1-(2-sqrt(2))/x * ((2+sqrt(2))/x-1));
1052  * The expression has factored wrongly. This example is now correct.
1053  */
1054 sign(1-(1+sqrt(2))*x);
1055 'pnz;
1056 sign(1-(1+sqrt(2))/x);
1057 'pnz;
1058
1059 /* Bug ID: 1038624 - askinteger ignores asksign database
1060  * With revision 1.64 of compar.lisp code has been added, which looks for
1061  * integer and noninteger facts into the database.
1062  */
1063 (assume(equal(a,0), equal(b,2), equal(c,1/3), equal(d,1.5), equal(e,3.0b0)),
1064  done);
1065 done;
1066
1067 map(askinteger, [a, b, 2*b, 2+b, c, d, e]);
1068 [yes, yes, yes, yes, no, no, no];
1069
1070
1071 (forget(equal(a,0), equal(b,2), equal(c,1/3), equal(d,1.5), equal(e,3.0b0)),
1072  done);
1073 done;
1074
1075 /* Bug ID: 3376603 - sign of declared imaginary */
1076 declare(f,imaginary, g,complex);
1077 done$
1078 csign(f(x));
1079 imaginary$
1080 csign(g(x));
1081 complex$
1082 kill(f,g);
1083 done$
1084
1085 /* Check adding new equaltiy does not make old inequality disappear */
1086 kill(all);
1087 done;
1088
1089 assume(notequal(a,b));
1090 [notequal(a, b)];
1091
1092 is(equal(a,b));
1093 false;
1094
1095 (assume(equal(a, x+y)), 0);
1096 0;
1097
1098 is(equal(a,b));
1099 false;
1100
1101 /* Check fix for bug 2547 (declare constant messes up sign calculations) */
1102 (declare (x, constant), declare (y, constant), assume (x > y), is (x>y));
1103 true$
1104
1105 /* facts in assume database not cleaned up by 'sign' */
1106
1107 (kill (foo), foo : %e^(abs(uu)+uu)*(uu/abs(uu)+1)+%e^(abs(uu)-uu)*(uu/abs(uu)-1), 0);
1108 0;
1109
1110 block ([bar, baz], bar : copy (facts (initial)), is (equal (foo, 0)), baz : facts (initial), is (bar = baz));
1111 true;
1112
1113 /* tnx to Barton Willis for the next couple of tests */
1114
1115 map('sign,[sqrt(x),x]);
1116 [pz, pnz];
1117
1118 (kill(buddy),
1119  buddy(p,q) := expand(if p >= 0 then q else q,0,0),
1120  buddy(sqrt(x),abs(x)));
1121 abs(x);
1122
1123 /* Ensure that asksign1 deals correctly with squared expressions */
1124 (assume (notequal(n, 1)), 0);
1125 0$
1126
1127 is ((n-1)^2 > 0);
1128 true$
1129
1130 /* Here are some calls to asksign & askinteger -- these don't cause
1131  * an interactive prompt. Interactive examples are in rtest_ask.mac.
1132  */
1133
1134 map(askinteger,[0,1/2,sqrt(17)]);
1135 [yes,no,no]$
1136
1137 /* Known constants */
1138 map(askinteger,[%pi,%e,%phi,%gamma,%i]);
1139 [no,no,no,no,no]$
1140
1141 map(asksign,[%pi,%e,%phi,%gamma,inf,minf]);
1142 [pos,pos,pos,pos,pos,neg]$
1143
1144 errcatch(asksign(%i));
1145 []$ /* argument cannot be imaginary. */
1146
1147 errcatch(asksign(infinity));
1148 []$ /* sign of infinity is undefined. */
1149
1150 /* Odd functions */
1151
1152 (declare(o, oddfun),0);
1153 0$
1154
1155 (assume(equal(q, 0)),0);
1156 0$
1157
1158 sign(o(q));
1159 zero$
1160
1161 (remove(o, oddfun),0);
1162 0$
1163
1164 (forget(equal(q, 0)),0);
1165 0$
1166
1167 /* Increasing and decreasing functions */
1168
1169 (declare(i, increasing, d, decreasing),0);
1170 0$
1171
1172 (assume(r > q),0);
1173 0$
1174
1175 is(i(r) > i(q));
1176 true$
1177
1178 is(d(r) < d(q));
1179 true$
1180
1181 (remove(i, increasing, d, decreasing),0);
1182 0$
1183
1184 (forget(r > q), 0);
1185 0$
1186
1187 /* Increasing and decreasing odd functions */
1188
1189 (declare(i, [oddfun, increasing], d, [oddfun, decreasing]),0);
1190 0$
1191
1192 (assume(q < 0, r > 0),0);
1193 0$
1194
1195 sign(i(q));
1196 neg$
1197
1198 sign(i(r));
1199 pos$
1200
1201 sign(d(q));
1202 pos$
1203
1204 sign(d(r));
1205 neg$
1206
1207 (remove(i, [oddfun, increasing], d, [oddfun, decreasing]),0);
1208 0$
1209
1210 (forget(q < 0, r > 0),0);
1211 0$
1212
1213 /* Bug #3109: is(sin(x) <= 1) returns "unknown", is(sin(x) <= 1.00001) returns "true" */
1214 (kill(all),0);
1215 0$
1216 is(sin(x) <= 1);
1217 true$
1218 is(cos(x) <= 1);
1219 true$
1220 is(sin(x) >= -1);
1221 true$
1222 is(cos(x) >= -1);
1223 true$
1224 sign(sin(x)+1);
1225 pz$
1226 sign(cos(x)+1);
1227 pz$
1228 sign(sin(x)-1);
1229 nz$
1230 sign(cos(x)-1);
1231 nz$
1232
1233 /* Assumptions and queries involving multiple unknowns */
1234 assume(-2*x*y>10);
1235 [x*y<-5]$
1236 is(10*x*y<-50);
1237 true$
1238 assume(3*x*y>0);
1239 [inconsistent]$
1240 assume(notequal(2*a*b,10));
1241 [notequal(a*b,5)]$
1242 is(equal(10*a*b,50));
1243 false$
1244 (kill(all),0);
1245 0$
1246
1247 /* Exponents in inequality assumptions and queries  */
1248 assume(x^3/y>=0);
1249 [x*y>=0]$
1250 sign(y^3/x);
1251 pz$
1252 (declare(e, even, o, odd), 0);
1253 0$
1254 assume(a^o>0);
1255 [a>0]$
1256 sign(-2*a^o);
1257 neg$
1258 assume(b^(e+1)<0);
1259 [b<0]$
1260 sign(-b^(e+1));
1261 pos$
1262 assume(c^m/d^n<=0);
1263 [c^m*d^n<=0]$
1264 assume(f^(1/3)*g^h<0);
1265 [f*g^h<0]$
1266 (kill(all),0);
1267 0$
1268
1269 /* The csign of a product with a complex factor and a zero factor used
1270  * to depend on the order of the factors: if the zero came first then
1271  * the sign was zero, but if the complex came first then the sign was
1272  * complex.
1273  */
1274
1275 (declare (a, complex), assume (equal (b, 0)), 0)$
1276 0;
1277 csign (a * b);
1278 zero;
1279 (remove (a, complex), forget (equal (b, 0)), 0)$
1280 0;
1281
1282 (declare (b, complex), assume (equal (a, 0)), 0)$
1283 0;
1284 csign (a * b);
1285 zero;
1286 (remove (b, complex), forget (equal (a, 0)), 0)$
1287 0;
1288
1289 /* SF bug report #3583: "Stack overflow for equality testing with assumptions" */
1290
1291 (domain: real,
1292  myctxt: newcontext (),
1293  assume (x > 0, y > 0),
1294  is(equal(y*(x-y),0)));
1295 unknown;
1296
1297 (domain: complex,
1298  is(equal(y*(x-y),0)));
1299 unknown;
1300
1301 (killcontext (myctxt),
1302  remvalue(myctxt),
1303  reset (domain));
1304 [domain];
1305
1306 /* Bug #3417: sign(1/zero) => 0 (where equal(zero,0)) */
1307
1308 (assume (equal (zero, 0), equal (q, r)), 0)$
1309 0;
1310
1311 errcatch (sign (1 / (q - r)))$
1312 [];
1313
1314 /* This used to return zero */
1315 errcatch (sign (1 / zero))$
1316 [];
1317
1318 (forget (equal (zero, 0), equal (q, r)), 0)$
1319 0;
1320
1321 /* bug reported to mailing list 2021-06-27: "ev(xxx,pred) vs is(xxx)" */
1322
1323 xxx:  '((0 < 1) or (0 < 2));
1324 (0 < 1) or (0 < 2);
1325
1326 ev(xxx, pred);
1327 true;
1328
1329 ev(xxx, nouns);
1330 true;
1331
1332 is(xxx);
1333 true;
1334
1335 yyy: '((0 < 1) and (0 < 2));
1336 (0 < 1) and (0 < 2);
1337
1338 is(yyy);
1339 true;
1340
1341 zzz: '((0 > 1) or (0 < 2));
1342 (0 > 1) or (0 < 2);
1343
1344 is(zzz);
1345 true;
1346
1347 aaa: '((0 > 1) and (0 < 2));
1348 (0 > 1) and (0 < 2);
1349
1350 is(aaa);
1351 false;
1352
1353 bbb: '((0 > 1) or (0 > 2));
1354 (0 > 1) or (0 > 2);
1355
1356 is(bbb);
1357 false;
1358
1359 (kill(xyz), ccc: '((xyz > 4) or (3 > 2)));
1360 (xyz > 4) or (3 > 2);
1361
1362 is(ccc);
1363 true;
1364
1365 ddd: '((2 < 1) or (2 < 2) or (1 < 3) and (2 < 4));
1366 (2 < 1) or (2 < 2) or ((1 < 3) and (2 < 4));
1367
1368 is(ddd);
1369 true;
1370
1371 /* SF bug #3324: "Stack overflow in sign() when domain complex" */
1372
1373 (kill(a, b, c, xxx, yyy, zzz, aaa, bbb, ccc, ddd),
1374  domain: complex,
1375  declare([a,b,c], real),
1376  mycontext: newcontext (),
1377  assume(a>0, b>0, c>0),
1378  sign(c - b^(1/3)*c^(1/3)));
1379 pnz;
1380
1381 sign(c - (b*c)^(1/3));
1382 pnz;
1383
1384 (killcontext (mycontext), remvalue(mycontext),0);
1385 0;
1386
1387 /* SF bug #3440: "complex domain + real variable = seg-fault"
1388  * possibly related to #3324
1389  */
1390
1391 (kill (m1, m2, m3, r12, r13, r23, A),
1392  mycontext: newcontext (),
1393  domain:complex,
1394  declare([m1,m2,m3],real),
1395  declare([r12,r13,r23],real),
1396  assume(r12>0,r13>0,r23>0),
1397  assume(r12<r13+r23,r13<r12+r23,r23<r12+r13),
1398  assume(m1>0,m2>0,m3>0),
1399  A : (-((((-r23^2)+r13^2+r12^2)*(r23^2-r13^2+r12^2))/((m2+m1)*r12^2*r13*r23)+(2*((-r23^2)-r13^2+r12^2))/(m3*r13*r23))^2/(4*((4*(m3+m1))/(m1*m3)-(m2*((-r23^2)+r13^2+r12^2)^2)/(m1*(m2+m1)*r12^2*r13^2))))-(m1*(r23^2-r13^2+r12^2)^2)/(4*m2*(m2+m1)*r12^2*r23^2)+(m3+m2)/(m2*m3),
1400  is(equal(A,0)));
1401 unknown;
1402
1403 (reset (),
1404  killcontext (mycontext),
1405  remvalue(A),
1406  remvalue(mycontext), 0);
1407 0;
1408
1409 /* SF bug #4120: is("foo"<3) gives internal error */
1410
1411 block ([prederror: false], is("foo"<3));
1412 false;
1413
1414 errcatch (block ([prederror: true], is("foo"<3)));
1415 [];
1416
1417 block ([prederror: false], is(3 < "foo"));
1418 false;
1419
1420 errcatch (block ([prederror: true], is(3 < "foo")));
1421 [];
1422
1423 block ([prederror: false],
1424        kill (foo),
1425        [is ("foo" < 3), is ("foo" < foo), is ("foo" < sin (foo))]);
1426 [false, false, false];
1427
1428 block ([prederror: true],
1429        [errcatch (is ("foo" < 3)), errcatch (is ("foo" < foo)), errcatch (is ("foo" < sin (foo)))]);
1430 [[], [], []];
1431
1432 block ([prederror: false], is("foo"<=3));
1433 false;
1434
1435 errcatch (block ([prederror: true], is("foo"<=3)));
1436 [];
1437
1438 block ([prederror: false], is(3 <= "foo"));
1439 false;
1440
1441 errcatch (block ([prederror: true], is(3 <= "foo")));
1442 [];
1443
1444 block ([prederror: false],
1445        [is ("foo" <= 3), is ("foo" <= foo), is ("foo" <= sin (foo))]);
1446 [false, false, false];
1447
1448 block ([prederror: true],
1449        [errcatch (is ("foo" <= 3)), errcatch (is ("foo" <= foo)), errcatch (is ("foo" <= sin (foo)))]);
1450 [[], [], []];
1451
1452 block ([prederror: false],
1453        [is ("abc" > "ab"), is ("abc" > "abc"), is ("abc" > "abcd")]);
1454 [true, false, false];
1455
1456 block ([prederror: true],
1457        [is ("abc" > "ab"), is ("abc" > "abc"), is ("abc" > "abcd")]);
1458 [true, false, false];
1459
1460 block ([prederror: false],
1461        [is ("abc" >= "ab"), is ("abc" >= "abc"), is ("abc" >= "abcd")]);
1462 [true, true, false];
1463
1464 block ([prederror: true],
1465        [is ("abc" >= "ab"), is ("abc" >= "abc"), is ("abc" >= "abcd")]);
1466 [true, true, false];
1467
1468 block ([prederror: false], sort (["xyz", "xy", "vwxy", "vw", "uvwxyz", "uv"], ">"));
1469 ["xyz", "xy", "vwxy", "vw", "uvwxyz", "uv"];
1470
1471 /* Consistency check for `is(expr >= 0)` and `sign(expr)` */
1472
1473 is(sqrt(x) >= 0);
1474 true$
1475
1476 /* Tests for sign-cos & sign-sin */
1477 sign(sin(x^2+1));
1478 pnz$
1479
1480 sign(sin(z));
1481 pnz$
1482
1483 block([ans], assume(0 < z, z < %pi), ans : sign(sin(z)), forget(0 < z, z < %pi), ans);
1484 pos$
1485
1486 block([ans], assume(0 <= z, z <= %pi), ans : sign(sin(z)), forget(0 <= z, z <= %pi), ans);
1487 pz$
1488
1489 block([ans], assume(0 < z, z < %pi), ans : sign(sin(z)), forget(0 < z, z < %pi), ans);
1490 pos$
1491
1492 block([ans], assume(-%pi < z, z < 0), ans : sign(sin(z)), forget(-%pi < z, z < 0), ans);
1493 neg$
1494
1495 block([ans], assume(-%pi <= z, z <= 0), ans : sign(sin(z)), forget(-%pi <= z, z <= 0), ans);
1496 nz$
1497
1498 csign(sin(-28/3 +%i));
1499 complex$
1500
1501 sign(cos(x^2+1));
1502 pnz$
1503
1504 sign(cos(z));
1505 pnz$
1506
1507 block([ans], assume(-%pi/2 < z, z < %pi/2), ans : sign(cos(z)), forget(-%pi/2 < z, z < %pi/2), ans);
1508 pos$
1509
1510 block([ans], assume(-%pi/2 <= z, z <= %pi/2), ans : sign(cos(z)), forget(-%pi/2 <= z, z <= %pi/2), ans);
1511 pz$
1512
1513 block([ans], assume(%pi/2 < z, z < 3*%pi/2), ans : sign(cos(z)), forget(%pi/2 < z, z < 3*%pi/2), ans);
1514 neg$
1515
1516 block([ans], assume(%pi/2 <= z, z <= 3*%pi/2), ans : sign(cos(z)), forget(%pi/2 <= z, z <= 3*%pi/2), ans);
1517 nz$
1518
1519 csign(cos(11/5 +%i));
1520 complex$
1521
1522 /* Tests for sign of ceiling & floor */
1523
1524 block([ans], assume(x >= 0), ans : sign(floor(x)), forget(x >= 0), ans);
1525 pz$
1526
1527 block([ans], assume(x >= 1), ans : sign(floor(x)), forget(x >= 1), ans);
1528 pos$
1529
1530 block([ans], assume(x > 1), ans : sign(floor(x)), forget(x > 1), ans);
1531 pos$
1532
1533 block([ans], assume(x < 0), ans : sign(floor(x)), forget(x < 0), ans);
1534 neg$
1535
1536 block([ans], assume(x <= 0), ans : sign(floor(x)), forget(x <= 0), ans);
1537 nz$
1538
1539 block([ans], assume(x > 0), ans : sign(ceiling(x)), forget(x > 0), ans);
1540 pos$
1541
1542 block([ans], assume(x > -1), ans : sign(ceiling(x)), forget(x > -1), ans);
1543 pz$
1544
1545 block([ans], assume(x <= -1), ans : sign(ceiling(x)), forget(x <= -1), ans);
1546 neg$
1547
1548 block([ans], assume(x < 0), ans : sign(ceiling(x)), forget(x < 0), ans);
1549 nz$
1550
1551
1552 /* Clean up!*/
1553
1554 (kill(a,b,c),killcontext(learndata),0);
1555 0$
1556
1557 facts();
1558 []$
1559
1560 values;
1561 []$
1562
1563 contexts;
1564 [initial,global]$