[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