[SMT-LIB] URL for draft Command Language

[cok@frontiernet.net]

----- "Jim D Grundy" <jim.d.grundy at intel.com> wrote:

> Hi Aaron
> 

> 
> * As one of the earlier commentators noted, it is overkill to allow
> symbols to be undeclared and redeclared.  A tool that connects via
> this interface, and which allows the undeclaration and redeclaration
> of its symbols can handle the situation via internal name mangling.  I
> could, however, see an application half-way where symbols may be
> undeclared, after which no new uses of them will be allowed.  Knowing
> that, the terms that defined them may be able to be garbage collected
> (when all references to them are gone).
> 

In interactive environments - continually converting a user's system, whatever it is, into logical formulae for the prover - it is a nuisance to have to keep track of names and mangle to new ones.  I find it a much cleaner design to simply pop the logical environment - including names that have been declared - and then assert the new translation of the user's system.  Hence I repeat my earlier comment: allow declarations to be on the stack along with assertions, and removed (undeclared) with a pop.

- David