[SMT-LIB] URL for draft Command Language

[Michal Moskal]

It's good to see such standard coming up. Thanks for all work on it.

Here are my comments:

1. it might be useful to have standard option for time limit
(expressed in seconds, but with decimal fractions allowed; yes it is
sometimes useful to have timeout lower than one second and the same
argument might one day hold for miliseconds ;-)

2. similarly an option for limiting the memory consumption (in
megabytes I guess)

3. it might be good idea to have to tell the prover we're going to
request the model and/or proof before starting the search, or even
before asserting anything, so boolean options model-required and
proof-required would be required to be set to true and otherwise the
dump-proof/model would be allowed to fail

4. the commands all require parenthesis (e.g., (exit) ), while
responses do not (e.g., unsupported). For parsing simplicity maybe it
would be better for all responses to be parenthesied

5. the current idea about getting output from the solver, while it is
running, seems to be to use the secondary output channel. However,
this introduces additional complexity in the tool interacting with the
solver, which needs to select() on two channels. This is somewhat
annoying to implment, particularly under .NET. While we might want to
keep these separate two channels, we might also have a standard format
for common kinds of asynchronous output coming out of the solver,
namely (warning ...) and (statistics ...) or maybe (info ...). If we
would limit the allowed output from the solver, while it is proving,
to (warning ...), (info ...) and (sat/unsat/unknown) (or maybe (result
sat/unsat/unknown)), using just one output channel would be perfectly
doable. Note, that it sill allows the prover to print whatever it
wants using (info ...). Such (info ...) could be for example used to
implement the "Z3 Inspector" kind of interface I demoed during the
workshop.

6. It might be useful to have errors (and warnings/infos)
categoriezed, e.g. (error no-triggers "cannot find a trigger not
invovling arithmetic symbols in (forall (x y) (x + y > 0))"). After a
while it might become clear what are the common kinds of warnings
(which might get into an appendix to the standard), and some tools
using SMT solvers will decide to ignore some categories.

7. now, this is somewhat serious problem with undeclare (we talked
about this a bit with Clark during the workshop). Consider (forgive me
the syntax):

declare y : int
declare f : int -> int
let x = f(y)
undeclare f
declare f : int -> int
assert ~(x = f(y))
check-sat

Are the two f's considered to be the same f? I guess they should not
be, because otherwise you need to distinguish between different
overloads of f (i.e., if the new f would have a different type, then
they cannot be the same).

This is somewhat awkward. I understand, that f's need to be
redeclared, if you for example are verifing several programs with one
SMT solver invocation and the source files all contain a function with
the same name but different bodies. However, it might be better,
especially for unambiguous printing of terms, if the name mangling
would be done by the verification tool, and then no undeclare would be
needed.


   Michał