[SMT-LIB] bitvectors

[Clark Barrett]

Despite our best efforts, some inconsistencies and typos have been identified
in the bitvector theory and logic.  Here are the problems and their solutions.
An updated version of the theory and logic have been posted on the web site.

1) The identifier bv1 was overloaded with two conflicting definitions (either
   11111111111111111111111111111111 or 00000000000000000000000000000001).  We
   will keep the second definition.  The definition of bv1 in the theory file
   is now:

   [[bv1]] := \lambda x : [0...32). if x = 0 then 1 else 0

   This change also required changing the definition of fill in the logic.
   That definition is now:

  For all numerals j with 0 < j <= 32,
  - (fill[j] bit0) abbreviates (extract[|j-1|:0] bv0)
  - (fill[j] bit1) abbreviates (repeat j bit1)

2) The definition of concat was inconsistent with our convention that
   most-significant-bit should be on the left and least-significant-bit on the
   right.  The definition of concat is now:

   - Function symbols for concatenation
   [[(concat s t)]] := \lambda x : [0...n+m).
                          if (x<m) then [[t]](x) else [[s]](x-m)
   where
   s and t are terms of sort BitVec[n] and BitVec[m], respectively,
   0 < n <= 32, 0 < m <= 32, and n+m <= 32.

3) The signed comparison operators were incorrectly listed as sbvlt, sbvleq,
   sbvgt, sbvgeq.  They should be bvslt, bvsleq bvsgt, and bvsgeq.

I apologize for these changes, but they are necessary to make the definitions
consistent with each other and with the benchmarks.

I will respond to Alessandro Cimatti's comments about signed operators in a
separate email.

Clark Barrett