#4746 calling forget gives stack overflow and forgets facts in global context

[Barton Willis]

Calling forget on F(%phi, constant) gives a stack overflow:

(%i1) forget(F(%phi, constant));
INFO: Caught stack overflow exception (sp=0x0000000000412000); proceed with caution.

Maxima encountered a Lisp error:

 Control stack exhausted (no more space for function call frames).
This is probably due to heavily nested or infinitely recursive function
calls, or a tail call that SBCL cannot or has not optimized away.

PROCEED WITH CAUTION.

Automatically continuing.
To enable the Lisp debugger set *debugger-hook* to nil.
INFO: Reprotecting control stack guard (0x0000000000411000+0x21000)

Also, forget incorrectly forgets facts that are in the global context:

(%i1) constantp(%phi);
(%o1)                                true
(%i2) forget(kind(%phi, constant));
(%o2)                       [kind(%phi, constant)]
(%i3) constantp(%phi);
(%o3)                                false

Finally, the user-documentation for forget says that forget "Removes predicates established by assume." Facts in global aren't established by a user using assume, but internally, at least effectively, they are established by assume. So arguably, the user-documentation isn't clear.

[Barton Willis]

Also, calling forget on a mapatom causes a stack overflow:

(%i1)   forget(a[1]);
Message from maxima's stderr stream: INFO: Caught stack overflow exception (sp=0x0000000000411ff0); proceed with caution.

<deleted>

[Barton Willis]

A version of forget that might fix these bugs:

(defun forget (pat)
  (cond
    (($listp pat)
       (fapply 'mlist (mapcar #'forget1 (cdr pat))))

    (t
     (let ((op (and (consp pat) (consp (car pat)) (caar pat))))
       (cond
         ;; Return pat when either (a) pat is atomic, (b) the operator of pat is $kind,
         ;; (c) pat is nonrelational, or (d) pat is a global fact.
         ((or ($mapatom pat)
              (not (member op '($kind mlessp mleqp mgreaterp mgeqp mnotequal $equal $notequal)))
              ($member pat ($facts '$global)))
          pat)

         ;; otherwise, forget the pattern
         (t
          (forget1 pat)))))))

But the check ($member pat ($facts '$global)) seems to require a noticeable amount of time and space.

[Robert Dodier]

Tracing KILL2 seems to show that it is calling itself recursively. Something about F(%phi, constant) makes KILL2 think that recursion is needed -- what is going on there? I notice that the presence of %phi seems to be key -- if it's foo, then the error is avoided.

About refusing to forget facts in the context global, I think I'm OK with removing those, and instead fixing up the documentation to say that built-in assertions in global can be forgotten. In general Maxima doesn't apply the same operations to built-in stuff as to user-defined; looks like this is an area in which it does. I think that's generally a good idea -- applying rules uniformly makes it easier to predict the outcome.

[David Scherfgen]

I would argue that allowing to forget facts such as that %pi is a constant or the newly added zeroa > 0, zerob < 0 is basically never a good idea and creates inconsistent and surprising results.

• These facts are implicitly used in many places in internal Maxima code. Such code will continue to treat %pi like a constant or having a certain value, regardless of whether the fact kind(%pi, constant) exists in the database or not.
• Maxima already forbids assigning a value to %pi and other system constants, so it's only consistent to also forbid making or removing assumptions about them.
• kill restores the initial assumptions on %pi etc. So allowing to forget that %pi is a constant and then calling kill(%pi) would restore the initial assumptions, which is very surprising. One wouldn't expect kill to actually add assumptions, only remove them.
• A user writing a cleanup script or manipulating context states might inadvertently clear these assumptions, leading to bizarre downstream behavior that is incredibly difficult to trace back to a forget call. In fact, a similar thing happened in rtest_limit_extra.mac, which contained aassume(zeroa > 0) followed by some tests and then forget(zeroa > 0). After these facts were promoted to the global context, this test (inadvertently) removed them.
• There is actually some code in place already that seems like it's supposed to prevent forgetting global facts. But it's not working correctly. It does indeed prevent the fact from being deleted from the context object itself, but then it removes the symbol's DATA property, which makes the fact effectively forgotten.