[SMT-LIB] new bitvector theories/logics

Clark Barrett barrett at cs.nyu.edu
Thu May 10 14:53:29 EDT 2007


Greetings all,

As you are probably aware, there has been a lot of discussion about updating
and expanding the bitvector theories and logics of SMT-LIB.  We now have drafts
of the new theories and logics that we would like to get feedback on.  Here are
the highlights:

Two new theories:
Fixed_Width_Bitvectors (Bitvectors of fixed but arbitrarily large size)
Bitvector_ArraysEx     (Bitvectors plus extentional arrays indexed by and containing bitvectors)

Three new logics:
QF_BV    (Based on Fixed_Width_Bitvectors)
QF_UFBV  (Same as above but with uninterpreted functions)
QF_AUFBV (Bitvectors plus uninterpreted functions and arrays)

I am attaching the formal theory and logic files for your feedback.  However,
as they are quite technical, let me point out the most important questions:

1. The logic file QF_BV.smt contains a summary of all the bitvector operations
   from both the theory and the logic.  Please let me know if you think there
   is a problem with any of these choices.

2. The new logic is mostly backward compatible, but in a few cases it is not.
   The following operators have been replaced or renamed in the new version:

    repeat -> repeat[i]
    sign_extend -> sign_extend[i]
    rotate_left -> rotate_left[i]
    rotate_right -> rotate_right[i]
    bvlt -> bvult
    bvleq -> bvule
    bvgeq -> bvuge
    bvgt -> bvugt
    bvsleq -> bvsle
    bvsgeq -> bvsge
    shift_left0, shift_left1 -> eliminated
    shift_right0, shift_right1 -> eliminated
    fill[i] -> eliminated

   I am planning to translate existing benchmarks to use the new version.
   However, this means that people will need to change their parsers.  I don't
   think it will be too hard to update your parsers, but if anyone has strong
   objections to this, please let me know.

3. Once we have the new theories/logics in place, we will be able to add
   several sets of benchmarks that are not expressible in the current
   theory/logic.  We plan to go ahead and use these benchmarks in this year's
   competition.  Thus, we are proposing 3 bitvector divisions: QF_BV, QF_UFBV,
   and QF_AUFBV, all of which will need to handle a larger set of operations
   than the previous version.  This will require some work for those planning to
   enter the bitvector divisions of the competition.  However, without these
   changes, we are left with only trivial benchmarks, so it seems that going
   ahead is the best thing to do.  I would be happy to hear feedback from
   people about this though.

Thanks,

Clark Barrett
-------------- next part --------------
(theory BitVector_ArraysEx

 :written_by {Clark Barrett}
 :date {May 7, 2007}
 
:sorts_description {
    All sort symbols of the form BitVec[m],
    where m is a numeral greater than 0.

    All sort symbols of the form Array[m:n],
    where m and n are numerals with m > 0 and n > 0.
}

:funs_description {
    All functions from the theory Fixed_Size_Bitvectors.
}

:funs_description {
    All function symbols with arity of the form

      (select Array[m:n] BitVec[m] BitVec[n])

    where
    - m,n are numerals
    - m > 0, n > 0
}

:funs_description {
    All function symbols with arity of the form

      (store Array[m:n] BitVec[m] BitVec[n] Array[m:n])

    where
    - m,n are numerals
    - m > 0, n > 0
}

:preds_description {
    All predicates from the theory Fixed_Size_Bitvectors.
}


 :definition 
 "This is a theory containing an infinite number of copies of the theory of
  functional arrays with extensionality: one for each pair of bitvector sorts.
  It can be formally defined as the union of the SMT-LIB theory
  Fixed_Size_Bitvectors and an infinite number of variants of the SMT-LIB
  theory ArraysEx: one for each distinct signature morphism mapping the sort Index
  to BitVec[m] and the sort Element to Bitvec[n] where m and n range over all
  positive numerals.  In each of the copies of ArraysEx, the sort Array is
  renamed to Array[m:n] and each copy of ArraysEx contributes exactly one select
  function and one store function to the infinite polymorphic family of select
  and store functions described above.
 "

 :notes
 "As in the theory Fixed_Size_Bitvectors, this theory does not
  provide a value for the formal attributes :sorts, :funs, and :preds because
  there are an infinite number of them.  See the notes in theory
  Fixed_Size_Bitvectors for details.

  If for i=1,2, T_i is an SMT-LIB theory with sorts S_i, function symbols F_i,
  predicate symbols P_i, and axioms A_i, by \"union\" of T_1 and T_2 
  we mean the theory T with sorts S_1 U S_2, function symbols F_1 U F_2,
  predicate symbols P_1 U P_2, and axioms A_1 U A_2 (where U stands for set
  theoretic union).

  The theory T is a well-defined SMT-LIB theory whenever S_1, S_2, F_1, F_2, 
  P_1, P_2 are all pairwise disjoint, as is the case for the component theories
  considered here. 
 "
)


