[SMT-LIB] comments on v 2.0

[cok@frontiernet.net]

I had a long plane ride yesterday, providing time to read through the v2.0 document.
Here are some corrections and questions.

- David

Comments on SMTLIB v2.0

1. Section 3.1: Regarding “Characters between the semi-colon character ; and a line breaking character are comments and so are to be ignored by a lexical analyzer.”

The semi-colon character is part of the comment.  The line-breaking character may or may not be. I suggest that it not be, since then a comment serves as white space delineating tokens and two line-breaking characters together (e.g. \r\n) act the same as one.  I suggest rewriting the above as

A character sequence beginning with a semi-colon character (not contained within a "-delimited string), up to but not including the first subsequent line-breaking character, is a comment and is to be ignored by a lexical analyzer.


2. Also, “There is no distinction between line breaks, tabs, and spaces--all are treated as whitespace.” Should perhaps read

“There is no distinction between line breaks, tabs, and spaces (except in ending comments)--all are treated as whitespace.”

3. Figure 3.1:  (par (A) (ite Bool A A)) should be (par (A) (ite Bool A A A))  - as it is in the file it purports to replicate.  Corresponding changes are needed in the text of the :definition (in the Core Theory file also).  Similarly twice in the text below Fig 3.1.

4. Definition 7: Typo – “Let be A and B’ should be ‘Let A and B be’

5. Section 4.4: Typo in the sentence after superscript 6: the should be they

6. Section 4.4.1: the enumeration in the definition breaks at a confusing spot, given the presence of the Figure

Chapter 5
7. The text allows for (push 0) which I presume simply does nothing, as (pop 0).

8. Section 5.1.3 and 5.1.4 should state that calling define-fun define-sort declare-fun declare-sort or assert if the assertion-set stack is empty (all assertion-sets, including the initial one, have been popped) results in an error response.

9. Section 5.1.5. It should be clarified whether produce-proofs need to be set to true only just before get-proof is called, just before check-sat is called, or before any assertions are asserted?

10. Section 5.1.5/5.3: It would be more user-convenient if get-proof returned unsupported if produce-proofs is false, or was defined to return an error response, rather than not being allowed to be called (with presumably arbitrary behavior).  Same for get-unsat-core.  Same for produce-models and produce-assignments and their corresponding commands.

11. error-behavior option – the problem with definition of this option is that a solver may mostly continue after an error, but in some hard cases may want to exit – which behavior is this?  Must a solver be all one or the other?

12. Section 5.4.2 – reason-unknown is allowed to return ‘timeout’ according to Appendix B, but that is not allowed here, nor in Appendix C (I suggest it should allow timeout as a response).  The problem with using fixed reserved words here, rather than terms that might contain a string, is that it makes it harder for solvers to extend this with solver-specific information.  I suppose that could be accomplished with other, non-standard, options.

Nice to haves

13. It may be that changing logics is rare, but I would have preferred that it be allowed to issue a subsequent set-logic command, with the effect of completely resetting the state of the prover, without having to restart the process.  If this were the case, however, the current semantics allowing push and pop operations before a set-logic would change.

14. It would be convenient and easy to implement to have a way of popping everything on the assertion-set stack, probably also pushing the initial empty assertion-set on the stack (e.g. a reset command, or the set-logic command as described above).  At present the caller has to keep track of the current depth, or exit and completely restart the process.