[SMT-LIB] New draft of Version 2.5 of SMT-LIB released

[Tinelli, Cesare]

Dear all,

This is an update on the status of Version 2.5 of the SMT-LIB standard. We have a new version of the draft at 

  http://smt-lib.org/papers/smt-lib-reference-v2.5-draft-2.pdf

that incorporates most of the suggestions and feedback we received for the first version, both on this list and privately from several of you. 

We'd like to thank all of those who provided their their comments, which as usual we found very useful, and their expressions of support, which is much appreciated.

Because of the quantity and variety of feedback and the length of some previous email discussions, it is not practical for us to reply to each comment individually. So we are attaching below a synopsis of the main changes we made to the document in response to your feedback.

We'd like to ask you to take a look at the new document and let us know if you find any new issues with it. As before, all new text specific to Version 2.5 plus some new clarifying text is in red in the draft. At this point, we hope to have addressed satisfactorily most of the pending issues and so we are looking just for comments on minor problems, unless there are very strong objections to the proposed solutions. More substantial changes and additions will have to wait until the next version.

As a heads up, here is an incomplete list of standard-related tasks we would like to complete next, once Version 2.5 is official, roughly in order of priority:

- Add inductive data types to the standard.
- Add an option to the standard to specify software timeouts. 
- Finalize a theory of strings and regular expressions.
- Propose a new theory of arrays that addresses some of the problems 
  with the current one (in particular, how to output models).
- Do a complete overhaul of the logic-specification mechanism, 
  to address the current explosion of logics.
- Propose a new theory of finite sets.
- Reconsider the definition and use of :named annotations
  (which probably complicate parsing more than they are worth).

As always, new or renewed requests for new features are welcome. We will add them to the list :)

Best,


Cesare, Clark & Pascal


========================================

Minor errors
------------

Thanks to those who proof-read the document and pointed out various types, errors in the wording, and so one. We hope to have fixed all of them. Please feel free to bug us again on anything that you think might have escaped out attention.


Command check-sat-assuming
--------------------------

The previous definition of this command in terms of push and pop was clearly not what people needed (my mistake, Cesare). There was a long discussion on this list on alternatives, several of which we think are overly complicated, in particular for being based on internal implementation details that do not need to be exposed. We have modified the definition of check-sat-assuming in a way that follows the spirit of the discussion. At the end of the day, as Adrien Champion pointed out at some point, we want a solver to check if the current context has a model that satisfies also the given assumptions and, if so, we want to be able to inspect the model as done with models found with check-sat. If the assumptions are inconsistent with the context, we would like to be able to get a subset of them that are already inconsistent. In any case, and regardless of how check-sat-assuming is implemented, the context at the end of a check-sat-assuming call should the same as the one at the beginning.

A couple of additional notes.

1) The check-sat command is now a special case of the new check-sat-assuming: (check-sat-assuming ())

2) We have decided against simply expanding check-sat to allow assumptions as arguments, as currently done in Z3, for instance. This would break an early design decision that, to simplify parsing, each command have a fixed number of arguments (although these arguments can be s-expressions and so lists of things). Changing check-sat to require an argument, a list of assumptions, is not a good option either since it would not be backward compatible.

3) We have not modified the functionality of (get-proof) and (get-unsat-core), which originally could be called only after check-sat returns unsat. Now they can be called also after (check-sat-assuming ()), but not after check-sat-assuming a non-empty list of assumptions. Further discussion is needed to see how to lift the latter constraint---and whether there is an interest in doing that at all.

4) As requested by Alberto Griggio, we have extended the restriction on the assumptions to allow for negated Boolean constants.


Execution modes
---------------

A few of us had lately had started taking about solvers as having different execution modes when explaining their reaction to certain commands. We thought that making this precise might simplify the description of the operational semantics of SMT-LIB scripts. We did that in the new version of the draft, and we think it does simplify things and make them more precise. Modes and mode transitions triggered by the various commands are described in Section 4.1.1 and Figure 4.1. 

Chances are that currently solvers are not 100% compliant with respect to the behavior described in Figure 4.1. However, we think that conforming to that behavior would make for a more uniform and predictable user-experience without introducing any serious restrictions. Feedback on this is of course welcome.


Command reset-assertions
------------------------

As proposed by Alberto Griggio, we modified the specification of the reset-assertions command so that it does not removed top-level declarations and definition from the assertion stack when :global-declarations is true. We agree with the view that setting :global-declarations to true should in essence be equivalent to stating that no declarations/definitions can be retracted.


Command meta-info
-----------------

We have eliminated the new meta-info command and reverted back to the old name, set-info, as requested by Morgan Deter, for the reason he gave in his email to this list on Oct 8, 2014.


Command define-fun-rec
----------------------

As pointed out by several people independently, the proposed syntax of define-fun-rec was problematic in the case of mutually recursive functions because it included forward references to functions not yet defined. To eliminate this problem we have modified the syntax in a new command called define-funs-rec. The previous define-fun-rec has now a simplified syntax and is restricted to defining just a single recursive function.


Command echo
------------

To those who asked why the command is supposed to print back the input string *with the surrounding quotes*, the short answer is that the command returns a string literal, and string literals in SMT-LIB are enclosed in quotes. The longer answer is that it would be difficult to parse the result back without the enclosing strings, or some other syntactical convention that lets the client application know when the response to echo starts and ends. (Consider that string literals in SMT-LIB can contain all sorts of things, including new line characters.)


Shadowing
---------

Although the new version does not change the lexical scoping rules of the language, the previous document was short on the details, especially with regards to shadowing of identifiers. We have added text in a few places that clarifies that.


Command declare-const
---------------------

A couple of people have asked why we added declare-const but not define-const. Neither one is needed and neither one introduces much simplification, but we added the former by popular demand (possibly created by the fact that Z3 has declare-const). In the spirit of keeping the command set small, we would like to introduce define-const only when, and if, we get enough requests for it.