rtoy / maxima

A Clone of Maxima's repo
Other
0 stars 0 forks source link

assume fails on sums #1875

Open rtoy opened 2 months ago

rtoy commented 2 months ago

Imported from SourceForge on 2024-07-05 10:19:56 Created by macrakis on 2020-02-22 22:00:51 Original: https://sourceforge.net/p/maxima/bugs/3611


Maxima 5.43.0 http://maxima.sourceforge.net using Lisp SBCL 1.4.14 Distributed under the GNU Public License. See the file COPYING. Dedicated to the memory of William Schelter. The function bug_report() provides bug reporting information. (%i1) rel: [equal(i1+i2,i3),equal(i1-i3,i2),equal(i1,i2+i3)];

map('assume,rel) => [[equal((- i3) + i2 + i1, 0)], [equal((- i3) - i2 + i1, 0)], [equal((- i3) - i2 + i1, 0)]] <<< has accepted all these assertions

map('is,rel) => [true, unknown, unknown] <<< doesn't recognize the exact cases that were asserted

This does NOT happen if you don't assume equal(i1+i2,i3).

rtoy commented 2 months ago

Imported from SourceForge on 2024-07-05 10:19:57 Created by peterpall on 2020-02-23 06:45:43 Original: https://sourceforge.net/p/maxima/bugs/3611/#2ac6


For me assume() works on some sums:

assume((4*C_In*R_Load^2+L_Cable1)>0);
is((4*C_In*R_Load^2+L_Cable1)>0);

and

assume((4*C_In*R_Load^2-L_Cable2)>0);
is((4*C_In*R_Load^2-L_Cable2)>0);

But the assume(equal(something)) syntax used in the original ticket seems not to be supported:

assume(equal(C,0));
is(C=0);
rtoy commented 2 months ago

Imported from SourceForge on 2024-07-05 10:20:00 Created by robert_dodier on 2021-01-18 00:01:09 Original: https://sourceforge.net/p/maxima/bugs/3611/#8eaf


rtoy commented 2 months ago

Imported from SourceForge on 2024-07-05 10:20:04 Created by robert_dodier on 2021-01-18 00:01:09 Original: https://sourceforge.net/p/maxima/bugs/3611/#fbf4


Something to investigate is whether it makes a difference if the names of the variables i1, i2, i3 are permuted.

The assume database is an ordered heap, if I understand the implementation correctly. Exactly where in the heap a new assumption is placed probably depends on variable ordering, and in turn that probably has an effect on whether is can make sense of a query. Just guessing at this point.