(logic QF_BV

:written_by {Silvio Ranise, Cesare Tinelli, and Clark Barrett}
:date {May 7, 2007}

:theory Fixed_Size_BitVectors

:language

 "Closed quantifier-free formulas built over an arbitrary expansion of the
  Fixed_Size_BitVectors signature with free constant symbols over the sorts
  BitVec[m] for 0 < m.  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).
 "

:notes
 "For quick reference, the following is a brief and informal summary of the
  legal symbols in this logic and their meaning (formal definitions are found
  either in the Fixed_Size_Bitvectors theory, or in the extensions below).

  Defined in theory Fixed_Size_Bitvectors:

    Functions/Constants:

    (bit0 BitVec[1])
      - the constant consisting of a single bit with value 0
    (bit1 BitVec[1])
      - the constant consisting of a single bit with value 1
    (concat BitVec[i] BitVec[j] BitVec[m])
      - concatenation of bitvectors of size i and j to get a new bitvector of
        size m, where m = i + j
    (extract[i:j] BitVec[m] BitVec[n])
      - extraction of bits i down to j from a bitvector of size m to yield a
        new bitvector of size n, where n = i - j + 1
    (bvnot BitVec[m] BitVec[m])
      - bitwise negation
    (bvand BitVec[m] BitVec[m] BitVec[m])
      - bitwise and
    (bvor BitVec[m] BitVec[m] BitVec[m])
      - bitwise or
    (bvneg BitVec[m] BitVec[m])
      - 2's complement unary minus
    (bvadd BitVec[m] BitVec[m] BitVec[m])
      - addition modulo 2^m
    (bvmul BitVec[m] BitVec[m] BitVec[m])
      - multiplication modulo 2^m
    (bvudiv BitVec[m] BitVec[m] BitVec[m])
      - unsigned division, truncating towards 0 (undefined if divisor is 0)
    (bvurem BitVec[m] BitVec[m] BitVec[m])
      - unsigned remainder from truncating division (undefined if divisor is 0)
    (bvshl BitVec[m] BitVec[m] BitVec[m])
      - shift left (equivalent to multiplication by 2^x where x is the value of
        the second argument)
    (bvlshr BitVec[m] BitVec[m] BitVec[m])
      - logical shift right (equivalent to unsigned division by 2^x where x is
        the value of the second argument)

    Predicates:

    (bvult BitVec[m] BitVec[m])
      - binary predicate for unsigned less than

  Defined below:

    Functions/Constants:

    Bitvector constants:
      - bvX[m] where X is a numeral in base 10 defines the bitvector constant
        with numeric value X of size m.
      - bvbinX where X is a binary numeral of length m defines the
        bitvector constant with value X and size m.
      - bvhexX where X is a hexadecimal numeral of length m defines the
        bitvector constant with value X and size 4*m.
    (bvnand BitVec[m] BitVec[m] BitVec[m])
      - bitwise nand (negation of and)
    (bvnor BitVec[m] BitVec[m] BitVec[m])
      - bitwise nor (negation of or)
    (bvxor BitVec[m] BitVec[m] BitVec[m])
      - bitwise exclusive or
    (bvxnor BitVec[m] BitVec[m] BitVec[m])
      - bitwise equivalence (equivalently, negation of bitwise exclusive or)
    (bvcomp BitVec[m] BitVec[m] BitVec[1])
      - bit comparator: equals bit1 iff all bits are equal
    (bvsub BitVec[m] BitVec[m] BitVec[m])
      - 2's complement subtraction modulo 2^m
    (bvsdiv BitVec[m] BitVec[m] BitVec[m])
      - 2's complement signed division
    (bvsrem BitVec[m] BitVec[m] BitVec[m])
      - 2's complement signed remainder (sign follows dividend)
    (bvsmod BitVec[m] BitVec[m] BitVec[m])
      - 2's complement signed remainder (sign follows divisor)
    (bvashr BitVec[m] BitVec[m] BitVec[m])
      - Arithmetic shift right, like logical shift right except that the most
        significant bits of the result always copy the most significant
        bit of the first argument.

    The following symbols are parameterized by the numeral i, where i >= 0.

    (repeat[i] BitVec[m] BitVec[i*m])
      - (repeat[i] x) means concatenate i copies of x
    (zero_extend[i] BitVec[m] BitVec[m+i])
      - (zero_extend[i] x) means extend x with zeroes to the (unsigned)
        equivalent bitvector of size m+i
    (sign_extend[i] BitVec[m] BitVec[m+i])
      - (sign_extend[i] x) means extend x to the (signed) equivalent bitvector
        of size m+i
    (rotate_left[i] BitVec[m] BitVec[m])
      - (rotate_left[i] x) means rotate bits of x to the left i times
    (rotate_right[i] BitVec[m] BitVec[m])
      - (rotate_right[i] x) means rotate bits of x to the right y times

    Predicates:

    (bvule BitVec[m] BitVec[m])
      - binary predicate for unsigned less than or equal
    (bvugt BitVec[m] BitVec[m])
      - binary predicate for unsigned greater than
    (bvuge BitVec[m] BitVec[m])
      - binary predicate for unsigned greater than or equal
    (bvslt BitVec[m] BitVec[m])
      - binary predicate for signed less than
    (bvsle BitVec[m] BitVec[m])
      - binary predicate for signed less than or equal
    (bvsgt BitVec[m] BitVec[m])
      - binary predicate for signed greater than
    (bvsge BitVec[m] BitVec[m])
      - binary predicate for signed greater than or equal

 "

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

  - Bitvector Constants:
    The string bv followed by the numeral n and a size [m] (as in bv13[32])
    abbreviates any term t of sort BitVec[m] built only out of the symbols in
    {concat, bit0, bit1} such that

    [[t]] = nat2bv[m](n) for n=0, ..., 2^m - 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.

    For backward compatibility, if the size [m] is omitted, then the size is
    assumed to be 32.

    The string bvbin followed by a sequence of 0's and 1's abbreviates the
    concatenation of a similar sequence of bit0 and bit1 terms.  Thus,
    if n is the numeral represented in base 2 by the sequence of 0's and 1's
    and m is the length of the sequence, then the term represents
    nat2bv[m](n).  For example bvbin0101 is equivalent to bv5[4].

    The string bvhex followed by a sequence of digits and/or letters from A to
    F is interpreted similarly as a concatenation of bit0 and bit1 as follows.
    If n is the numeral represented in hexadecimal (base 16) by the sequence of
    digits and letters from A to F and m is four times the length of the
    sequence, then the term represents nat2bv[m](n).  For example, bvbinFF is
    equivalent to bv255[8].  Letters in the hexadecimal sequence may be in
    either upper or lower case.

  - Bitwise operators

    For all terms s,t of sort BitVec[m], where 0 < m,

    (bvnand s t) abbreviates (bvnot (bvand s t))
    (bvnor s t) abbreviates (bvnot (bvor s t))
    (bvxor s t) abbreviates (bvor (bvand s (bvnot t)) (bvand (bvnot s) t))
    (bvxnor s t) abbreviates (bvor (bvand s t) (bvand (bvnot s) (bvnot t)))
    (bvcomp s t) abbreviates (bvxnor s t) if m = 1, and
       (bvand (bvxnor (extract[|m-1|:|m-1|] s) (extract[|m-1|:|m-1|] t))
              (bvcomp (extract[|m-2|:0] s) (extract[|m-2|:0] t))) otherwise

  - Arithmetic operators

    For all terms s,t of sort BitVec[m], where 0 < m,

    (bvsub s t) abbreviates (bvadd s (bvneg t))
    (bvsdiv s t) abbreviates
      (let (?msb_s (extract[|m-1|:|m-1|] s))
      (let (?msb_t (extract[|m-1|:|m-1|] t))
      (ite (and (= ?msb_s bit0) (= ?msb_t bit0))
           (bvudiv s t)
      (ite (and (= ?msb_s bit1) (= ?msb_t bit0))
           (bvneg (bvudiv (bvneg s) t))
      (ite (and (= ?msb_s bit0) (= ?msb_t bit1))
           (bvneg (bvudiv s (bvneg t)))
           (bvudiv (bvneg s) (bvneg t)))))))
    (bvsrem s t) abbreviates
      (let (?msb_s (extract[|m-1|:|m-1|] s))
      (let (?msb_t (extract[|m-1|:|m-1|] t))
      (ite (and (= ?msb_s bit0) (= ?msb_t bit0))
           (bvurem s t)
      (ite (and (= ?msb_s bit1) (= ?msb_t bit0))
           (bvneg (bvurem (bvneg s) t))
      (ite (and (= ?msb_s bit0) (= ?msb_t bit1))
           (bvurem s (bvneg t)))
           (bvneg (bvurem (bvneg s) (bvneg t)))))))
    (bvsmod s t) abbreviates
      (let (?msb_s (extract[|m-1|:|m-1|] s))
      (let (?msb_t (extract[|m-1|:|m-1|] t))
      (ite (and (= ?msb_s bit0) (= ?msb_t bit0))
           (bvurem s t)
      (ite (and (= ?msb_s bit1) (= ?msb_t bit0))
           (bvadd (bvneg (bvurem (bvneg s) t)) t)
      (ite (and (= ?msb_s bit0) (= ?msb_t bit1))
           (bvadd (bvurem s (bvneg t)) t)
           (bvneg (bvurem (bvneg s) (bvneg t)))))))
    (bvule s t) abbreviates (or (bvult s t) (= s t))
    (bvugt s t) abbreviates (bvult t s)
    (bvuge s t) abbreviates (or (bvult t s) (= s t))
    (bvslt s t) abbreviates:
      (or (and (= (extract[|m-1|:|m-1|] s) bit1)
               (= (extract[|m-1|:|m-1|] t) bit0))
          (and (= (extract[|m-1|:|m-1|] s) (extract[|m-1|:|m-1|] t))
               (bvult s t)))
    (bvsle s t) abbreviates:
      (or (and (= (extract[|m-1|:|m-1|] s) bit1)
               (= (extract[|m-1|:|m-1|] t) bit0))
          (and (= (extract[|m-1|:|m-1|] s) (extract[|m-1|:|m-1|] t))
               (bvule s t)))
    (bvsgt s t) abbreviates (bvslt t s)
    (bvsge s t) abbreviates (bvsle t s)

  - Other operations

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

    (bvashr s t) abbreviates 
      (ite (= (extract[|m-1|:|m-1|] s) bit0)
           (bvlshr s t)
           (bvnot (bvlshr (bvnot s) t)))

    (repeat[1] t) stands for t
    (repeat[j] t) abbreviates (concat t (repeat[|j-1|] t))

    (zero_extend[0] t) stands for t
    (zero_extend[j] t) abbreviates (concat (repeat[j] bit0) t)

    (sign_extend[0] t) stands for t
    (sign_extend[j] t) abbreviates
      (concat (repeat[j] (extract[|m-1|:|m-1|] t)) t)

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

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

 "
)