[SMT-LIB] BitVectors32

[Domagoj Babic]

Hi,

On 1/5/07, Clark Barrett <barrett at cs.nyu.edu> wrote:
> > bv(0|1) are in the logic files, but where are bv<op>, op=(add|sub|...)
> > specified?
>
> in the theory file (theory Fixed_Size_BitVectors[32])

Thx, I missed that. Sorry.

> > Also, I'm wondering about a couple of other related things:
> >
> > 1) My application requires a full set of integer operators (sdiv,
> > udiv, urem, mul...).
> > If I generate benchmarks in BitVec[32] format am I supposed to define the
> > operators, or I can just use bvsdiv, for instance?
>
> Currently, we do not have a mechanism for defining macros, so all operations
> must be in the theory or logic file.  However, we are considering extending the
> bitvector logic to include more operators, so please let us know which
> operators you think are necessary.

SDIV,        // Signed division
UDIV,        // Unsigned division
SREM,        // Signed remainder
UREM,        // Unsigned remainder

I'd also suggest replacing the current set of comparisons:
theory file: leq, lt, eq, gt,
extensions: slt, sleq, sgt, sgeq

With a more consistent set:

SETEQ,       // ==
SETNE,       // !=
SETULE,      // <= unsigned
SETUGE,      // >= unsigned
SETULT,      // <  unsigned
SETUGT,      // >  unsigned
SETSLE,      // <= signed
SETSGE,      // >= signed
SETSLT,      // <  signed
SETSGT,      // >  signed

from the theory file it is not clear what leq, lt, eq, gt are. Only when
I saw the signed extensions, I concluded that those in the theory file
are probably unsigned versions.

Although it is easy to encode ASHR/LSHR operators with
shift_right0 and shift_right1, the following set would be (in my opinion)
simpler and more intuitive:

SHL,         // Shift left
ASHR,        // Arithmetic shift right (sign extended)
LSHR,        // Logical shift right (zero extended)

> > 2) Are theorem provers required to interpret all the operators? If not, how
> > do you compare (during the competition) theorem provers that handle
> > expensive operators as UIFs and those that handle them precisely?
>
> Theorem provers that compete in the bitvector division are required to
> interpret all of the operations precisely.  This is one reason we are reluctant
> to add operations that do not appear in any benchmarks.

If you specify the additional operators, I can generate benchmarks from
software verification of open source applications. Just submitted
benchmarks to SAT competition. Without the additional operators, and
with a bit confusing comparisons (at least confusing to me), I can't
generate the benchmarks. Generating 10-20k benchmarks is not a problem.

BTW, what does "packet" mean in egt benchmarks?

Regards,
    Domagoj Babic