SMT-LIB format: A detail proposal

[Cesare Tinelli]

Dear Alessandro,

thank you for your first comments on the paper.

Alessandro Armando wrote:
 > 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
 >
Correct.


 > neither allows you to express their
 >    disjointness.
 >
Not quite. See later.

First, we think that a clarification on what is meant by "disjoint"
is needed here. According to the proposed translation semantics for
the SMT-LIB language, subsorting does not correspond to set inclusion
but to set embedding.
The semantics allows models in which a sort symbol S_1 declared as
a subsort of a symbol S_2 is interpreted not as a subset of S_2 but
as a set that *embeds* into S_2, that is, a set isomorphic to a
subset of S_2. In that model, the sets denoted by S_1 and S_2
may as well be disjoint, (or not, it does not matter).
This view of subsorts is common in the literature. It is more
flexible than insisting on subset inclusion.

We take it then that by saying S_1 and S_2 are disjoint,
you just mean that no individual has both sort S_1 and S_2.

 > 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.)
 >
Comments by others are indeed solicited.

In the meantime, we show how sort constraints such as sort disjointness
can already be expressed in the current language, albeit perhaps a bit
indirectly.

In fact, suppose that S_1 and S_2, the sort we want to be disjoint,
have a common supersort in the signature. Then we can express their
disjointness in the proposed language by an appropriate use of
quantifiers. There are many ways to do this. Probably the most
coincise is to use the sentence:

(:forall (x S_1) (:forall (y S_2) (:not (= x y))))

(Incidentally, note that a similar use of quantifiers to express
sort constraints is provided in the paper in the Examples section,
where the definition of REALS-II specifies, among other things,
that the sum of two naturals is a natural.)

Currently the only problem is with sorts that do not have a
common supersort. The supersort is necessary really just to make
the formula above well-sorted.
So, a simple solution to the problem, both syntactically and
semantically, would be to add to language a predefined universal
sort Top (a bit like the "Object" class in Java).
Syntactically, we would then have that every declared sort is
implicitly a subsort of Top. Semantically, we would have that
everything is a Top ($\forall x. Top(x)$).

We decided against adding a top sort from the beginning, mainly
for the sake of simplicity, but considering that the disjointness
constraint is a useful one to have, we are not opposed to adding
it the language.
But we encourage everybody to express their opinion on this.


 > 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.
 >
As mentioned in the paper, the theory specification is meant for the
human reader, especially because in SMT solvers the backgound theory
is typically built-in (with a decision procedure).
But of course other approaches to satisfiability modulo theory are
conceivable in which a solver takes as input both the formula to be
checked *and* the background theory.
Therefore, we have no objections to this proposal either.

Unless there are objections or alternative proposal by others in the
meantime, we will then bring both points up at the PDPAR panel and
recommend the introduction of a top supersort in the language
and a :definition field in the theory specification.


[...]
 >
 > 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.
 >
We too look forward to the panel.
But let us stress to everybody that comments and suggestions are welcome
on this email forum from all of you at any time, no matter whether you
will be able to attend the panel or not.


 > (You will
 > produce a short report, won't you? ;-) )
 >
We will certaintly produce a report. But we cannot promise it will be
a short one :)

Best,


Silvio & Cesare



 > 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
 >
 >
 >
 >