[SMT-LIB] URL for draft Command Language

[David Cok]

Aaron, et al.

Thanks for this document and the work behind it.  I have a few comments 
and suggestions for your consideration.  I come at this with the 
perspective of creating systems that interact with a prover - that is 
that let the user (through some system) add to, remove from, or explore 
a current set of logical formulae and its implications.  Current SMT 
solvers have varying capabilities for this (they're being built to blast 
through benchmarks as fast as possible :-), but I'm hoping that will 
improve over time.

1) Some provers allow for retracting individual assertions.  This is 
sometimes much more convenient than having to organize everything in 
stack fashion in order to use push and pop.  For this, an identifier 
needs to be returned by or provided to an assert statement and a retract 
command would be added.  This would also allow provers that provide 
unsat core information  to respond with a list of identifiers of the 
assertions in the unsat core.  Specifically,
a) either allow an optional, user supplied, identifier with an assert 
statement or have the response to an assert include a prover generated 
identifier, unique to that run of the prover;
b) add a retract command that takes a list of such identifiers and 
removes the corresponding assertions from the current assertion set (and 
be clear about hos this interacts with push and pop)
c) provide a command to query (after an unsat response to a check-sat 
command) for the unsat core, which would reply with a list of assertion 
identifiers (or 'unsupported')

2) This comment is just about the explication.  It is generally unclear, 
both here and in the documentation of some individual provers, what is 
the relationship between (i) the place where an asserted fomula is put  
and (ii) the stack of assertion sets.  In your section 3.7, you state 
that an assert command adds a formula to the current assertion set, 
which is the union of all the assertion sets on the stack, but you don't 
say to which stack element - presumably the 'top' element of the stack.  
But then in 3.4 it should be clearer that the push command adds a new 
empty assertion set to the top of the stack (and that the stack begins 
with just one empty assertion set).  Clarifying this carefully, although 
perhaps pedantic to those used to interacting with provers, will be 
helpful to individuals new to this space and is just what standards need 
to do.

3) It seems to me (in 3.6) that definitions ought to be stacked just 
like assertions (though I agree that declarations are more useful as 
globals).  At least in my usage, definitions serve as just another form 
of assertion.  Without stacking of definitions, I would often need to 
maintain a parallel user-side stack of which definitions occurred in 
which push-pop level.  So perhaps there are use cases for both and there 
should be syntax for defining and declaring both global and stack variables.

4) Although the dump-sat-assertions command gives all the satisfying 
assignment information the prover has , it is also useful to query the 
current satisfying assignment for the values of specific variables.  
There are two types of useful queries.  In one the prover responds with 
just the assigned value  that that variable would have in the 
dump-sat-assertions output and unknown if the variable does not have an 
assignment.  In the other, the prover responds with either that value 
or, if not yet known, a value that is consistent with the current 
satisfying assignment and the new variable-value combination is added to 
the current context.  This second form does require extending the 
search, but an appropriate value should always exist.  This 
functionality is very useful in providing to the user the ability to 
explore the resulting satisfying assignment, without being overloaded 
with extraneous information.  [It is reasonable to require a 
keep-sat-assertions prior to any of these queries.]

5) The command language semantics should allow a push command between a 
check-sat and a keep-sat-assertions.  It is not clear in 3.7 whether it 
is intended to permit that.

6) Since some functionality is optional or provers might have extended 
or experimental functionality, it should be possible to query the prover 
for which functionality is supported, in some agreed, standard way, 
without having to actually try that functionality. The get-info command 
could be used, as in
"get-info supports retract", which would return 'success' or 'unsupported' .


Comments welcome.

- David (Cok)