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

[Morgan Deters]

Hi Cesare, Clark, and Pascal (and everyone),

Thanks for your efforts on the new draft.  I have a few comments on parts
of the draft that haven't yet sparked public debate.  In order, below, (1)
I argue against changing the name of the set-info command to meta-info; and
(2) I seek to clarify certain difficulties in properly handling the
define-fun-rec command.

1. SET-INFO AND META-INFO

First, I would suggest against renaming set-info to meta-info, because this
command is used to signal compliance level.  A typical way for an SMT-LIB
script to advertise its version is with set-info, for example, it may be
marked with:

(set-info :smt-lib-version 2.5)

If a 2.0-compliant solver reads this, it can immediately warn the user that
it does not understand version 2.5 of SMT-LIB---a useful error message, to
be sure.  However, the above is in deprecated syntax.  If this syntax is
dropped in favor of:

(meta-info :smt-lib-version 2.5)

now 2.0-compliant solvers give much less useful errors since they cannot
parse the command at all.

The way the 2.5 draft standard is currently written, the SMT-LIB library
(when updated to the 2.5 standard) will either have to use deprecated
syntax or lead to un-useful errors in 2.0-compliant solvers.  (Neither
option is ideal.)

2. DIFFICULTIES WITH DEFINE-FUN-REC

My second comment has to do with define-fun-rec.  Parsing these is
considerably more difficult than parsing anything else in the standard.
Consider:

(define-fun-rec (
  (f ((x Int)) Int (g (h 4)))
  ;; at this point in the parse, g and h are undefined, but must be
accepted (with
  ;; unknown sorts) until after the entire define-fun-rec block is read
  (g ((x Int)) Int 4)
  (h ((x Int)) Int 3)
  ;; only now can we see that the definition of f is well-sorted
))

The standard is clear on what does and does not make a correct, well-sorted
define-fun-rec.  That is not the issue.  The issue is in supporting this in
an SMT-LIB 2.5 parser.  I'd argue that parsing this block is even more
complicated that parsing mutually-recursive datatypes (which in any case is
not yet in the standard), as there only new sort symbols must be accepted
temporarily and later "filled in"; here, function symbols must be accepted
and later filled in.

Certainly parsing of such blocks is possible, and I'm happy to implement
them.  However, I wanted to raise the issue, since it seems to me that such
complications in parsing work against the spirit of the design of the
SMT-LIB language.

Morgan


On Sat, Sep 27, 2014 at 1:16 PM, Tinelli, Cesare <cesare-tinelli at uiowa.edu>
wrote:

> Dear all,
>
> We, the SMT-LIB coordinators, have been working for some time on the next
> version of the SMT-LIB 2 standard to incorporate several requests from the
> community and fix a few issues in the current language.
> A close-to-final draft of the new version, Version 2.5, can be found at
>
>   http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.5-draft.pdf
>
> We are submitting this document to the community for a final feedback
> round. See below for a few notes on it.
>
> If you have ***any comments, corrections, suggestions or exceptions***,
> please send them to this list as soon as possible but no later than ***Oct
> 27, 2014***.
>
> We will have round of discussion on those as needed. We hope to finalize
> and make the new version official by Nov 15, 2014.
>
> Thanks,
>
>
> Cesare, Clark & Pascal
>
>
> ------------------------
> Notes on the new version
> ------------------------
>
> With a couple of minor exceptions, the new version is backward compatible
> with Version 2.0. A summary of the differences between them is provided in
> Section 1.1.1 of the draft.
>
> The draft is a substantial revision of the Version 2.0 document. In
> particular, the operational semantics of the SMT-LIB language is now
> provided in terms of concrete syntax. Abstract syntax is used, in the
> unchanged Section 5, only to describe the logical semantics of formulas.
>
> Any text specific to Version 2.5 is written in red. As with the Version
> 2.0 document, end notes are used to provide the rationale for salient
> design choices in the extension. Those too are in red.
>
> The current version does not include any changes to the way SMT-LIB logics
> are defined and named. In response to several requests to tame the
> explosion of logics, we are working on a new mechanism for that. This is a
> major change that requires considerable thought and discussion within the
> community, so it will be introduced in a later version.
>
>
>
>
>
>
>
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>
>


-- 
Morgan Deters
Senior Research Scientist
Courant Institute of Mathematical Sciences
251 Mercer St., New York, NY 10012
mdeters at cs.nyu.edu - http://cs.nyu.edu/~mdeters/