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

[Clark Barrett]

> 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