[SMT-LIB] corrected version of bitvector theory and logic

[Cesare Tinelli]

Hi all,

Clark Barrett has kindly pointed out several small errors in the latest 
version of the bitvector theory and logic. The revised definitions 
follow below.

The only major change with respect to the previous version is that now 
the logic also allows free function and predicate symbols, in addition 
to free constants.

Unless there are any objections by tomorrow, we will officially
add this theory and logic to SMT-LIB, together with a 32-bit version of 
them.

Best,


Cesare


--------------------- bv4.theory -------------------------------

(theory Fixed_Size_BitVectors[4]

:written_by {Silvio Ranise and Cesare Tinelli}

:date {10/05/2006}

:sorts_description
   "All sort symbols of the form BitVec[i],
    where i is a numeral between 1 and 4, inclusive."

:funs_description
   "All function symbols with arity of the form

      (concat BitVec[i] BitVec[j] BitVec[m])

    where
    - i,j,m are numerals
    - i,j > 0
    - i + j = m <= 4
   "

:funs_description
   "All function symbols with arity of the form

      (extract[i:j] BitVec[m] BitVec[n])

    where
    - i,j,m,n are numerals
    - 4 >= m > i >= j >= 0,
    - n = i-j+1.
   "

:funs_description
   "All function symbols with arity of the form

       (op1 BitVec[m] BitVec[m])
    or
       (op2 BitVec[m] BitVec[m] BitVec[m])

    where
    - op1 is from {bvnot, bvneg}
    - op2 is from {bvand, bvor, bvxor, bvsub, bvadd, bvmul}
    - m is a numeral
    - 0 < m <= 4
   "

:preds_description
   "All predicate symbols with arity of the form

       (pred BitVec[m] BitVec[m])

    where
    - pred is from {bvlt, bvleq, bvgeq, bvgt}
    - m is a numeral
    - 0 < m <= 4
   "

:definition
  "This is a core theory for fixed-size bitvectors where the operations
   of concatenation and extraction of bitvectors as well as the usual
   logical and arithmetic operations are overloaded.
   The theory is defined semantically as follows.

   The sort BitVec[m] (for m=1, ..., 4) is the set of finite functions
   whose domain is the initial segment of the naturals [0...m), meaning
   that 0 is included and m is excluded, and the co-domain is {0,1}.

   The semantic interpretation [[_]] of well-sorted BitVec-terms is
   inductively defined as follows.

   - Variables
   If v is a variable of sort BitVec[m] with 0 < m <= 4, then
   [[v]] is some element of [{0,...,m-1} -> {0,1}], the set of total
   functions from {0,...,m-1} to {0,1}.

   - Constant symbols bv0 and bv1 of sort BitVec[4]
   [[bv0]] := \lambda x : [0...4). 0
   [[bv1]] := \lambda x : [0...4). 1

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

   - Function symbols for extraction
   [[(extract[i:j] s)]] := \lambda x : [0...i-j+1). [[s]](j+x)
   where s is of sort BitVec[l], 0 <= j <= i < l <= 4.

   - Function symbols for bit-wise operations
   [[(bvnot s)]] := \lambda x : [0...m). if [[s]](x) = 0 then 1 else 0

   [[(bvand s t)]] := \lambda x : [0...m).
                         if [[s]](x) = 0 then 0 else [[t]](x)

   [[(bvor s t)]] := \lambda x : [0...m).
                         if [[s]](x) = 1 then 1 else [[t]](x)

   [[(bvxor s t)]] := \lambda x : [0...m).
                         if [[s]](x) = [[t]](x) then 0 else 1
   where s and t are both of sort BitVec[m] and 0 < m <= 4.

   - Function symbols for arithmetic operations

   To define the semantics of the bitvector operators bvadd, bvsub,
   bvneg, and bvmul, it is helpful to use these ancillary functions:

   o bv2nat which takes a bitvector b: [0...m) --> {0,1}
     with 0 < m <= 4, and returns an integer in the range [0...2^m),
     and is defined as follows:

       bv2nat(b) := b(m-1)*2^{m-1} + b(m-2)*2^{m-2} + ... + b(0)*2^0

   o nat2bv[m], with 0 < m <= 4, which takes a non-negative integer
     n and returns the (unique) bitvector b: [0,...,m) -> {0,1}
     such that

       b(m-1)*2^{m-1} + ... + b(0)*2^0 = n MOD 2^m

     where MOD is usual modulo operation.


   [[(bvadd s t)]] := nat2bv[m](bv2nat(s) + bv2nat(t))

   [[(bvsub s t)]] := nat2bv[m](2^m + bv2nat(s) - bv2nat(t))

   [[(bvneg s)]] := nat2bv[m](2^m - 1 - bv2nat(s))

   [[(bvmul s t)]] := nat2bv[m](bv2nat(s) * bv2nat(t))

   where s and t are both of sort BitVec[m].
  "

:sorts ( BitVec[1] BitVec[2] BitVec[3] BitVec[4] )

:funs (
(bv0 BitVec[4]) (bv1 BitVec[4]))

(concat BitVec[1] BitVec[1] BitVec[2])
(concat BitVec[1] BitVec[2] BitVec[3])
(concat BitVec[1] BitVec[3] BitVec[4])
(concat BitVec[2] BitVec[1] BitVec[3])
(concat BitVec[2] BitVec[2] BitVec[4])
(concat BitVec[3] BitVec[1] BitVec[4])

(extract[0:0] BitVec[1] BitVec[1])
(extract[0:0] BitVec[2] BitVec[1])
(extract[1:0] BitVec[2] BitVec[2])
(extract[1:1] BitVec[2] BitVec[1])
(extract[0:0] BitVec[3] BitVec[1])
(extract[1:0] BitVec[3] BitVec[2])
(extract[2:0] BitVec[3] BitVec[3])
(extract[1:1] BitVec[3] BitVec[1])
(extract[2:1] BitVec[3] BitVec[2])
(extract[2:2] BitVec[3] BitVec[1])
(extract[0:0] BitVec[4] BitVec[1])
(extract[1:0] BitVec[4] BitVec[2])
(extract[2:0] BitVec[4] BitVec[3])
(extract[3:0] BitVec[4] BitVec[4])
(extract[1:1] BitVec[4] BitVec[1])
(extract[2:1] BitVec[4] BitVec[2])
(extract[3:1] BitVec[4] BitVec[3])
(extract[2:2] BitVec[4] BitVec[1])
(extract[3:2] BitVec[4] BitVec[2])
(extract[3:3] BitVec[4] BitVec[1])

(bvnot BitVec[1] BitVec[1])
(bvnot BitVec[2] BitVec[2])
(bvnot BitVec[3] BitVec[3])
(bvnot BitVec[4] BitVec[4])

(bvand BitVec[1] BitVec[1] BitVec[1])
(bvand BitVec[2] BitVec[2] BitVec[2])
(bvand BitVec[3] BitVec[3] BitVec[3])
(bvand BitVec[4] BitVec[4] BitVec[4])

(bvor BitVec[1] BitVec[1] BitVec[1])
(bvor BitVec[2] BitVec[2] BitVec[2])
(bvor BitVec[3] BitVec[3] BitVec[3])
(bvor BitVec[4] BitVec[4] BitVec[4])

(bvxor BitVec[1] BitVec[1] BitVec[1])
(bvxor BitVec[2] BitVec[2] BitVec[2])
(bvxor BitVec[3] BitVec[3] BitVec[3])
(bvxor BitVec[4] BitVec[4] BitVec[4])

(bvadd BitVec[1] BitVec[1] BitVec[1])
(bvadd BitVec[2] BitVec[2] BitVec[2])
(bvadd BitVec[3] BitVec[3] BitVec[3])
(bvadd BitVec[4] BitVec[4] BitVec[4])

(bvneg BitVec[1] BitVec[1])
(bvneg BitVec[2] BitVec[2])
(bvneg BitVec[3] BitVec[3])
(bvneg BitVec[4] BitVec[4])

(bvsub BitVec[1] BitVec[1] BitVec[1])
(bvsub BitVec[2] BitVec[2] BitVec[2])
(bvsub BitVec[3] BitVec[3] BitVec[3])
(bvsub BitVec[4] BitVec[4] BitVec[4])

(bvmul BitVec[1] BitVec[1] BitVec[1])
(bvmul BitVec[2] BitVec[2] BitVec[2])
(bvmul BitVec[3] BitVec[3] BitVec[3])
(bvmul BitVec[4] BitVec[4] BitVec[4])
)


