On Fri, Mar 15, 2013 at 9:54 AM, Stavros Macrakis <macrakis at alum.mit.edu> wrote:
> Sign shouldn't be modifying the assume database, even with *correct*
> inferences because the user/program loses control of the DB. But it
> shouldn't be clearing existing assumptions either.
Well, that is a good point. CLEARSIGN clears out all stuff introduced
by sign functions, which could include stuff not introduced by 'sign'
(by 'asksign', I guess, dunno if there are other ways to introduce
such facts). So it seems the correct policy is for 'sign' to restore
the assume db to its state when 'sign' was called.
Instead of maintaining a single global list, which will always be
susceptible to competing modification bugs, I wonder if the same
effect (preserving sign assumptions across a single top-level evaluation)
could be achieved by the context mechanism. I won't think too hard
about it if I can get 'sign' & friends to behave well enough to
resolve bug #2557 and the one or two that have been mentioned
in this discussion.
best
Robert Dodier