[SMT-LIB] Draft of SMT-LIB 2.5: request for feedback - typos and minor comments

[David R. Cok]

On my first read through, here is my accumulated list of typos and 
clarifications that do not affect the definition of SMT-LIB. - David


Typos or wording:
p.11: change ":produced-assertions" to ":produce-assertions"
p. 11 (reset-assertions bullet) change 'remove' to 'removes'
p.13: change 'seeked' to 'sought'
p. 17, first full paragraph: change 'set of sort' to 'set of sorts'
p.17: change "a lot more" to "much more"
p.25, last full paragraph: change "specifying the sort of" to 
"specifying the sorts of"
p.27: change "The values of the :named attribute ranges over" to "The 
values of the :named attribute range over"
p. 27: In the example showing the use of :pattern, the syntax such as  
(x1 t1) is used. In this context t1 is a sort, not a term. Since t is 
usually used to designate terms, using a sigma would be better.
p.28: The first alternative of <theory_attribute> should be (:sorts 
<sort_symbol_decl>+ ), as stated on p.29
p.37: Say "all defined sort and function symbols by their respective 
definitions" (two plurals)
p.37: say "complement the values attributes" (plural)
p.43: the uses of @ for abstract values are supposed to be enclosed in 
(as ...) expressions
p.46: change "from a scripts stored" to "from a script stored"
p.47: say "In general, *when* a solver completes"...
p.48: the examples of terms with :named should include a ! symbol - also 
at the top of p.49, p.54, p.55, p.57
p.51: change "is defined by" to "is defined by the"
p.51: change "se Figure 3.8" to "see Figure 3.8"
p. 51: :all-statistics: remove "intervening". [You can't precede 
intervening commands.]
p. 51: :error-behavior : change "solver is states" to "solver is stating"
p. 52: change ":unsupported" to "unsupported"
p. 52 (push): change "no assertion level" to "no assertion levels"
p. 52 (4.2.3): change "new functions symbols" to "new function symbols"
p. 52 (4.2.3): remove "also"
p.54: change ":interactive-mode" to ":produce-assertions"
p.54: change ":set-logic" to "set-logic"
p. 54, check-sat-assuming: change "effect of" to "effect as" (in two places)
p.54, penultimate line: adding a comma - "after the command executes, 
the current context" would improve first-read parsability.
p. 55: change "as the same sort as" to "has the same sort as"
p.56: change "modify the assertions set" to "modify the assertion set"
p.57: change ":unsupported" to "unsupported"
p.59: remove the comma from "(defined later), use" in the penultimate 
paragraph
p.62: change "definedby" to "defined by"
p.64, last line: change "if and only the" to "if and only if the"
p. 74, note 12: perhaps say "by listing a set of axioms as *the value 
of* an :axioms attribute"
p. 75, note 31: change "proving" to "providing"
p. 78: the list of predefined keywords is missing :pattern and 
:produce-unsat-assumptions
p.82: list of command options is missing :produce-unsat-assumptions

Clarifications (perhaps pedantic)
Section: 4.1.6
:diagnostic-output-channel, :regular-output-channel : change "subsequent 
solver output" to "subsequent solver output (including that of the 
current set-option command)
:global declarations, :produce-assertions, :produce-assignments, 
:produce-models, :produce-proofs, :produce-unsat-assumptions, 
:produce-unsat-cores: change "The option may not be set after a 
set-logic without an intervening reset." to "The option may only be set 
after the beginning of a script or a reset command and before the first 
subsequent set-logic command."
:print-success : change "in all responses to commands." to "in all 
subsequent responses to commands, including of the current set-option 
command, until the option is set again to true."
:random-seed : add "The intent for the option that the solver will 
produce identical results for identical input and identical non-zero 
seeds on repeated runs of the solver."
p. 51, :assertion-stack-levels: be clearer about the value. Instead of 
the sentence beginning "Intuitively", say, for example, "The value of n 
returned is the sum of the arguments of all the valid push commands 
minus the sum of the arguments of all the valid pop commands since the 
most recent reset or reset-assertions command."
p. 51, :version : the phrase "a singleton" seems extraneous
p. 53: There is a restriction on user-defined symbols that they are not 
'already present in the assertion stack'. Do we consider that symbols 
from the background theory are defined in the global assertion level? I 
think it would be clearer if we stated in 4.1.3 and/or on p.39 that a 
set-logic command introduces into the global assertion level all the 
sort and function symbols defined by the stated logic.
p.55: we should state somewhere the precise set of commands that "modify 
the assertion set": reset, reset-assertions, assert, push, pop, 
check-sat-assuming
p.78: :axioms is not defined in V 2.0 and 2.5, according to note 12
p.79: the definition of <symbol> should say "a sequence of whitespace 
and printable characters that starts and ends with | and does not 
otherwise include | or \"  , as stated on p.23 (which could use the 
addition of otherwise). [The current wording here allows |a|b| as a 
symbol, which is not a symbol.]