assume database



My analysis was not correct, the function isp is not used to query the
assume database. Actually it is only used at the end of mevalp2 (in
compar.lisp) and I cant find any input for which it would return
something other than unknown or a lisp error. I don't really
understand what it is supposed to do, but whatever it does it should
check to see if the input is something that it can handle.

And simple example to get a lisp error is is(f(f(a)));. It is actually
a known bug (1891911 and 1891216).

Andrej

On Mon, Sep 28, 2009 at 11:13 AM, Andrej Vodopivec
<andrej.vodopivec at gmail.com> wrote:
> The documentation for assume states that only certain expressions can
> be put in the assume database:
>
> ? ? The predicates <pred_1>, ..., <pred_n> can only be expressions
> ? ? with the relational operators `< <= equal notequal >=' and `>'.
> ? ? Predicates cannot be literal equality `=' or literal inequality
> ? ? `#' expressions, nor can they be predicate functions such as
> ? ? `integerp'.
>
> however this is never checked.
>
> assume(f(1,f(1)) -> lisp error
> is(f(1,f(1)) -> lisp error
>
> I propose we check if the argument to isp (in db.lisp) is something
> that can be put into assume database:
>
> (defmfun isp (pat)
> ?(if (member (car pat) '(mlessp mleqp mgreaterp mgeqp $equal $notequal))
> ? ? ?(cond ((truep pat))
> ? ? ? ? ? ?((falsep pat) nil)
> ? ? ? ? ? ?(t 'unknown))
> ? ? ?'unknown))
>
> With this change we get
>
> (%i1) assume(f(1,f(1)));
> (%o1) ? ? ? ? ? ? ? ? ? ? ? ? ? ?[meaningless]
> (%i2) is(f(1,f(1)));
> (%o2) ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? unknown
>
> BTW, this fixes the bug exposed with logic.mac
> (http://www.math.utexas.edu/pipermail/maxima/2009/015307.html) which
> is why I got interested.
>
> Andrej
>