-------------- next part --------------
(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)
    (bvredor BitVec[m] BitVec[1])
      - reduction or: equals bit0 iff all bits are 0
    (bvredand BitVec[m] BitVec[1])
      - reduction and: equals bit1 iff all bits are 1
    (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)))
    (bvredor t) abbreviates t if m = 1, and
       (bvor (extract[|m-1|:|m-1|] t) (bvredor (extract[|m-2|:0] t))) otherwise
    (bvredand t) abbreviates (bvnot (bvredor (bvnot t)))
    (bvcomp s t) abbreviates (bvredand (bvxnor s t))

  - 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)
           (bvneg (bvlshr (bvadd (bvneg s) bv1[m]) 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

 "
)

-------------- next part --------------
(logic QF_UFBV

:written_by {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 function and predicate 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).
 "

:extensions
 "As in the logic QF_BV."
)

-------------- next part --------------
(logic QF_AUFBV

 :written_by {Clark Barrett}
 :date {May 7, 2007}
 
 :theory BV_ArraysEx

 :language 
 "Closed quantifier-free formulas built over an arbitrary expansion of the
  BV_ArraysEx signature with free function and predicate symbols over
  the sorts of BV_ArraysEx.  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
 "As in the logic QF_BV."
)


-------------- next part --------------
(theory Fixed_Size_BitVectors

:written_by {Silvio Ranise, Cesare Tinelli, and Clark Barrett}

:date {May 7, 2007}

:notes
   "Against the requirements of the current SMT-LIB standard this theory does
    not provide a value for the formal attributes :sorts, :funs, and :preds.
    The reason is that the theory has an infinite number of sort, function, and
    predicate symbols, and so they cannot be specified formally in the current
    SMT-LIB language.  While extending SMT-LIB's type system with dependent
    types would allow a finitary formal specification of all the symbols in
    this theory's signature, such an extension does not seem to be worth the
    trouble at the moment.  As a temporary ad-hoc solution, this theory
    declaration specifies the signature, in English, in the user-defined
    attributes :sorts_description, :funs_description, and :preds_description.
    "

:sorts_description {
    All sort symbols of the form BitVec[m],
    where m is a numeral greater than 0.
}

:funs_description {
    Constant symbols bit0 and bit1 of sort BitVec[1]
}

: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
}

:funs_description {
    All function symbols with arity of the form

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

    where
    - i,j,m,n are numerals
    - 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, bvadd, bvmul, bvudiv, bvurem, bvshl, bvlshr}
    - m is a numeral greater than 0
}

:preds_description {
    All predicate symbols with arity of the form

       (pred BitVec[m] BitVec[m])

    where
    - pred is from {bvult}
    - m is a numeral greater than 0
}

: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 > 0) 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, 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 bit0 and bit1 of sort BitVec[1]

   [[bit0]] := \lambda x : [0,1). 0
   [[bit1]] := \lambda x : [0,1). 1

   - 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, 0 < m.

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

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

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

   - Arithmetic operations

   To define the semantics of the bitvector arithmetic operators, we first
   introduce some additional definitions:

   o (x div y) where x and y are integers with x >= 0 and y > 0 returns the
     integer part of x divided by y (i.e., truncated integer division).

   o (x rem y) where x and y are integers with x >= 0 and y > 0 returns the
     remainder when x is divided by y.  Note that we always have the following
     equivalence (for y > 0): (x div y) * y + (x rem y) = x.

   o bv2nat which takes a bitvector b: [0...m) --> {0,1}
     with 0 < m, 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, 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 rem 2^m

   Now, we can define the following operations.  Suppose s and t are both terms
   of sort BitVec[m], m > 0.

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

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

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

   [[(bvudiv s t)]] := if bv2nat([[t]]) != 0 then
                          nat2bv[m](bv2nat([[s]]) div bv2nat([[t]]))

   [[(bvurem s t)]] := if bv2nat([[t]]) != 0 then
                          nat2bv[m](bv2nat([[s]]) rem bv2nat([[t]]))

   - Shift operations

   Suppose s and t are both terms of sort BitVec[m], m > 0.  We make use of the
   definitions given for the arithmetic operations, above.

   [[(bvshl s t)]] := nat2bv[m](bv2nat([[s]]) * 2^(bv2nat([[t]])))

   [[(bvlshr s t)]] := nat2bv[m](bv2nat([[s]]) div 2^(bv2nat([[t]])))

   Finally, we can define the binary predicate bvult:

   (bvult s t) is interpreted to be true iff bv2nat([[s]]) < bv2nat([[t]])

   Note that the semantic interpretation above is underspecified because it
   does not specify the meaning of (bvudiv s t) or (bvurem s t) in case
   bv2nat([[t]]) is 0.  Since the semantics of SMT-LIB's underlying logic
   associates *total* functions to function symbols, we then consider as models
   of this theory *any* interpretation conforming to the specifications above
   (and defining bvudiv and bvurem arbitrarily when the second argument
   evaluates to 0).  Benchmarks using this theory should only include a
   :status sat or :status unsat attribute if the status is independent of
   the particular choice of model for the theory.

  "

)


More information about the SMT-LIB mailing list