[SMT-LIB] QF_UFBV: on last-minute extension with sign

[Alessandro Cimatti]

Hi Clark,

the new version of the QF_UFBV benchmarks is indeed fixed - there are no

undefined symbols - and they are an excellent addition to SMT-LIB.

The use of signed operators is a not a major extension, and it 
seems that many of the interesting benchmarks make use of them.

So, I now think that they shuold all be included in the competition. 

Thanks for your efforts on setting everything up,

Alessandro


> -----Original Message-----
> From: Clark Barrett [mailto:barrett at cs.nyu.edu]
> Sent: Tuesday, July 11, 2006 5:55 PM
> To: Alessandro Cimatti
> Cc: Clark Barrett; SMT-LIB; smtcomp at csl.sri.com
> Subject: Re: QF_UFBV: on last-minute extension with sign
> 
> > However, I think that the extension of QF_UFBV32 with signed
operators
> > should not be accepted at this stage of the competition.
> >
> > In fact, the bit vectors theory has been fixed a long time ago ---
the
> > description was posted on the list by Cesare on May 5th.  The
> > description made it clear that the interpretation would be
> > unsigned. That signed arithmetic would not be part of the theory had
> > been discussed and agreed upon with Cesare, Silvio, and others.
> >
> > No variations were communicated on the topic since. Thus, the
> > competitors entering this category had no reason to include signed
> > operators. A last minute addition to the theory would give them a
> > disadvantage against those who have signed arithmetic operators
> > already available, or somehow knew that the extension was being
taken
> > into consideration.
> >
> > Notice that this is really a last minute extension: for the other
> > categories, not only the theories, but also the benchmarks, have
been
> > frozen more than a week ago.
> 
> Let me comment on why this happened.  When we first formalized the
bit-
> vector
> theory, we anticipated receiving benchmarks from industry that would
fit
> nicely
> in the defined theory and logic.  Unfortunately, these benchmarks
never
> came.
> When it became clear they would not be available, I went looking for
other
> benchmarks.  Stanford offered the ones that I ultimately translated.
> Unfortunately, most of them required the use of signed arithmetic as
well
> as
> arrays.
> 
> One important aim of SMT-LIB is to capture benchmarks in their native
form
> and
> avoid as much as possible translations and re-interpretations, so I
was
> reluctant to make any changes to the theories and signatures used by
the
> benchmarks.
> 
> In fact, I was contemplating adding a theory combining bitvectors with
> arrays
> to properly translate the benchmarks, but upon closer examination, I
> realized
> that in most cases, arrays were simply being used like functions (i.e.
the
> update/store/write feature was not being used).  Thus, I felt that it
was
> more
> accurate to represent these as uninterpreted functions and I made that
> translation.
> 
> A similar translation could have been done to eliminate the signed
> arithmetic
> operations, but I felt that would be against the spirit of SMT-LIB
because
> these are common bit-vector operations, and they should be included in
the
> logic instead.  I am happy with the benchmarks as they are and feel
that
> they
> are an accurate representation of the original application and a good
> addition
> to SMT-LIB.
> 
> The question of whether they should be included in SMT-COMP is
somewhat
> orthogonal, but related.  I tend to think they should be included for
the
> following reasons:
> 
> 1) First, let me clear up a misunderstanding resulting from a typo in
the
>    previous version of the logic (see my previous email).  It is
actually
> the
>    case that 6819 of 8247 files (83%) use the signed operators, not
just
> 437.
>    Perhaps there is still enough variation in the remaining
benchmarks,
> but I
>    don't know.  By the way, I suspect this also explains Alessandro's
note
>    about undeclared symbols.
> 
> 2) The signed comparison and extend operators can be expressed fairly
> simply in
>    terms of the previously existing operators, so it shouldn't be
> difficult to
>    add the extensions.
> 
> 3) One possible criticism is that "native" support for signed
operators
> will be
>    more efficient than implementing them as existing operators, but
for my
> own
>    part, I can say that I expect my system would have the same
performance
> and
>    I don't know of any system that has special performance
capabilities
> for
>    signed operations.
> 
> That said, I am interested in what others think.  Should we use the
full
> set of
> benchmarks for SMT-COMP, or restrict it to the 17% of them that do not
use
> the
> signed operators?  I suggest that the remainder of this discussion
take
> place
> on the smt-comp list rather than the smt-lib list.
> 
> Clark Barrett