[SMT-LIB] BitVectors32

[Clark Barrett]

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

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

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

-Clark