4 /* numbers and constants */
68 sign(x^2 + sqrt(5) + 101);
71 sign(%pi * x^2 + sqrt(5) + 101);
74 sign((sqrt(97) - 1) * x^2 + sqrt(5) + 101);
80 sign(x^2 - 2 * x + 1);
83 sign(-x^2 + 2 * x - 1);
89 sign(x^2 + 2 * x * y + y^2);
92 sign(x^2 + 2 * x * y + y^2 + 1);
95 sign((x+y)^2 + (z-x)^2);
98 sign(sqrt(2) * (x+y)^2 + %e * (z-x)^2);
101 sign(-(x+y)^2 - (z-x)^2);
104 sign(-(x+y)^2 - (z-x)^2 - %pi);
107 sign(-sqrt(2) * (x+y)^2 - %phi * (z-x)^2 - %pi);
133 (assume(a < b, b < c, c < d),0);
154 sign(7*(c-a) + %pi * (d-b));
157 sign(-7*(c-a) - %pi * (d-b));
166 (forget(a < b, b < c, c < d),0);
177 sign(sqrt(a) + sqrt(b));
189 sign(-(x^(1/4) + 1));
263 sign(sqrt(2)/2 - 1/sqrt(2));
267 * This case is fixed in compar.lisp revision 1.76.
268 * Adding some more examples.
271 (assume(a > 1, b > 1),0);
281 (forget(a > 1, b > 1),0);
284 (assume(a < -1, b < -1),0);
294 (forget(x < -1, y < -1),0);
299 (aaa : 'bbb, bbb : 'ccc, ccc : 23.5,0);
308 (remvalue(aaa, bbb, ccc),0);
320 /* [ 1981623 ] wrong sign of sqrt() */
321 (assume(xx >= 0, xx <= 1), 0);
328 /*****************************************************************************
330 Add tests for the function $csign
332 First: We repeat all tests which give a correct result for $sign.
333 The tests which are expected to fail are commented out.
335 ******************************************************************************/
340 /* numbers and constants */
401 /* This is expected to be wrong
406 csign(x^2 + sqrt(5) + 101);
409 csign(%pi * x^2 + sqrt(5) + 101);
412 csign((sqrt(97) - 1) * x^2 + sqrt(5) + 101);
415 /* This is expected to be wrong
416 csign(-x^2 + x - 42);
420 csign(x^2 - 2 * x + 1);
423 csign(-x^2 + 2 * x - 1);
429 csign(x^2 + 2 * x * y + y^2);
432 /* This is expected to be wrong.
433 csign(x^2 + 2 * x * y + y^2 + 1);
437 csign((x+y)^2 + (z-x)^2);
440 csign(sqrt(2) * (x+y)^2 + %e * (z-x)^2);
443 csign(-(x+y)^2 - (z-x)^2);
446 csign(-(x+y)^2 - (z-x)^2 - %pi);
449 csign(-sqrt(2) * (x+y)^2 - %phi * (z-x)^2 - %pi);
467 /* This is expected to be wrong.
468 csign(1 + x/(1+x^2));
477 (assume(a < b, b < c, c < d),0);
498 csign(7*(c-a) + %pi * (d-b));
501 csign(-7*(c-a) - %pi * (d-b));
504 csign((b-a) * (d-a));
510 (forget(a < b, b < c, c < d),0);
518 csign(sqrt(x^2 + 1));
521 csign(sqrt(a) + sqrt(b));
533 csign(-(x^(1/4) + 1));
541 /* This is expected to be wrong.
546 /* This is expected to be wrong.
554 /* This is exprected to be wrong.
579 /* This is expected to be wrong.
611 /* This is expected to be wrong.
624 csign(sqrt(2)/2 - 1/sqrt(2));
631 (assume(a > 1, b > 1),0);
637 (forget(a > 1, b > 1),0);
644 (aaa : 'bbb, bbb : 'ccc, ccc : 23.5,0);
653 (remvalue(aaa, bbb, ccc),0);
665 /******************************************************************************
666 Second: $csign with complex expressions.
667 ******************************************************************************/
669 declare(n,integer,x,real,j,imaginary,z,complex);
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];
676 /* Symbols declcared as integeger, real, imaginary or complex */
677 map(csign, [n,x,j,z]);
678 [pnz,pnz,imaginary,complex];
680 /* Some arithmetic with pure imaginary numbers and symbols */
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];
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];
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];
692 /* the same with an negative expression */
693 (assume(xneg < 0, xpos>0),done);
695 map(csign,[(xneg)^(1/2),(xneg)^(3/2),(xneg)^(5/2),(xneg)^(7/2)]);
696 [imaginary,imaginary,imaginary,imaginary];
698 map(csign,[(-xpos)^(1/2),(-xpos)^(3/2),(-xpos)^(5/2),(-xpos)^(7/2)]);
699 [imaginary,imaginary,imaginary,imaginary];
701 map(csign,[(-1)^xpos, (-1)^xneg]);
704 map(sign,[(-1)^xpos, (-1)^xneg]);
707 /* Expressions with an addition */
713 csign((x+%i*y)^(1/2));
716 csign((a+x+%i*y)/(b-y*%i));
719 /* More expressions */
729 csign((10*a+(c/j)^2)^n);
731 csign((10*a+(c/j)^3)^n);
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. */
738 csign((1+%i)*(1-%i));
739 complex; /* shoule be pos */
741 csign(expand((1+%i)*(1-%i)));
742 pos; /* after expansion correct */
744 /* Functions which are declared to be complex give the sign $complex */
748 csign(conjugate(x)); /* x is real */
756 /* realpart and imagpart are real valued */
764 * Examples for assumptions with abs(x)<a, a is positive
789 assume(a>0,abs(x)<a);
814 assume(abs(x)<2*a+1);
824 forget(abs(x)<2*a+1);
849 assume(sin(abs(x)) < 1);
861 forget(sin(abs(x)) < 1);
864 assume(cos(abs(x)) < 1);
876 forget(cos(abs(x)) < 1);
879 assume(abs(sin(x)) < 1);
891 forget(abs(sin(x)) < 1);
894 assume(abs(cos(x)) < 1);
906 forget(abs(cos(x)) <1);
909 csign(log((1 + %i)/sqrt(2)));
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
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
935 assume(abs(x) < sin(1)+%e/2);
936 [sin(1)+%e/2>abs(x)];
941 (forget(abs(x)<sin(1)+%e/2),done);
944 /* Bug ID: 2876382 - sign(a+b+sin(1)) unknown */
945 (assume(a>0,b>0),done);
949 (forget(a>0,b>0),done);
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.
957 sign(1-(1+sqrt(2))*x);
959 sign(1-(1+sqrt(2))/x);
962 /* Bug ID: 1038624 - askinteger ignores asksign database
963 * With revison 1.64 of compar.lisp code has been added, which looks for
964 * integer and noninteger facts into the database.
966 (assume(equal(a,0), equal(b,2), equal(c,1/3), equal(d,1.5), equal(e,3.0b0)),
970 map(askinteger, [a, b, 2*b, 2+b, c, d, e]);
971 [yes, yes, yes, yes, no, no, no];
974 (forget(equal(a,0), equal(b,2), equal(c,1/3), equal(d,1.5), equal(e,3.0b0)),
978 /* Bug ID: 3376603 - sign of declared imaginary */
979 declare(f,imaginary, g,complex);
988 /* Check adding new equaltiy does not make old inequality disappear */
992 assume(notequal(a,b));
998 (assume(equal(a, x+y)), 0);
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));
1008 /* facts in assume database not cleaned up by 'sign' */
1010 (kill (foo), foo : %e^(abs(uu)+uu)*(uu/abs(uu)+1)+%e^(abs(uu)-uu)*(uu/abs(uu)-1), 0);
1013 block ([bar, baz], bar : copy (facts (initial)), is (equal (foo, 0)), baz : facts (initial), is (bar = baz));
1016 /* tnx to Barton Willis for the next couple of tests */
1018 map('sign,[sqrt(x),x]);
1022 buddy(p,q) := expand(if p >= 0 then q else q,0,0),
1023 buddy(sqrt(x),abs(x)));
1026 /* Ensure that asksign1 deals correctly with squared expressions */
1027 (assume (notequal(n, 1)), 0);
1033 /* Here are some calls to asksign & askinteger -- these don't cause
1034 * an interactive prompt. Interactive examples are in rtest_ask.mac.
1037 map(askinteger,[0,1/2,sqrt(17)]);
1040 /* Known constants */
1041 map(askinteger,[%pi,%e,%phi,%gamma,%i]);
1044 map(asksign,[%pi,%e,%phi,%gamma,inf,minf]);
1045 [pos,pos,pos,pos,pos,neg]$
1047 errcatch(asksign(%i));
1048 []$ /* argument cannot be imaginary. */
1050 errcatch(asksign(infinity));
1051 []$ /* sign of infinity is undefined. */
1055 (declare(o, oddfun),0);
1058 (assume(equal(q, 0)),0);
1064 (remove(o, oddfun),0);
1067 (forget(equal(q, 0)),0);
1070 /* Increasing and decreasing functions */
1072 (declare(i, increasing, d, decreasing),0);
1084 (remove(i, increasing, d, decreasing),0);
1090 /* Increasing and decreasing odd functions */
1092 (declare(i, [oddfun, increasing], d, [oddfun, decreasing]),0);
1095 (assume(q < 0, r > 0),0);
1110 (remove(i, [oddfun, increasing], d, [oddfun, decreasing]),0);
1113 (forget(q < 0, r > 0),0);
1116 /* Bug #3109: is(sin(x) <= 1) returns "unknown", is(sin(x) <= 1.00001) returns "true" */
1136 /* Assumptions and queries involving multiple unknowns */
1143 assume(notequal(2*a*b,10));
1145 is(equal(10*a*b,50));
1150 /* Exponents in inequality assumptions and queries */
1155 (declare(e, even, o, odd), 0);
1167 assume(f^(1/3)*g^h<0);
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
1178 (declare (a, complex), assume (equal (b, 0)), 0)$
1182 (remove (a, complex), forget (equal (b, 0)), 0)$
1185 (declare (b, complex), assume (equal (a, 0)), 0)$
1189 (remove (b, complex), forget (equal (a, 0)), 0)$