:preds (
(bvleq BitVec[1] BitVec[1])
(bvleq BitVec[2] BitVec[2])
(bvleq BitVec[3] BitVec[3])
(bvleq BitVec[4] BitVec[4])

(bvlt BitVec[1] BitVec[1])
(bvlt BitVec[2] BitVec[2])
(bvlt BitVec[3] BitVec[3])
(bvlt BitVec[4] BitVec[4])

(bvgeq BitVec[1] BitVec[1])
(bvgeq BitVec[2] BitVec[2])
(bvgeq BitVec[3] BitVec[3])
(bvgeq BitVec[4] BitVec[4])

(bvgt BitVec[1] BitVec[1])
(bvgt BitVec[2] BitVec[2])
(bvgt BitVec[3] BitVec[3])
(bvgt BitVec[4] BitVec[4])
)
)



------------------ bv4.logic ----------------------------------

(logic QF_UFBV[4]

:written_by {Silvio Ranise and Cesare Tinelli}
:date {10/05/2006}

:theory Fixed_Size_BitVectors[4]

:language
  "Closed quantifier-free formulas built over an arbitrary expansion
   of the Fixed_Size_BitVectors[4] signature with free function and
   predicate symbols over the sorts BitVec[m] for 0 < m <= 4.
   Formulas in ite terms must satisfy the same restriction as well,
   with the exception that they need not be closed (because they may
   be in the scope of a let expression).
  "

:extensions
  "Below, let |exp| denote the integer resulting from the evaluation
   of the arithmetic expression exp.

   - bit0 abbreviates (extract[0:0] bv0)
   - bit1 abbreviates (extract[0:0] bv1)

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

   - the string bv followed by the numeral n (as in bv13) abbreviates
     any term t of sort BitVec[4] built out only of the symbols in
     {concat, bit0, bit1} such that

     [[t]] = nat2bv[4](n) for n=0, ..., 2^4 - 1.

     See the specification of the theory's semantics for a definition
     of the functions [[_]] and nat2bv.
     Note that this convention implicitly considers the numeral n as a
     number written in base 10.

   - (bvnand s t) abbreviates (bvnot (bvand s t))
   - (bvnor s t) abbreviates (bvnot (bvor s t))

   For all numerals j > 1 and 1 <= m <= 4, and all terms of s and t of
   sort BitVec[m],

   - (shift_left0 t 0) stands for t
   - (shift_left0 t j) abbreviates
     bit0 if m = 1, and
     (shift_left0 (concat (extract[|m-2|:0] t) bit0) |j-1|) otherwise

   - (shift_left1 t 0) stands for t
   - (shift_left1 t j) abbreviates
     bit1 if m = 1, and
     (shift_left1 (concat (extract[|m-2|:0] t) bit1) |j-1|) otherwise

   - (shift_right0 t 0) stands for t
   - (shift_right0 t j) abbreviates bit0 if m = 1 and
     (shift_right0 (concat bit0 (extract[|m-1|:1] t)) |j-1|) otherwise

   - (shift_right1 t 0) stands for t
   - (shift_right1 t j) abbreviates bit1 if m = 1 and
     (shift_right1 (concat bit1 (extract[|m-1|:1] t)) |j-1|) otherwise

   - (repeat t 1) abbreviates t
   - (repeat t j) abbreviates (concat t (repeat t |j-1|))
     provided that j*m <= 4

   - (rotate_left t 0) stands for t
   - (rotate_left t j) abbreviates t if m = 1, and
     (rotate_left
      (concat (extract[|m-2|:0] t) (extract[|m-1|:|m-1|] t)
      |j-1|) otherwise

   - (rotate_right t 0) stands for t
   - (rotate_right t j) abbreviates t if m = 1, and
     (rotate_right
      (concat (extract[0:0] t) (extract[|m-1|:1] t))
      |j-1|) otherwise

  "
)