[SMT-LIB] Draft of SMT-LIB 2.5: request for feedback

[David R. Cok]

Other comments - David

p. 24: Why the restriction of <index> to <simple symbol> rather than 
<symbol> ?

p.27: perhaps have :pattern annotate the forall or exists term, rather 
than its body. That is
(! Q ((x1 t1)) t :pattern p1), since the pattern really applies to the 
quantification, not to the term. But if this  definition reflects 
existing practice, let it be.

p.25: I think it would be helpful to state what a variable is - the 
identifiers bound in a forall or exists or let term - and be clearer in 
the use of the term. p.24 uses the term bound variable as if there are 
also unbound variables. On p.27 (last sentence) the text seems to allow 
variables that are global to the formula - which I don't think exist in 
SMT-LIB, except if you mean variables free in a term but bound by an 
enclosing binding term.

p.31, theory and logics: Some attribute keywords are allowed to be 
repeated, e.g., :sorts and :funs. The document should state that such 
repetitions are equivalent to a single attribute whose value contains 
the concatenation of the values in the repetitions.

p. 49, opening of section 4.1.6: suggest rewording to state that solvers 
are required to respond in a standard way to all options, but, except 
for those that a designated as required, a solver may choose to respond 
'unsupported'.

p. 53: How about a define-const as well?

p. 54 and elsewhere. Why the use of 'assumptions' instead of 
'assertions'? They seem synonymous in this paper but the different 
terminology makes one wonder if they are intended to be different. Here 
particularly, we have only described assertion levels as containing 
declarations, definitions, and assertions. So what are these assumptions 
we are adding?

p.55: in a given sequence of get-value commands (without any 
assertion-set-changing commands) will different instances of the same 
symbol denoting an abstract value have the same value in the model? What 
about in different models after different check-sat commands?

p.65: Must compatible signatures have exactly the same sort symbols or 
must they only agree on the sort symbols they have in common? I see that 
the latter makes n-ary combination more complicated, but it seems to be 
how the concept is used in practice. With the former, which is what is 
stated in the text, one first has to expand each theory with the union 
of all the sorts in all the theories to be combined, before combining 
them. At minimum, that pre-step of expansion is not discussed here.