|
From: tomasriker <tom...@us...> - 2026-05-28 22:14:17
|
This is an automated email from the git hooks/post-receive script. It was
generated because a ref change was pushed to the repository containing
the project "Maxima CAS".
The branch, master has been updated
via 96ea422c6c5dbf5440ea544500fe8fc885247b64 (commit)
from 72870542c3f841c1aad2537bf86215afc9df3bbb (commit)
Those revisions listed above that are new to this repository have
not appeared on any other notification email; so we list those
revisions in full, below.
- Log -----------------------------------------------------------------
commit 96ea422c6c5dbf5440ea544500fe8fc885247b64
Author: David Scherfgen <d.s...@go...>
Date: Fri May 29 00:11:25 2026 +0200
SIGNDIFF-SPECIAL: handle sign(abs(a)-b) and sign(a^pos_int-b)
Maxima can now determine more signs without using factoring or when factoring
wouldn't work, for example sign(x^2-2) with -1 < x < 1.
Absolute value handling allows Maxima to, e.g., determine that abs(cos(x)) <= 1.
Also, to make sure that the cases handled by SIGNDIFF-SPECIAL work correctly
regardless of whether XLHS and XRHS are swapped, a simple "swap and flip sign"
logic is introduced.
This fixes bugs #2288 and #3155.
diff --git a/src/compar.lisp b/src/compar.lisp
index 8a5bf0bc6..3e33b3800 100644
--- a/src/compar.lisp
+++ b/src/compar.lisp
@@ -1481,7 +1481,7 @@ TDNEG TDZERO TDPN) to store it, and also sets SIGN."
(defun signdiff-special (xlhs xrhs)
;; xlhs may be a constant
- (let ((sgn nil))
+ (let ((sgn nil) flip-sign)
(when (or (and (realp xrhs) (minusp xrhs)
(not (atom xlhs)) (eq (sign* xlhs) '$pos))
; e.g. sign(a^3+%pi-1) where a>0
@@ -1506,7 +1506,16 @@ TDNEG TDZERO TDPN) to store it, and also sets SIGN."
(eq (sign* (sub (cadr xlhs) 1)) '$pos)
(eq (sign* (sub (caddr xlhs) (caddr xrhs))) '$pos)))
(setq sgn '$pos))
-
+
+ ;; For the following test, swap XLHS and XRHS, if necessary, so that XLHS
+ ;; is one of the operators that we can handle, and remember to flip the result.
+ (let ((operators '(%sin %cos %cosh %sech %signum mabs)))
+ (when (and (not (atom xrhs))
+ (member (caar xrhs) operators :test #'eq)
+ (or (atom xlhs)
+ (not (member (caar xlhs) operators :test #'eq))))
+ (psetq xlhs xrhs xrhs xlhs flip-sign (not flip-sign))))
+
;; sign(sin(x)+c)
(when (and (not (atom xlhs))
(member (caar xlhs) '(%sin %cos))
@@ -1556,10 +1565,46 @@ TDNEG TDZERO TDPN) to store it, and also sets SIGN."
(setq sgn '$pnz))
(t ;; -1 < c < 1, but c # 0
(setq sgn '$pn))))
-
+
+ ;; sign(abs(a) - b) = sign_max(sign(a - b), sign(-a - b)) with real a, b
+ (when (and (null sgn)
+ (not (atom xlhs))
+ (eq (caar xlhs) 'mabs)
+ (zerop1 ($imagpart (cadr xlhs)))
+ (zerop1 ($imagpart xrhs)))
+ (let* ((a (cadr xlhs))
+ (b xrhs)
+ (s1 (sign* (sub a b)))
+ (s2 (sign* (sub (neg a) b)))
+ (max-sign (sminmax '$max s1 s2)))
+ (when (not (eq max-sign '$pnz))
+ (setq sgn max-sign))))
+
+ ;; For the following test, swap XLHS and XRHS, if necessary, so that XRHS is
+ ;; the number, e.g. x^2 - 3 -> 3 - x^2, and remember to flip the result.
+ (when (and (mnump xlhs) (not (mnump xrhs)))
+ (psetq xlhs xrhs xrhs xlhs flip-sign (not flip-sign)))
+
+ ;; sign(a^pos_int - b) = sign(abs_if_even(a) - b^(1/pos_int))
+ ;; with real a, b >= 0 (for even pos_int), and b^(1/pos_int) being the real root
+ (when (and (null sgn)
+ (mnump xrhs)
+ (mexptp xlhs)
+ (integerp (caddr xlhs))
+ (> (caddr xlhs) 0)
+ (or (oddp (caddr xlhs)) (not (mnegp xrhs)))
+ (zerop1 ($imagpart (cadr xlhs))))
+ (let* ((exponent (caddr xlhs))
+ (root (mul (if (mnegp xrhs) -1 1) (power (ftake 'mabs xrhs) (div 1 exponent))))
+ (base (cadr xlhs))
+ (maybe-abs-base (if (evenp exponent) (ftake 'mabs base) base))
+ (diff-sign (sign* (sub maybe-abs-base root))))
+ (when (not (eq diff-sign '$pnz))
+ (setq sgn diff-sign))))
+
(when (and $useminmax (or (minmaxp xlhs) (minmaxp xrhs)))
(setq sgn (signdiff-minmax xlhs xrhs)))
- (when sgn (setq sign sgn minus nil odds nil evens nil)
+ (when sgn (setq sign (if flip-sign (flip sgn) sgn) minus nil odds nil evens nil)
t)))
;;; Look for symbols with an assumption a > n or a < -n, where n is a number.
diff --git a/tests/rtest_sign.mac b/tests/rtest_sign.mac
index 62f02312f..e83d91993 100644
--- a/tests/rtest_sign.mac
+++ b/tests/rtest_sign.mac
@@ -1606,3 +1606,62 @@ block ([S: make_string_output_stream (), S1],
S1);
"sign: sign undefined for foo
";
+
+/* Bug #2288: "x^2<1 can't get x^2<2, but can get x^2<100" */
+/* and related tests */
+
+assume(x > -1, x < 1);
+[x > -1, x < 1];
+
+[sign(abs(x) - 1), sign(1 - abs(x))];
+[neg, pos];
+
+[sign(abs(x) - 2), sign(2 - abs(x))];
+[neg, pos];
+
+[sign(abs(x) - 1/2), sign(1/2 - abs(x))];
+[pnz, pnz];
+
+[sign(x^2 - 1), sign(1 - x^2)];
+[neg, pos];
+
+[sign(x^2 - 2), sign(2 - x^2)];
+[neg, pos];
+
+[sign(x^2 - 1/2), sign(1/2 - x^2)];
+[pnz, pnz];
+
+[sign(x^2 - 100), sign(100 - x^2)];
+[neg, pos];
+
+[sign(x^2 - 10000), sign(10000 - x^2)];
+[neg, pos];
+
+[sign(x^4 - 2), sign(2 - x^4)];
+[neg, pos];
+
+[sign(x^3 - 1), sign(1 - x^3)];
+[neg, pos];
+
+[sign(x^3 - 2), sign(2 - x^3)];
+[neg, pos];
+
+[sign(x^3 - 1/2), sign(1/2 - x^3)];
+[pnz, pnz];
+
+[sign(x^3 + 1), sign(-1 - x^3)];
+[pos, neg];
+
+[sign(x^3 + 2), sign(-2 - x^3)];
+[pos, neg];
+
+[sign(x^3 + 1/2), sign(-1/2 - x^3)];
+[pnz, pnz];
+
+forget(x > -1, x < 1);
+[x > -1, x < 1];
+
+/* Bug #3155: "is(abs(cos(x))<=1) is unknown, but is(cos(x)<=1) and is(cos(x)>=-1) are true" */
+
+is(abs(cos(x)) <= 1);
+true;
-----------------------------------------------------------------------
Summary of changes:
src/compar.lisp | 53 ++++++++++++++++++++++++++++++++++++++++++----
tests/rtest_sign.mac | 59 ++++++++++++++++++++++++++++++++++++++++++++++++++++
2 files changed, 108 insertions(+), 4 deletions(-)
hooks/post-receive
--
Maxima CAS
|