SMT-LIB format: A detail proposal

[Alessandro Armando]

Dear Cesare and Silvio,

Cesare> a detailed first proposal on the SMT-LIB language and format is finally
Cesare> avalaible on the SMT-LIB website at

Cesare> http://combination.cs.uiowa.edu/smtlib/proposal.pdf

Cesare> The proposal was drafted taking into account as much as possible the
Cesare> suggestions made in this discussion list.

Thank you very much for your work.  The document is well written and I
largely agree with the proposed approach.  Here are a few comments
from me:

1. If I am not mistaken, the type system you propose does not assume
   types are disjoint neither allows you to express their
   disjointness.  This can be a problem as in many practical
   situations you want to enforce disjointness of types.  Consider for
   instance a theory of arrays where arrays should not be used as
   indexes.  (In a project I am currently working with my group we
   have developed sorted specification language where sorts are
   assumed disjoint by default and subsort declarations allow us to
   express sort inclusion.  This approach works nicely for our
   purposes, but could have problems in other contexts.  So other
   groups' experience could be valuable here.)

2. The :definition field of the theory specification (cf Section 5 of
   the document) is restricted to be a string.  While this is ok when
   a presentation the theory is not always readily available, it does
   not provide formal support to the specification of the theory when
   a presentation is available (e.g. the theory of array).  My
   proposal is to add an optional :presentation field whose value is
   a set of formulae.

Cesare> As announced earlier, the proposal will be discussed in a panel of the
Cesare> PDPAR03 this July 29 during CADE-19 (see
Cesare> http://www.loria.fr/~ranise/pdpar03/page.html).

Cesare> We again invite everybody who will be attending PDPAR or CADE to also
Cesare> attend the panel. Those who cannot, are invite to post their comments
Cesare> and further suggestions on this list.

Cesare> We plan to review the proposal, following the indications of the PDPAR
Cesare> panels and the discussion on this list, and produce a second version
Cesare> by the end of August.

As you know, unfortunately I won't be able to be in Miami for CADE.  I
am sure PDPAR03 will be a very successful workshop and I look forward
to hearing the ideas that will be raised during the panel.  (You will
produce a short report, won't you? ;-) )

Regards,

alessandro

--
Alessandro Armando		    e-mail: armando at dist.unige.it
DIST - Universita' di Genova,       http://www.mrg.dist.unige.it/~armando
viale Causa 13,                     phone:  +39-0103532216
16145 GENOVA, ITALY                 fax:    +39-0103532948
				    mobile: +39-3281003201