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
 260
 261 /* SF bug 798571 */
 262
 263 sign(sqrt(2)/2 - 1/sqrt(2));
 264 zero$
 265
 266 /* SF bug 1045920
 267  * This case is fixed in compar.lisp revision 1.76.
 268  * Adding some more examples.
 269  */
 270
 271 (assume(a > 1, b > 1),0);
 272 0$
 273
 274 sign(a+b-2);
 275 pos;
 276 sign(2*a+b-3);
 277 pos;
 278 sign(2*a+b-4);
 279 pnz;
 280
 281 (forget(a > 1, b > 1),0);
 282 0$
 283
 284 (assume(a < -1, b < -1),0);
 285 0$
 286
 287 sign(a+b+2);
 288 neg;
 289 sign(2*a+b+3);
 290 neg;
 291 sign(2*a+b+4);
 292 pnz;
 293
 294 (forget(x < -1, y < -1),0);
 295 0;
 296
 297 /* SF bug 1724592  */
 298
 299 (aaa : 'bbb, bbb : 'ccc, ccc : 23.5,0);
 300 0$
 301
 302 sign(1.0*aaa);
 303 pnz$
 304
 305 sign(1.0*bbb);
 306 pnz$
 307
 308 (remvalue(aaa, bbb, ccc),0);
 309 0$
 310
 311 assume(x32 > 3/2);
 312 [x32 > 3/2];
 313
 314 kill(all);
 315 done;
 316
 317 assume(x32 < 1);
 318 [x32 < 1];
 319
 320 /* [ 1981623 ] wrong sign of sqrt() */
 321 (assume(xx >= 0, xx <= 1), 0);
 322 0$
 323
 324 sqrt(a/(xx-1)^2);
 325 sqrt(a)/(1-xx);
 326
 327
 328 /*****************************************************************************
 329
 330  Add tests for the function $csign
 331
 332  First: We repeat all tests which give a correct result for $sign.
 333         The tests which are expected to fail are commented out.
 334
 335 ******************************************************************************/
 336
 337 (kill(all),0);
 338 0$
 339
 340 /* numbers and constants */
 341
 342 csign(minf);
 343 neg$
 344
 345 csign(-1);
 346 neg$
 347
 348 csign(-1.0);
 349 neg$
 350
 351 csign(-1.0b0);
 352 neg$
 353
 354 csign(0);
 355 zero$
 356
 357 csign(0.0);
 358 zero$
 359
 360 csign(0.0b0);
 361 zero$
 362
 363 csign(1);
 364 pos$
 365
 366 csign(1.0);
 367 pos$
 368
 369 csign(1.0b0);
 370 pos$
 371
 372 csign(inf);
 373 pos$
 374
 375 csign(%pi);
 376 pos$
 377
 378 csign(%e);
 379 pos$
 380
 381 csign(%phi);
 382 pos$
 383
 384 /* polynomials */
 385
 386 csign(x);
 387 pnz$
 388
 389 csign(x^2);
 390 pz$
 391
 392 csign(x^3);
 393 pnz$
 394
 395 csign(x^4);
 396 pz$
 397
 398 csign(x^2 + x);
 399 pnz$
 400
 401 /* This is expected to be wrong
 402 csign(x^2 + x + 42);
 403 pos$
 404 */
 405
 406 csign(x^2 + sqrt(5) + 101);
 407 pos$
 408
 409 csign(%pi * x^2 + sqrt(5) + 101);
 410 pos$
 411
 412 csign((sqrt(97) - 1) * x^2 + sqrt(5) + 101);
 413 pos$
 414
 415 /* This is expected to be wrong
 416 csign(-x^2 + x - 42);
 417 neg$
 418 */
 419
 420 csign(x^2 - 2 * x + 1);
 421 pz$
 422
 423 csign(-x^2 + 2 * x - 1);
 424 nz$
 425
 426 csign(x+y);
 427 pnz$
 428
 429 csign(x^2 + 2 * x * y + y^2);
 430 pz$
 431
 432 /* This is expected to be wrong.
 433 csign(x^2 + 2 * x * y + y^2 + 1);
 434 pos$
 435 */
 436
 437 csign((x+y)^2 + (z-x)^2);
 438 pz$
 439
 440 csign(sqrt(2) * (x+y)^2 + %e * (z-x)^2);
 441 pz$
 442
 443 csign(-(x+y)^2 - (z-x)^2);
 444 nz$
 445
 446 csign(-(x+y)^2 - (z-x)^2 - %pi);
 447 neg$
 448
 449 csign(-sqrt(2) * (x+y)^2 - %phi * (z-x)^2 - %pi);
 450 neg$
 451
 452
 453 /* rational */
 454
 455 csign(1/x);
 456 pn$
 457
 458 csign(1/(x-1));
 459 pn$
 460
 461 csign(1/x + 1);
 462 pnz$
 463
 464 csign(x/(1+x^2));
 465 pnz$
 466
 467 /* This is expected to be wrong.
 468 csign(1 + x/(1+x^2));
 469 pos$
 470 */
 471
 472 csign((1+x^2)/x);
 473 pn$
 474
 475 /* assumptions */
 476
 477 (assume(a < b, b < c, c < d),0);
 478 0$
 479
 480 csign(b-a);
 481 pos$
 482
 483 csign(a-b);
 484 neg$
 485
 486 csign(c-a);
 487 pos$
 488
 489 csign(a-c);
 490 neg$
 491
 492 csign(d-b);
 493 pos$
 494
 495 csign(b-d);
 496 neg$
 497
 498 csign(7*(c-a) + %pi * (d-b));
 499 pos$
 500
 501 csign(-7*(c-a) - %pi * (d-b));
 502 neg$
 503
 504 csign((b-a) * (d-a));
 505 pos$
 506
 507 csign((b-a)/(c-b));
 508 pos$
 509
 510 (forget(a < b, b < c, c < d),0);
 511 0$
 512
 513 /* algebraic */
 514
 515 csign(sqrt(x));
 516 pz$
 517
 518 csign(sqrt(x^2 + 1));
 519 pos$
 520
 521 csign(sqrt(a) + sqrt(b));
 522 pz$
 523
 524 csign(x^(1/3));
 525 pnz$
 526
 527 csign(x^(1/4));
 528 pz$
 529
 530 csign(x^(1/4) + 1);
 531 pos$
 532
 533 csign(-(x^(1/4) + 1));
 534 neg$
 535
 536 /* exp-like */
 537
 538 csign(cos(x));
 539 pnz$
 540
 541 /* This is expected to be wrong.
 542 csign(cos(x) + 42);
 543 pos$
 544 */
 545
 546 /* This is expected to be wrong.
 547 csign(sin(x) - 42);
 548 neg$
 549 */
 550
 551 csign(cosh(x));
 552 pos$
 553
 554 /* This is exprected to be wrong.
 555 csign(cosh(x)-1);
 556 pz$
 557 */
 558
 559 csign(sinh(x));
 560 pnz$
 561
 562 csign(tanh(x));
 563 pnz$
 564
 565 csign(exp(x));
 566 pos$
 567
 568 csign(exp(-x^2));
 569 pos$
 570
 571 csign(exp(-x) - 1);
 572 pnz$
 573
 574 csign(exp(-x) + 1);
 575 pos$
 576
 577 /* log-like */
 578
 579 /* This is expected to be wrong.
 580 csign(acos(x));
 581 pz$
 582 */
 583
 584 csign(asin(x));
 585 pnz$
 586
 587 csign(atan(x));
 588 pnz$
 589
 590 csign(log(x));
 591 complex$
 592
 593 (assume(x > 0),0);
 594 0$
 595
 596 csign(log(x));
 597 pnz$
 598
 599 (forget(x > 0),0);
 600 0$
 601
 602 (assume(x >= 1),0);
 603 0$
 604
 605 csign(log(x));
 606 pz$
 607
 608 (forget(x >= 1),0);
 609 0$
 610
 611 /* This is expected to be wrong.
 612 csign(acosh(x));
 613 pz$
 614 */
 615
 616 csign(asinh(x));
 617 pnz$
 618
 619 csign(tanh(x));
 620 pnz$
 621
 622 /* SF bug 798571 */
 623
 624 csign(sqrt(2)/2 - 1/sqrt(2));
 625 zero$
 626
 627 /* SF bug 1045920 */
 628
 629 /*
 630
 631 (assume(a > 1, b > 1),0);
 632 0$
 633
 634 csign(a + b -2);
 635 pos$
 636
 637 (forget(a > 1, b > 1),0);
 638 0$
 639
 640 */
 641
 642 /* SF bug 1724592  */
 643
 644 (aaa : 'bbb, bbb : 'ccc, ccc : 23.5,0);
 645 0$
 646
 647 csign(1.0*aaa);
 648 pnz$
 649
 650 csign(1.0*bbb);
 651 pnz$
 652
 653 (remvalue(aaa, bbb, ccc),0);
 654 0$
 655
 656 assume(x32 > 3/2);
 657 [x32 > 3/2];
 658
 659 kill(all);
 660 done;
 661
 662 assume(x32 < 1);
 663 [x32 < 1];
 664
 665 /******************************************************************************
 666   Second: $csign with complex expressions.
 667 ******************************************************************************/
 668
 669 declare(n,integer,x,real,j,imaginary,z,complex);
 670 done;
 671
 672 /* We test the constants. UND and IND do not give a result, but an error. */
 673 map(csign, [%e,%gamma,%phi,%i, minf,inf,infinity]);
 674 [pos,pos,pos,imaginary,neg,pos,complex];
 675
 676 /* Symbols declcared as integeger, real, imaginary or complex */
 677 map(csign, [n,x,j,z]);
 678 [pnz,pnz,imaginary,complex];
 679
 680 /* Some arithmetic with pure imaginary numbers and symbols */
 681
 682 map(csign,[%i,sqrt(-1),10*%i,x*%i,%i^2,%i^3,%i^4,%i^5]);
 683 [imaginary,imaginary,imaginary,imaginary,neg,imaginary,pos,imaginary];
 684
 685 map(csign,[j,sqrt(-1),10*j,x*j,j^2,j^3,j^4,j^5]);
 686 [imaginary,imaginary,imaginary,imaginary,nz,imaginary,pz,imaginary];
 687
 688 /* negative base and half integral exponent */
 689 map(csign,[(-1)^(1/2),(-1)^(3/2),(-1)^(5/2), (-1)^(7/2), (-1)^(9/2)]);
 690 [imaginary,imaginary,imaginary,imaginary,imaginary];
 691
 692 /* the same with an negative expression */
 693 (assume(xneg < 0, xpos>0),done);
 694 done;
 695 map(csign,[(xneg)^(1/2),(xneg)^(3/2),(xneg)^(5/2),(xneg)^(7/2)]);
 696 [imaginary,imaginary,imaginary,imaginary];
 697
 698 map(csign,[(-xpos)^(1/2),(-xpos)^(3/2),(-xpos)^(5/2),(-xpos)^(7/2)]);
 699 [imaginary,imaginary,imaginary,imaginary];
 700
 701 map(csign,[(-1)^xpos, (-1)^xneg]);
 702 [complex,complex];
 703
 704 map(sign,[(-1)^xpos, (-1)^xneg]);
 705 [pn,pn];
 706
 707 /* Expressions with an addition */
 708
 709 csign(x+%i*y);
 710 complex;
 711 csign((x+%i*y)^2);
 712 complex;
 713 csign((x+%i*y)^(1/2));
 714 complex;
 715
 716 csign((a+x+%i*y)/(b-y*%i));
 717 complex;
 718
 719 /* More expressions */
 720
 721 csign(1/z);
 722 complex;
 723 csign(1/j);
 724 imaginary;
 725 csign(10*a+c/z);
 726 complex;
 727 csign(10*a+c/j);
 728 complex;
 729 csign((10*a+(c/j)^2)^n);
 730 pnz;
 731 csign((10*a+(c/j)^3)^n);
 732 complex;
 733
 734 /* This does not work correctly.
 735    The answer complex is not really wrong, but could be better.
 736    To achieve this we have first to improve the function rectform. */
 737
 738 csign((1+%i)*(1-%i));
 739 complex; /* should be pos */
 740
 741 csign(expand((1+%i)*(1-%i)));
 742 pos; /* after expansion correct */
 743
 744 /* Functions which are declared to be complex give the sign $complex */
 745
 746 csign(conjugate(z));
 747 complex;
 748 csign(conjugate(x)); /* x is real */
 749 pnz;
 750
 751 declare(f,complex);
 752 done;
 753 csign(f(x));
 754 complex;
 755
 756 /* realpart and imagpart are real valued */
 757
 758 csign(realpart(z));
 759 pnz;
 760 csign(imagpart(z));
 761 pnz;
 762
 763 /*
 764  * Examples for assumptions with abs(x)<a, a is positive
 765  *
 766  */
 767
 768 kill(all);
 769 done;
 770
 771 assume(abs(x)<1);
 772 [abs(x)<1];
 773
 774 sign(1-x);
 775 pos;
 776 sign(2-x);
 777 pos;
 778 sign(x-1);
 779 neg;
 780 sign(x-2);
 781 neg;
 782
 783 forget(abs(x)<1);
 784 [abs(x)<1];
 785
 786 facts();
 787 [];
 788
 789 assume(a>0,abs(x)<a);
 790 [a>0,a>abs(x)];
 791
 792 sign(a-x);
 793 pos;
 794 sign(x-a);
 795 neg;
 796
 797 forget(abs(x)<a);
 798 [a>abs(x)];
 799
 800 facts();
 801 [a>0];
 802
 803 assume(a*abs(x)<1);
 804 [a*abs(x)<1];
 805
 806 sign(1/a-x);
 807 pos;
 808 sign(x-1/a);
 809 neg;
 810
 811 forget(a*abs(x)<1);
 812 [a*abs(x)<1];
 813
 814 assume(abs(x)<2*a+1);
 815 [2*a-abs(x)+1>0];
 816
 817 sign(2*a+1-x);
 818 pos;
 819 sign(2*a+1+x);
 820 pos;
 821 sign(a*(2*a+1-x));
 822 pos;
 823
 824 forget(abs(x)<2*a+1);
 825 [2*a-abs(x)+1>0];
 826
 827 facts();
 828 [a>0];
 829
 830 assume(b>0,b<1);
 831 [b>0,b<1];
 832
 833 assume(abs(x)<b);
 834 [b>abs(x)];
 835
 836 is(x<1);
 837 true;
 838 sign(1-x);
 839 pos;
 840 sign(x-1);
 841 neg;
 842
 843 forget(abs(x)<b);
 844 [b>abs(x)];
 845
 846 facts();
 847 [a>0,b>0,1>b];
 848
 849 assume(sin(abs(x)) < 1);
 850 [sin(abs(x))<1];
 851
 852 sign(1-sin(x));
 853 pos;
 854 sign(2-sin(x));
 855 pos;
 856 sign(sin(x)-1);
 857 neg;
 858 sign(sin(x)-2);
 859 neg;
 860
 861 forget(sin(abs(x)) < 1);
 862 [sin(abs(x))<1];
 863
 864 assume(cos(abs(x)) < 1);
 865 [cos(abs(x))<1];
 866
 867 sign(1-cos(x));
 868 pos;
 869 sign(2-cos(x));
 870 pos;
 871 sign(cos(x)-1);
 872 neg;
 873 sign(cos(x)-2);
 874 neg;
 875
 876 forget(cos(abs(x)) < 1);
 877 [cos(abs(x))<1];
 878
 879 assume(abs(sin(x)) < 1);
 880 [abs(sin(x))<1];
 881
 882 sign(1-sin(x));
 883 pos;
 884 sign(2-sin(x));
 885 pos;
 886 sign(sin(x)-1);
 887 neg;
 888 sign(sin(x)-2);
 889 neg;
 890
 891 forget(abs(sin(x)) < 1);
 892 [abs(sin(x))<1];
 893
 894 assume(abs(cos(x)) < 1);
 895 [abs(cos(x))<1];
 896
 897 sign(1-cos(x));
 898 pos;
 899 sign(2-cos(x));
 900 pos;
 901 sign(cos(x)-1);
 902 neg;
 903 sign(cos(x)-2);
 904 neg;
 905
 906 forget(abs(cos(x)) <1);
 907 [abs(cos(x))<1];
 908
 909 csign(log((1 + %i)/sqrt(2)));
 910 imaginary$
 911
 912 /* Examples to show that learn-numer works
 913  * Related bug report:
 914  * Bug ID: 2477795 - "assume":problems with fractions or multiples of %pi and %e
 915  */
 916 kill(all);
 917 done;
 918 assume(a>0,a<%pi/2);
 919 [a>0,%pi/2>a];
 920
 921 is(a>%pi/2);
 922 false;
 923 is(a>%pi);
 924 false;
 925
 926 assume(b>0,b<2*%pi);
 927 [b>0, 2*%pi>b];
 928 is(b>3*%pi);
 929 false;
 930
 931 /* An example involving a numerical constant, the value of a function
 932  * and the abs function.
 933  * This example no longer works because of revision 1.62 of compar.lisp
 934  */
 935 assume(abs(x) < sin(1)+%e/2);
 936 [sin(1)+%e/2>abs(x)];
 937 is(x<2*%e);
 938 true;
 939 is(x>-2*%e);
 940 true;
 941 (forget(abs(x)<sin(1)+%e/2),done);
 942 done;
 943
 944 /* Bug ID: 2876382 - sign(a+b+sin(1)) unknown */
 945 (assume(a>0,b>0),done);
 946 done;
 947 sign(a+b+sin(1));
 948 pos;
 949 (forget(a>0,b>0),done);
 950 done;
 951
 952 /* Bug ID: 2184396 - Wrong factorization of sqrt()
 953  * This is the example from the bug report which has triggered the bug in sign
 954  *      sqrt(1-(2-sqrt(2))/x * ((2+sqrt(2))/x-1));
 955  * The expression has factored wrongly. This example is now correct.
 956  */
 957 sign(1-(1+sqrt(2))*x);
 958 'pnz;
 959 sign(1-(1+sqrt(2))/x);
 960 'pnz;
 961
 962 /* Bug ID: 1038624 - askinteger ignores asksign database
 963  * With revision 1.64 of compar.lisp code has been added, which looks for
 964  * integer and noninteger facts into the database.
 965  */
 966 (assume(equal(a,0), equal(b,2), equal(c,1/3), equal(d,1.5), equal(e,3.0b0)),
 967  done);
 968 done;
 969
 970 map(askinteger, [a, b, 2*b, 2+b, c, d, e]);
 971 [yes, yes, yes, yes, no, no, no];
 972
 973
 974 (forget(equal(a,0), equal(b,2), equal(c,1/3), equal(d,1.5), equal(e,3.0b0)),
 975  done);
 976 done;
 977
 978 /* Bug ID: 3376603 - sign of declared imaginary */
 979 declare(f,imaginary, g,complex);
 980 done$
 981 csign(f(x));
 982 imaginary$
 983 csign(g(x));
 984 complex$
 985 kill(f,g);
 986 done$
 987
 988 /* Check adding new equaltiy does not make old inequality disappear */
 989 kill(all);
 990 done;
 991
 992 assume(notequal(a,b));
 993 [notequal(a, b)];
 994
 995 is(equal(a,b));
 996 false;
 997
 998 (assume(equal(a, x+y)), 0);
 999 0;
