[SMT-LIB] extensions to bitvector theory

[Clark Barrett]

There has been a fair amount of discussion about the bitvector theory and I'd
like to finally make some concrete suggestions that I hope will address the
issues being discussed.  This should be viewed as a tentative proposal where
feedback is welcome.

1. Restriction to length 32

I think that most of us agree that the restriction to bitvectors of length 32
is cumbersome and somewhat artificial.  The reason for this of course was that
the SMT-LIB standard did not easily support an unbounded set of sorts.  I
expect this difficulty to be addressed in the next version of the SMT-LIB
standard, so we should be able to accommodate any size of bitvectors in the
future.

2. Existing operators

Some people have suggested renaming or adding redundant operations to the
existing set.  (For example, an explicit equality operator for bitvectors
rather than using "=".)  I am resistant to this for several reasons: 1) the
existing benchmarks and solvers already support the current operators and
changing them would require a lot of people to make unnecessary changes; 2) we
are striving for a minimal but complete set of operations--we would like to
minimize redundancy; 3) it is impossible to make everyone happy, so the best we
can hope for is to have a set of operations that are expressive enough to
accommodate all benchmarks.

I would encourage those who have suggested adding or changing existing
operators to take a close look at the definitions of existing operators and see
if they will do for your purposes.  If not, or if the definitions seem
ambiguous, let us know, and we will try to address your specific objections.

3. New operators

There are several operations that are not yet supported and I think the time
has come to add these.  Here are the extensions I am suggesting:

For each m > 0:
(bvdiv BitVec[m] BitVec[m] BitVec[m])
(bvsdiv BitVec[m] BitVec[m] BitVec[m])
(bvmod BitVec[m] BitVec[m] BitVec[m])
(bvsmod BitVec[m] BitVec[m] BitVec[m])
(bvshl BitVec[m] BitVec[m] BitVec[m])
(bvlshr BitVec[m] BitVec[m] BitVec[m])
(bvashr BitVec[m] BitVec[m] BitVec[m])

Semantics:

bvdiv: unsigned integer division, any fractional part is dropped
bvsdiv: signed integer division; bit-vectors are assumed to be in two's
        complement; truncation is towards zero
bvmod: unsigned integer modulo (remainder after bvdiv)
bvsmod: signed integer modulo (remainder after bvsdiv)

Note that these semantics follow those of most programming languages (including
C and Verilog).  Note also that the following equation is always satisfied
for a particular choice of signed or unsigned:
  (x/y)*y + (x%y) = x
In smt format, this is:
  (= (bvplus (bvmul (bvdiv x y) y) (bvmod x y)) x), and
  (= (bvplus (bvmul (bvsdiv x y) y) (bvsmod x y)) x)

The actual semantics will be more formal, but I hope this is clear.  Let me
know if it is not.

(bvshl x y): Shift x left by y bits; shift zeroes into least significant bits.
(bvlshr x y): (logical) shift x right by y bits; shift zeroes into most significant bits.
(bvashr x y): (arithmetic) shift x right by y bits; duplicate most significant
              bit (i.e. sign bit) with each shift, so that result has same sign as x.

Please let me know if you have comments or suggestions about these changes.

-Clark