1000
1001 is(equal(a,b));
1002 false;
1003
1004 /* Check fix for bug 2547 (declare constant messes up sign calculations) */
1005 (declare (x, constant), declare (y, constant), assume (x > y), is (x>y));
1006 true$
1007
1008 /* facts in assume database not cleaned up by 'sign' */
1009
1010 (kill (foo), foo : %e^(abs(uu)+uu)*(uu/abs(uu)+1)+%e^(abs(uu)-uu)*(uu/abs(uu)-1), 0);
1011 0;
1012
1013 block ([bar, baz], bar : copy (facts (initial)), is (equal (foo, 0)), baz : facts (initial), is (bar = baz));
1014 true;
1015
1016 /* tnx to Barton Willis for the next couple of tests */
1017
1018 map('sign,[sqrt(x),x]);
1019 [pz, pnz];
1020
1021 (kill(buddy),
1022  buddy(p,q) := expand(if p >= 0 then q else q,0,0),
1023  buddy(sqrt(x),abs(x)));
1024 abs(x);
1025
1026 /* Ensure that asksign1 deals correctly with squared expressions */
1027 (assume (notequal(n, 1)), 0);
1028 0$
1029
1030 is ((n-1)^2 > 0);
1031 true$
1032
1033 /* Here are some calls to asksign & askinteger -- these don't cause
1034  * an interactive prompt. Interactive examples are in rtest_ask.mac.
1035  */
1036
1037 map(askinteger,[0,1/2,sqrt(17)]);
1038 [yes,no,no]$
1039
1040 /* Known constants */
1041 map(askinteger,[%pi,%e,%phi,%gamma,%i]);
1042 [no,no,no,no,no]$
1043
1044 map(asksign,[%pi,%e,%phi,%gamma,inf,minf]);
1045 [pos,pos,pos,pos,pos,neg]$
1046
1047 errcatch(asksign(%i));
1048 []$ /* argument cannot be imaginary. */
1049
1050 errcatch(asksign(infinity));
1051 []$ /* sign of infinity is undefined. */
1052
1053 /* Odd functions */
1054
1055 (declare(o, oddfun),0);
1056 0$
1057
1058 (assume(equal(q, 0)),0);
1059 0$
1060
1061 sign(o(q));
1062 zero$
1063
1064 (remove(o, oddfun),0);
1065 0$
1066
1067 (forget(equal(q, 0)),0);
1068 0$
1069
1070 /* Increasing and decreasing functions */
1071
1072 (declare(i, increasing, d, decreasing),0);
1073 0$
1074
1075 (assume(r > q),0);
1076 0$
1077
1078 is(i(r) > i(q));
1079 true$
1080
1081 is(d(r) < d(q));
1082 true$
1083
1084 (remove(i, increasing, d, decreasing),0);
1085 0$
1086
1087 (forget(r > q), 0);
1088 0$
1089
1090 /* Increasing and decreasing odd functions */
1091
1092 (declare(i, [oddfun, increasing], d, [oddfun, decreasing]),0);
1093 0$
1094
1095 (assume(q < 0, r > 0),0);
1096 0$
1097
1098 sign(i(q));
1099 neg$
1100
1101 sign(i(r));
1102 pos$
1103
1104 sign(d(q));
1105 pos$
1106
1107 sign(d(r));
1108 neg$
1109
1110 (remove(i, [oddfun, increasing], d, [oddfun, decreasing]),0);
1111 0$
1112
1113 (forget(q < 0, r > 0),0);
1114 0$
1115
1116 /* Bug #3109: is(sin(x) <= 1) returns "unknown", is(sin(x) <= 1.00001) returns "true" */
1117 (kill(all),0);
1118 0$
1119 is(sin(x) <= 1);
1120 true$
1121 is(cos(x) <= 1);
1122 true$
1123 is(sin(x) >= -1);
1124 true$
1125 is(cos(x) >= -1);
1126 true$
1127 sign(sin(x)+1);
1128 pz$
1129 sign(cos(x)+1);
1130 pz$
1131 sign(sin(x)-1);
1132 nz$
1133 sign(cos(x)-1);
1134 nz$
1135
1136 /* Assumptions and queries involving multiple unknowns */
1137 assume(-2*x*y>10);
1138 [x*y<-5]$
1139 is(10*x*y<-50);
1140 true$
1141 assume(3*x*y>0);
1142 [inconsistent]$
1143 assume(notequal(2*a*b,10));
1144 [notequal(a*b,5)]$
1145 is(equal(10*a*b,50));
1146 false$
1147 (kill(all),0);
1148 0$
1149
1150 /* Exponents in inequality assumptions and queries  */
1151 assume(x^3/y>=0);
1152 [x*y>=0]$
1153 sign(y^3/x);
1154 pz$
1155 (declare(e, even, o, odd), 0);
1156 0$
1157 assume(a^o>0);
1158 [a>0]$
1159 sign(-2*a^o);
1160 neg$
1161 assume(b^(e+1)<0);
1162 [b<0]$
1163 sign(-b^(e+1));
1164 pos$
1165 assume(c^m/d^n<=0);
1166 [c^m*d^n<=0]$
1167 assume(f^(1/3)*g^h<0);
1168 [f*g^h<0]$
1169 (kill(all),0);
1170 0$
1171
1172 /* The csign of a product with a complex factor and a zero factor used
1173  * to depend on the order of the factors: if the zero came first then
1174  * the sign was zero, but if the complex came first then the sign was
1175  * complex.
1176  */
1177
1178 (declare (a, complex), assume (equal (b, 0)), 0)$
1179 0;
1180 csign (a * b);
1181 zero;
1182 (remove (a, complex), forget (equal (b, 0)), 0)$
1183 0;
1184
1185 (declare (b, complex), assume (equal (a, 0)), 0)$
1186 0;
1187 csign (a * b);
1188 zero;
1189 (remove (b, complex), forget (equal (a, 0)), 0)$
1190 0;
1191
1192 /* SF bug report #3583: "Stack overflow for equality testing with assumptions" */
1193
1194 (domain: real,
1195  myctxt: newcontext (),
1196  assume (x > 0, y > 0),
1197  is(equal(y*(x-y),0)));
1198 unknown;
1199
1200 (domain: complex,
1201  is(equal(y*(x-y),0)));
1202 unknown;
1203
1204 (killcontext (myctxt),
1205  reset (domain));
1206 [domain];
1207
1208 /* Bug #3417: sign(1/zero) => 0 (where equal(zero,0)) */
1209
1210 (assume (equal (zero, 0), equal (q, r)), 0)$
1211 0;
1212
1213 errcatch (sign (1 / (q - r)))$
1214 [];
1215
1216 /* This used to return zero */
1217 errcatch (sign (1 / zero))$
1218 [];
1219
1220 (forget (equal (zero, 0), equal (q, r)), 0)$
1221 0;
1222
1223 /* bug reported to mailing list 2021-06-27: "ev(xxx,pred) vs is(xxx)" */
1224
1225 xxx:  '((0 < 1) or (0 < 2));
1226 (0 < 1) or (0 < 2);
1227
1228 ev(xxx, pred);
1229 true;
1230
1231 ev(xxx, nouns);
1232 true;
1233
1234 is(xxx);
1235 true;
1236
1237 yyy: '((0 < 1) and (0 < 2));
1238 (0 < 1) and (0 < 2);
1239
1240 is(yyy);
1241 true;
1242
1243 zzz: '((0 > 1) or (0 < 2));
1244 (0 > 1) or (0 < 2);
1245
1246 is(zzz);
1247 true;
1248
1249 aaa: '((0 > 1) and (0 < 2));
1250 (0 > 1) and (0 < 2);
1251
1252 is(aaa);
1253 false;
1254
1255 bbb: '((0 > 1) or (0 > 2));
1256 (0 > 1) or (0 > 2);
1257
1258 is(bbb);
1259 false;
1260
1261 (kill(xyz), ccc: '((xyz > 4) or (3 > 2)));
1262 (xyz > 4) or (3 > 2);
1263
1264 is(ccc);
1265 true;
1266
1267 ddd: '((2 < 1) or (2 < 2) or (1 < 3) and (2 < 4));
1268 (2 < 1) or (2 < 2) or ((1 < 3) and (2 < 4));
1269
1270 is(ddd);
1271 true;
1272
1273 /* SF bug #3324: "Stack overflow in sign() when domain complex" */
1274
1275 (kill(a, b, c),
1276  domain: complex,
1277  declare([a,b,c], real),
1278  mycontext: newcontext (),
1279  assume(a>0, b>0, c>0),
1280  sign(c - b^(1/3)*c^(1/3)));
1281 pnz;
1282
1283 sign(c - (b*c)^(1/3));
1284 pnz;
1285
1286 killcontext (mycontext);
1287 done;
1288
1289 /* SF bug #3440: "complex domain + real variable = seg-fault"
1290  * possibly related to #3324
1291  */
1292
1293 (kill (m1, m2, m3, r12, r13, r23, A),
1294  mycontext: newcontext (),
1295  domain:complex,
1296  declare([m1,m2,m3],real),
1297  declare([r12,r13,r23],real),
1298  assume(r12>0,r13>0,r23>0),
1299  assume(r12<r13+r23,r13<r12+r23,r23<r12+r13),
1300  assume(m1>0,m2>0,m3>0),
1301  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),
1302  is(equal(A,0)));
1303 unknown;
1304
1305 (reset (),
1306  killcontext (mycontext));
1307 done;